Split SAT into its own section

Author: mpizenberg

src/SUMMARY.md

@@ -17,5 +17,6 @@
   - [Building a report tree](./internals/report_tree.md)
 - [Testing and benchmarking](./testing/intro.md)
   - [Property testing](./testing/property.md)
+  - [Comparison with a SAT solver](./testing/sat.md)
   - [Benchmarking](./testing/benchmarking.md)
 - [How can I contribute? Here are some ideas](./contributing.md)

src/testing/property.md

@@ -139,53 +139,3 @@ Here are some of these:
   Only adding dependencies should impact that.
 - **Removing a package that does not appear in a solution cannot break that solution**.
   Just as before, it should not impact the existence of a solution.
-
-
-## Comparison with a SAT solver
-
-The [SAT problem](https://en.wikipedia.org/wiki/Boolean_satisfiability_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)](https://en.wikipedia.org/wiki/Conjunctive_normal_form)
-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 verify the following property:
-
-- **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.**

src/testing/sat.md

@@ -0,0 +1,49 @@
+# Comparison with a SAT solver
+
+The [SAT problem](https://en.wikipedia.org/wiki/Boolean_satisfiability_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)](https://en.wikipedia.org/wiki/Conjunctive_normal_form)
+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.**