Comparison with a SAT solver

The SAT problem aims at answering if there exist a set of Boolean variables assignments satisfying a given Boolean expression. So if we can formulate dependencies as a Boolean expression, we can use these well tested tools to compare the result of pubgrub with the one of a SAT solver. SAT solvers usually work with Boolean expressions in a conjunctive normal form (CNF) meaning a conjunction of clauses, an "AND of ORs". So our goal is to convert the following rules of dependency solving into a set of clauses.

  1. There must be only one version per package.
  2. Dependencies of a package must be present if that package is present.
  3. The root package must be present in the solution.

Each package version \((p,v)\) is associated to a unique Boolean variable \(b_{p,v}\) that can be true or false. For a given package \(p\) and its set of existing versions \(V_p\), the property (1) can be expressed by the set of clauses

\[ \{ \neg b_{p,v_1} \lor \neg b_{p,v_2} \ | \ (v_1, v_2) \in V_p^2, v_1 \neq v_2 \}. \]

Each one of these clauses specifies that \(v_1\) or \(v_2\) is not present in the solution for package \(p\). These clauses are generated by the sat_at_most_one function in the testing code. A more efficent approach is used when a package has 4 or more versions but the idea is the same. For a given package version \((p,v)\) depending on another package \(d\) at versions \((v_1, v_2, \cdots, v_k)\), the property (2) can be encoded by the clause

\[ \neg b_{p,v} \lor b_{d,v_1} \lor b_{d,v_2} \lor \cdots \lor b_{d,v_k} \]

specifying that either \((p,v)\) is not present in the solution, or at least one of versions \((v_1, v_2, \cdots, v_k)\) of package \(d\) is present in the solution. Finally, the last constraint of version solving (3) is encoded with the following unit clause,

\[ b_{r,v_r} \]

where \((r, v_r)\) is the root package version for which we are solving dependencies.

Once the conversion to the SAT formulation is done, we can combine it with property testing, and verify the following properties:

  • If pubgrub finds a solution, the SAT solver is also satisfied by that solution.
  • If pubgrub does not find a solution, neither does the SAT solver.