SAT (Boolean satisfiability) is the problem of assigning truth values to variables so that a given Boolean formula becomes true.
A formula is called 2-SAT if it is written in 2-CNF form, that is, as an AND of clauses, where each clause contains exactly two literals.
For example:
The 2-SAT problem can be solved in linear time.
The main idea is to transform the formula into an implication graph.
A clause
Solve these external problems (e.g., from Codeforces) to reinforce the lesson material:
is equivalent to the pair of implications
Indeed, if is false, then must be true. Similarly, if is false, then must be true.
So every clause gives us two directed implications.
We build a directed graph with vertices, where is the number of variables.
For each variable , we create two vertices:
For a clause
we add the edges:
For example, for the formula
we get the following implications:
After building the implication graph, we find all strongly connected components.
Let comp[x] be the component number of vertex x.
If for some variable , the vertices and belong to the same strongly connected component, then no solution exists.
Why? Because in that case:
so both values force each other, which is impossible.
If for every variable we have
then a solution exists.
To construct one valid assignment:
comp[x] > comp[not x];This works when the components are processed in topological order.
The total complexity is:
where is the number of variables and is the number of implications.
int n;
vector<int> v[N]; // implication graph
vector<int> g[N]; // reversed graph
vector<int> order;
int comp[N];
bool used[N];
vector<int> res;
void add_edge(int x, int y) {
v[x].push_back(y);
g[y].push_back(x);
v[y ^ 1].push_back(x ^ 1);
g[x ^ 1].push_back(y ^ 1);
}
// add disjunction (x OR y)
void add_disjunction(int x, int y) {
add_edge(x ^ 1, y);
add_edge(y ^ 1, x);
}
void dfs1(int x) {
used[x] = true;
for (int y : v[x]) {
if (!used[y]) {
dfs1(y);
}
}
order.push_back(x);
}
void dfs2(int x, int c) {
comp[x] = c;
for (int y : g[x]) {
if (comp[y] == -1) {
dfs2(y, c);
}
}
}
bool solve_2SAT() {
order.clear();
for (int i = 0; i < 2 * n; i++) {
used[i] = false;
comp[i] = -1;
}
for (int i = 0; i < 2 * n; i++) {
if (!used[i]) {
dfs1(i);
}
}
for (int i = 2 * n - 1, C = 0; i >= 0; i--) {
int x = order[i];
if (comp[x] == -1) {
dfs2(x, C++);
}
}
res.clear();
for (int i = 0; i < 2 * n; i += 2) {
if (comp[i] == comp[i ^ 1]) {
return false;
} else if (comp[i] > comp[i ^ 1]) {
res.push_back(i);
}
}
return true;
}