Skip to content

Commit d0f1a33

Browse files
adamant-pwnadamant-pwn
authored
Merge pull request cp-algorithms#1274 from dpaleka/patch-1
Fix 2SAT.md
2 parents 25b0b11 + a45e808 commit d0f1a33

2 files changed

Lines changed: 99 additions & 85 deletions

File tree

‎src/graph/2SAT.md‎

Lines changed: 68 additions & 51 deletions
Original file line numberDiff line numberDiff line change
@@ -102,64 +102,81 @@ Below is the implementation of the solution of the 2-SAT problem for the already
102102
In the graph the vertices with indices $2k$ and $2k+1$ are the two vertices corresponding to variable $k$ with $2k+1$ corresponding to the negated variable.
103103

104104
```{.cpp file=2sat}
105-
int n;
106-
vector<vector<int>> adj, adj_t;
107-
vector<bool> used;
108-
vector<int> order, comp;
109-
vector<bool> assignment;
110-
111-
void dfs1(int v) {
112-
used[v] = true;
113-
for (int u : adj[v]) {
114-
if (!used[u])
115-
dfs1(u);
105+
struct TwoSatSolver {
106+
int n_vars;
107+
int n_vertices;
108+
vector<vector<int>> adj, adj_t;
109+
vector<bool> used;
110+
vector<int> order, comp;
111+
vector<bool> assignment;
112+
113+
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) {
114+
order.reserve(n_vertices);
116115
}
117-
order.push_back(v);
118-
}
119-
120-
void dfs2(int v, int cl) {
121-
comp[v] = cl;
122-
for (int u : adj_t[v]) {
123-
if (comp[u] == -1)
124-
dfs2(u, cl);
116+
void dfs1(int v) {
117+
used[v] = true;
118+
for (int u : adj[v]) {
119+
if (!used[u])
120+
dfs1(u);
121+
}
122+
order.push_back(v);
125123
}
126-
}
127-
128-
bool solve_2SAT() {
129-
order.clear();
130-
used.assign(n, false);
131-
for (int i = 0; i < n; ++i) {
132-
if (!used[i])
133-
dfs1(i);
124+
125+
void dfs2(int v, int cl) {
126+
comp[v] = cl;
127+
for (int u : adj_t[v]) {
128+
if (comp[u] == -1)
129+
dfs2(u, cl);
130+
}
131+
}
132+
133+
bool solve_2SAT() {
134+
order.clear();
135+
used.assign(n_vertices, false);
136+
for (int i = 0; i < n_vertices; ++i) {
137+
if (!used[i])
138+
dfs1(i);
139+
}
140+
141+
comp.assign(n_vertices, -1);
142+
for (int i = 0, j = 0; i < n_vertices; ++i) {
143+
int v = order[n_vertices - i - 1];
144+
if (comp[v] == -1)
145+
dfs2(v, j++);
146+
}
147+
148+
assignment.assign(n_vars, false);
149+
for (int i = 0; i < n_vertices; i += 2) {
150+
if (comp[i] == comp[i + 1])
151+
return false;
152+
assignment[i / 2] = comp[i] > comp[i + 1];
153+
}
154+
return true;
134155
}
135156

136-
comp.assign(n, -1);
137-
for (int i = 0, j = 0; i < n; ++i) {
138-
int v = order[n - i - 1];
139-
if (comp[v] == -1)
140-
dfs2(v, j++);
157+
void add_disjunction(int a, bool na, int b, bool nb) {
158+
// na and nb signify whether a and b are to be negated
159+
a = 2 * a ^ na;
160+
b = 2 * b ^ nb;
161+
int neg_a = a ^ 1;
162+
int neg_b = b ^ 1;
163+
adj[neg_a].push_back(b);
164+
adj[neg_b].push_back(a);
165+
adj_t[b].push_back(neg_a);
166+
adj_t[a].push_back(neg_b);
141167
}
142168

143-
assignment.assign(n / 2, false);
144-
for (int i = 0; i < n; i += 2) {
145-
if (comp[i] == comp[i + 1])
146-
return false;
147-
assignment[i / 2] = comp[i] > comp[i + 1];
169+
static void example_usage() {
170+
TwoSatSolver solver(3); // a, b, c
171+
solver.add_disjunction(0, false, 1, true); // a v not b
172+
solver.add_disjunction(0, true, 1, true); // not a v not b
173+
solver.add_disjunction(1, false, 2, false); // b v c
174+
solver.add_disjunction(0, false, 0, false); // a v a
175+
assert(solver.solve_2SAT() == true);
176+
auto expected = vector<bool>{{true, false, true}};
177+
assert(solver.assignment == expected);
148178
}
149-
return true;
150-
}
151-
152-
void add_disjunction(int a, bool na, int b, bool nb) {
153-
// na and nb signify whether a and b are to be negated
154-
a = 2*a ^ na;
155-
b = 2*b ^ nb;
156-
int neg_a = a ^ 1;
157-
int neg_b = b ^ 1;
158-
adj[neg_a].push_back(b);
159-
adj[neg_b].push_back(a);
160-
adj_t[b].push_back(neg_a);
161-
adj_t[a].push_back(neg_b);
162-
}
179+
};
163180
```
164181
165182
## Practice Problems

‎test/test_2sat.cpp‎

Lines changed: 31 additions & 34 deletions
Original file line numberDiff line numberDiff line change
@@ -4,50 +4,47 @@ using namespace std;
44

55
#include "2sat.h"
66

7-
void setup(int size) {
8-
n = 2 * size;
9-
adj.clear();
10-
adj.resize(n);
11-
adj_t.clear();
12-
adj_t.resize(n);
7+
void test_2sat_example_usage() {
8+
TwoSatSolver::example_usage();
139
}
1410

1511
void test_2sat_article_example() {
16-
setup(3);
17-
add_disjunction(0, 0, 1, 1); // a v not b
18-
add_disjunction(0, 1, 1, 0); // not a v b
19-
add_disjunction(0, 1, 1, 1); // not a v not b
20-
add_disjunction(0, 0, 2, 1); // a v not c
21-
assert(solve_2SAT() == true);
22-
auto expected = vector<bool>{{false, false, false}};
23-
assert(assignment == expected);
12+
TwoSatSolver solver(3); // a, b, c
13+
solver.add_disjunction(0, false, 1, true); // a v not b
14+
solver.add_disjunction(0, true, 1, false); // not a v b
15+
solver.add_disjunction(0, true, 1, true); // not a v not b
16+
solver.add_disjunction(0, false, 2, true); // a v not c
17+
assert(solver.solve_2SAT() == true);
18+
auto expected = vector<bool>{{false, false, false}};
19+
assert(solver.assignment == expected);
2420
}
2521

2622
void test_2sat_unsatisfiable() {
27-
setup(2);
28-
add_disjunction(0, 0, 1, 0); // x v y
29-
add_disjunction(0, 0, 1, 1); // x v not y
30-
add_disjunction(0, 1, 1, 0); // not x v y
31-
add_disjunction(0, 1, 1, 1); // not x v not y
32-
assert(solve_2SAT() == false);
23+
TwoSatSolver solver(2); // a, b
24+
solver.add_disjunction(0, false, 1, false); // a v b
25+
solver.add_disjunction(0, false, 1, true); // a v not b
26+
solver.add_disjunction(0, true, 1, false); // not a v b
27+
solver.add_disjunction(0, true, 1, true); // not a v not b
28+
assert(solver.solve_2SAT() == false);
3329
}
3430

3531
void test_2sat_other_satisfiable_example() {
36-
setup(4);
37-
add_disjunction(0, 0, 1, 1); // a v not b
38-
add_disjunction(0, 1, 2, 1); // not a v not c
39-
add_disjunction(0, 0, 1, 0); // a v b
40-
add_disjunction(3, 0, 2, 1); // d v not c
41-
add_disjunction(3, 0, 0, 1); // d v not a
42-
assert(solve_2SAT() == true);
43-
// two solutions
44-
auto expected_1 = vector<bool>{{true, true, false, true}};
45-
auto expected_2 = vector<bool>{{true, false, false, true}};
46-
assert(assignment == expected_1 || assignment == expected_2);
32+
TwoSatSolver solver(4); // a, b, c, d
33+
solver.add_disjunction(0, false, 1, true); // a v not b
34+
solver.add_disjunction(0, true, 2, true); // not a v not c
35+
solver.add_disjunction(0, false, 1, false); // a v b
36+
solver.add_disjunction(3, false, 2, true); // d v not c
37+
solver.add_disjunction(3, false, 0, true); // d v not a
38+
assert(solver.solve_2SAT() == true);
39+
// two solutions
40+
auto expected_1 = vector<bool>{{true, true, false, true}};
41+
auto expected_2 = vector<bool>{{true, false, false, true}};
42+
assert(solver.assignment == expected_1 || solver.assignment == expected_2);
4743
}
4844

4945
int main() {
50-
test_2sat_article_example();
51-
test_2sat_unsatisfiable();
52-
test_2sat_other_satisfiable_example();
46+
test_2sat_example_usage();
47+
test_2sat_article_example();
48+
test_2sat_unsatisfiable();
49+
test_2sat_other_satisfiable_example();
5350
}

0 commit comments

Comments
 (0)