add example usage, fix var names, descriptions on tests

src/graph/2SAT.md

@@ -103,17 +103,16 @@ In the graph the vertices with indices $2k$ and $2k+1$ are the two vertices corr
 
 ```{.cpp file=2sat}
 struct TwoSatSolver {
-    int n;
+    int n_vars;
+    int n_vertices;
     vector<vector<int>> adj, adj_t;
     vector<bool> used;
     vector<int> order, comp;
     vector<bool> assignment;
 
-    // n is the number of variables
-    TwoSatSolver(int n) : n(n), adj(2 * n), adj_t(2 * n), used(2 * n), order(), comp(2 * n, -1), assignment(n) {
-        order.reserve(2 * n);
+    TwoSatSolver(int _n_vars) : n_vars(_n_vars), n_vertices(2 * n_vars), adj(n_vertices), adj_t(n_vertices), used(n_vertices), order(), comp(n_vertices, -1), assignment(n_vars) {
+        order.reserve(n_vertices);
     }
-
     void dfs1(int v) {
         used[v] = true;
         for (int u : adj[v]) {
@@ -131,24 +130,23 @@ struct TwoSatSolver {
         }
     }
 
-    // m will be the number of vertices in the graph (= 2 * n)
-    bool solve_2SAT(int m) {
+    bool solve_2SAT() {
         order.clear();
-        used.assign(m, false);
-        for (int i = 0; i < m; ++i) {
+        used.assign(n_vertices, false);
+        for (int i = 0; i < n_vertices; ++i) {
             if (!used[i])
                 dfs1(i);
         }
 
-        comp.assign(m, -1);
-        for (int i = 0, j = 0; i < m; ++i) {
-            int v = order[m - i - 1];
+        comp.assign(n_vertices, -1);
+        for (int i = 0, j = 0; i < n_vertices; ++i) {
+            int v = order[n_vertices - i - 1];
             if (comp[v] == -1)
                 dfs2(v, j++);
         }
 
-        assignment.assign(m / 2, false);
-        for (int i = 0; i < m; i += 2) {
+        assignment.assign(n_vars, false);
+        for (int i = 0; i < n_vertices; i += 2) {
             if (comp[i] == comp[i + 1])
                 return false;
             assignment[i / 2] = comp[i] > comp[i + 1];
@@ -167,6 +165,17 @@ struct TwoSatSolver {
         adj_t[b].push_back(neg_a);
         adj_t[a].push_back(neg_b);
     }
+
+    static void example_usage() {
+        TwoSatSolver solver(3); // a, b, c
+        solver.add_disjunction(0, false, 1, true);  //     a  v  not b
+        solver.add_disjunction(0, true, 1, true);   // not a  v  not b
+        solver.add_disjunction(1, false, 2, false); //     b  v      c
+        solver.add_disjunction(0, false, 0, false); //     a  v      a
+        assert(solver.solve_2SAT() == true);
+        auto expected = vector<bool>{{true, false, true}};
+        assert(solver.assignment == expected);
+    }
 };
 ```
 

test/test_2sat.cpp

@@ -4,50 +4,47 @@ using namespace std;
 
 #include "2sat.h"
 
-void setup(int size) {
-  n = 2 * size;
-  adj.clear();
-  adj.resize(n);
-  adj_t.clear();
-  adj_t.resize(n);
+void test_2sat_example_usage() {
+    TwoSatSolver::example_usage();
 }
 
 void test_2sat_article_example() {
-  setup(3);
-  add_disjunction(0, 0, 1, 1); //     a v not b
-  add_disjunction(0, 1, 1, 0); // not a v     b
-  add_disjunction(0, 1, 1, 1); // not a v not b
-  add_disjunction(0, 0, 2, 1); //     a v not c
-  assert(solve_2SAT() == true);
-  auto expected = vector<bool>{{false, false, false}};
-  assert(assignment == expected);
+    TwoSatSolver solver(3); // a, b, c
+    solver.add_disjunction(0, false, 1, true); //      a  v not b
+    solver.add_disjunction(0, true, 1, false); //  not a  v     b
+    solver.add_disjunction(0, true, 1, true);  //  not a  v not b
+    solver.add_disjunction(0, false, 2, true); //      a  v not c
+    assert(solver.solve_2SAT() == true);
+    auto expected = vector<bool>{{false, false, false}};
+    assert(solver.assignment == expected);
 }
 
 void test_2sat_unsatisfiable() {
-  setup(2);
-  add_disjunction(0, 0, 1, 0); //     x v     y
-  add_disjunction(0, 0, 1, 1); //     x v not y
-  add_disjunction(0, 1, 1, 0); // not x v     y
-  add_disjunction(0, 1, 1, 1); // not x v not y
-  assert(solve_2SAT() == false);
+    TwoSatSolver solver(2); // a, b
+    solver.add_disjunction(0, false, 1, false); //      a  v      b
+    solver.add_disjunction(0, false, 1, true);  //      a  v  not b
+    solver.add_disjunction(0, true, 1, false);  //  not a  v      b
+    solver.add_disjunction(0, true, 1, true);   //  not a  v  not b
+    assert(solver.solve_2SAT() == false);
 }
 
 void test_2sat_other_satisfiable_example() {
-  setup(4);
-  add_disjunction(0, 0, 1, 1); //     a v not b
-  add_disjunction(0, 1, 2, 1); // not a v not c
-  add_disjunction(0, 0, 1, 0); //     a v     b
-  add_disjunction(3, 0, 2, 1); //     d v not c
-  add_disjunction(3, 0, 0, 1); //     d v not a
-  assert(solve_2SAT() == true);
-  // two solutions
-  auto expected_1 = vector<bool>{{true, true, false, true}};
-  auto expected_2 = vector<bool>{{true, false, false, true}};
-  assert(assignment == expected_1 || assignment == expected_2);
+    TwoSatSolver solver(4); // a, b, c, d
+    solver.add_disjunction(0, false, 1, true); //      a  v  not b
+    solver.add_disjunction(0, true, 2, true);  //  not a  v  not c
+    solver.add_disjunction(0, false, 1, false); //     a  v      b
+    solver.add_disjunction(3, false, 2, true); //      d  v  not c
+    solver.add_disjunction(3, false, 0, true); //      d  v  not a
+    assert(solver.solve_2SAT() == true);
+    // two solutions
+    auto expected_1 = vector<bool>{{true, true, false, true}};
+    auto expected_2 = vector<bool>{{true, false, false, true}};
+    assert(solver.assignment == expected_1 || solver.assignment == expected_2);
 }
 
 int main() {
-  test_2sat_article_example();
-  test_2sat_unsatisfiable();
-  test_2sat_other_satisfiable_example();
+    test_2sat_example_usage();
+    test_2sat_article_example();
+    test_2sat_unsatisfiable();
+    test_2sat_other_satisfiable_example();
 }