8000 Fix 2SAT.md by dpaleka · Pull Request #1274 · cp-algorithms/cp-algorithms · GitHub
[go: up one dir, main page]
Skip to content

Fix 2SAT.md #1274

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Jun 19, 2024
Merged

Fix 2SAT.md #1274

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
2fb1fdb
Fix 2SAT.md
dpaleka May 10, 2024
a45e808
add example usage, fix var names, descriptions on tests
dpaleka Jun 9, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
119 changes: 68 additions & 51 deletions src/graph/2SAT.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -102,64 +102,81 @@ Below is the implementation of the solution of the 2-SAT problem for the already
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.

```{.cpp file=2sat}
int n;
vector<vector<int>> adj, adj_t;
vector<bool> used;
vector<int> order, comp;
vector<bool> assignment;

void dfs1(int v) {
used[v] = true;
for (int u : adj[v]) {
if (!used[u])
dfs1(u);
struct TwoSatSolver {
int n_vars;
int n_vertices;
vector<vector<int>> adj, adj_t;
vector<bool> used;
vector<int> order, comp;
vector<bool> assignment;

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);
}
order.push_back(v);
}

void dfs2(int v, int cl) {
comp[v] = cl;
for (int u : adj_t[v]) {
if (comp[u] == -1)
dfs2(u, cl);
void dfs1(int v) {
used[v] = true;
for (int u : adj[v]) {
if (!used[u])
dfs1(u);
}
order.push_back(v);
}
}

bool solve_2SAT() {
order.clear();
used.assign(n, false);
for (int i = 0; i < n; ++i) {
if (!used[i])
dfs1(i);

void dfs2(int v, int cl) {
comp[v] = cl;
for (int u : adj_t[v]) {
if (comp[u] == -1)
dfs2(u, cl);
}
}

bool solve_2SAT() {
order.clear();
used.assign(n_vertices, false);
for (int i = 0; i < n_vertices; ++i) {
if (!used[i])
dfs1(i);
}

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(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];
}
return true;
}

comp.assign(n, -1);
for (int i = 0, j = 0; i < n; ++i) {
int v = order[n - i - 1];
if (comp[v] == -1)
dfs2(v, j++);
void add_disjunction(int a, bool na, int b, bool nb) {
// na and nb signify whether a and b are to be negated
a = 2 * a ^ na;
b = 2 * b ^ nb;
int neg_a = a ^ 1;
int neg_b = b ^ 1;
adj[neg_a].push_back(b);
adj[neg_b].push_back(a);
adj_t[b].push_back(neg_a);
adj_t[a].push_back(neg_b);
}

assignment.assign(n / 2, false);
for (int i = 0; i < n; i += 2) {
if (comp[i] == comp[i + 1])
return false;
assignment[i / 2] = comp[i] > comp[i + 1];
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);
}
return true;
}

void add_disjunction(int a, bool na, int b, bool nb) {
// na and nb signify whether a and b are to be negated
a = 2*a ^ na;
b = 2*b ^ nb;
int neg_a = a ^ 1;
int neg_b = b ^ 1;
adj[neg_a].push_back(b);
adj[neg_b].push_back(a);
adj_t[b].push_back(neg_a);
adj_t[a].push_back(neg_b);
}
};
```

## Practice Problems
Expand Down
65 changes: 31 additions & 34 deletions test/test_2sat.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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();
}
0