4.2.8 2-SAT

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125

/*

Solve a Boolean formula in 2-CNF, where each clause contains at most two literals. A clause like $(a
\lor b)$ is represented by the implications $\lnot a \rightarrow b$ and $\lnot b \rightarrow a$. The
formula is satisfiable if and only if no variable and its negation belong to the same strongly
connected component of the implication graph.

Variables are numbered from $0$ to $n - 1$. A literal is represented by `literal(variable, value)`,
where `value == true` means the variable itself and `value == false` means its negation.

- `TwoSAT(n)` constructs an empty formula over `n` variables.
- `literal(variable, value)` returns the integer ID for a variable or its negation.
- `add_implication(a, b)` adds the implication $a \rightarrow b$.
- `add_or(a, b)` adds the clause $(`a` \lor `b`)$.
- `add_true(a)` forces literal `a` to be true.
- `add_false(a)` forces literal `a` to be false.
- `add(variable, value)` forces a variable to equal `value`.
- `add(x, xval, y, yval)` adds the clause $(`x` = `xval` \lor `y` = `yval`)$.
- `satisfiable()` returns whether all added clauses can be satisfied and stores one valid assignment
  in `answer`.

Time Complexity:
- O(n) per call to the constructor, where $n$ is the number of variables.
- O(1) per call to `literal()`, `add_implication()`, `add_or()`, `add_true()`, `add_false()`, and
  `add()`.
- O(max(n, m)) per call to `satisfiable()`, where $n$ is the number of variables and $m$ is the
  number of clauses.

Space Complexity:
- O(max(n, m)) for the implication graph and DFS stacks.

*/

#include <algorithm>
#include <vector>

struct TwoSAT {
  int variables;
  std::vector<std::vector<int>> adj, rev;
  std::vector<int> order, component, answer;

  TwoSAT(int n = 0) : variables(n), adj(2 * n), rev(2 * n), answer(n, false) {}

  int literal(int variable, bool value) { return 2 * variable + (value ? 0 : 1); }
  int neg(int x) { return x ^ 1; }

  void add_implication(int a, int b) {
    adj[a].push_back(b);
    rev[b].push_back(a);
  }

  void add_or(int a, int b) {
    add_implication(neg(a), b);
    add_implication(neg(b), a);
  }

  void add_true(int a) { add_implication(neg(a), a); }
  void add_false(int a) { add_implication(a, neg(a)); }
  void add(int variable, bool value) { add_true(literal(variable, value)); }
  void add(int x, bool xval, int y, bool yval) { add_or(literal(x, xval), literal(y, yval)); }

  void dfs_order(int u, std::vector<bool> &visited) {
    visited[u] = true;
    for (int v : adj[u]) {
      if (!visited[v]) {
        dfs_order(v, visited);
      }
    }
    order.push_back(u);
  }

  void dfs_component(int u, int id) {
    component[u] = id;
    for (int v : rev[u]) {
      if (component[v] == -1) {
        dfs_component(v, id);
      }
    }
  }

  bool satisfiable() {
    order.clear();
    component.assign(2 * variables, -1);
    std::vector<bool> visited(2 * variables, false);
    for (int i = 0; i < 2 * variables; i++) {
      if (!visited[i]) {
        dfs_order(i, visited);
      }
    }
    std::reverse(order.begin(), order.end());
    int id = 0;
    for (int u : order) {
      if (component[u] == -1) {
        dfs_component(u, id++);
      }
    }
    for (int i = 0; i < variables; i++) {
      if (component[2 * i] == component[2 * i + 1]) {
        return false;
      }
      answer[i] = component[2 * i] > component[2 * i + 1];
    }
    return true;
  }
};

/*** Example Usage ***/

#include <cassert>
using namespace std;

int main() {
  TwoSAT solver(3);
  int x0 = solver.literal(0, true);
  int not_x0 = solver.literal(0, false);
  int x1 = solver.literal(1, true);
  int x2 = solver.literal(2, true);
  solver.add_or(x0, x1);
  solver.add_or(not_x0, x2);
  solver.add_true(x0);
  solver.add(1, true, 2, false);
  assert(solver.satisfiable());
  assert(solver.answer[0]);
  return 0;
}