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
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151

/*

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 $[0, n)$. A literal is represented by `literal(variable, value)`, where
`value == true` means the variable itself and `value == false` means its negation.

- `TwoSAT(n = 0)` 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$ together with its contrapositive
  $\lnot b \rightarrow \lnot a$. Both edges are required for the strongly connected component test
  to detect contradictions, so callers should not add the contrapositive separately.
- `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.
- `assignment()` returns the valid assignment found by the last successful `satisfiable()` call.

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 edges in the implication graph.

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

*/

#include <algorithm>
#include <vector>

class TwoSAT {
  int variables;
  std::vector<std::vector<int>> adj, rev;
  std::vector<int> order, component, solution;

  static int neg(int x) { return x ^ 1; }

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

  void dfs_order(int u, std::vector<char> &visit) {
    visit[u] = true;
    for (int v : adj[u]) {
      if (!visit[v]) {
        dfs_order(v, visit);
      }
    }
    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);
      }
    }
  }

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

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

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

  void add_or(int a, int b) { add_implication(neg(a), b); }
  void add_true(int a) { add_edge(neg(a), a); }
  void add_false(int a) { add_edge(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)); }

  bool satisfiable() {
    order.clear();
    component.assign(2 * variables, -1);
    std::vector<char> visit(2 * variables);
    for (int i = 0; i < 2 * variables; i++) {
      if (!visit[i]) {
        dfs_order(i, visit);
      }
    }
    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;
      }
    }
    for (int i = 0; i < variables; i++) {
      solution[i] = component[2 * i] > component[2 * i + 1];
    }
    return true;
  }

  const std::vector<int> &assignment() const { return solution; }
};

/*** 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.assignment() == vector<int>{true, true, true}));

  TwoSAT stateful(2);
  assert(stateful.satisfiable());
  vector<int> last_assignment = stateful.assignment();
  stateful.add(0, false);
  stateful.add(1, true);
  stateful.add(1, false);
  assert(!stateful.satisfiable());
  assert(stateful.assignment() == last_assignment);

  TwoSAT implication(2);
  int x = implication.literal(0, true);
  int y = implication.literal(1, true);
  implication.add_true(x);
  implication.add_false(y);
  implication.add_implication(x, y);
  assert(!implication.satisfiable());
  return 0;
}