Hi codeforces community.
I thought there is no good 2-SAT tutorial in the internet, so I decided to write one.
2-SAT is a special case of boolean satisfiability.
Good question! Boolean satisfiability or just SAT determines whether we can give values (TRUE or FALSE only) to each boolean variable in such a way that the value of the formula become TRUE or not. If we can do so, we call formula satisfiable, otherwise we call it unsatisfiable. Look at the example below:
f = A ∧ ¬B, is satisfiable, cause A = TRUE and B = FALSE makes it TRUE.
but g = A ∧ ¬A, is unsatisfiable, look at this table:
|A||¬A||A ∧ ¬A|
As you can see g is unsatisfiable cause whatever values of its boolean variables are, g is FALSE.
Note: ¬ in ¬X is boolean not operation. ∧ in X ∧ Y is boolean and operation and finally ∨ in X ∨ Y is boolean or operation.
SAT is a
NP-Complete problem, though we can solve 1-SAT and 2-SAT problems in a polynomial time.
Note: This doesn't really exist, I define it cause it help understanding 2-SAT.
Consider f = x 1 ∧ x 2 ∧ ... ∧ x n.
Problem: Is f satisfiable?
Solution: Well 1-SAT is an easy problem, if there aren't both of x i and ¬x i in f, then f is satisfiable, otherwise it's not.
Consider f = (x 1 ∨ y 1) ∧ (x 2 ∨ y 2) ∧ ... ∧ (x n ∨ y n).
Problem: Is f satisfiable?
But how to solve this problem? x i ∨ y i and and are all equivalent. So we convert each of (x i ∨ y i) s into those two statements.
Now consider a graph with 2n vertices; For each of (x i ∨ y i) s we add two directed edges
From ¬x i to y i
From ¬y i to x i
f is not satisfiable if both ¬x i and x i are in the same SCC (Strongly Connected Component) (Why?) Checking this can be done with a simple Kosaraju's Algorithm.
Assume that f is satisfiable. Now we want to give values to each variable in order to satisfy f. It can be done with a topological sort of vertices of the graph we made. If ¬x i is after x i in topological sort, x i should be FALSE. It should be TRUE otherwise.
- SPOJ — BUGLIFE
- SPOJ — TORNJEVI
- UVa — Manhattan
- UVa — Wedding
- CF — The Road to Berland is Paved With Good Intentions
- CF — Ring Road 2
- CF — TROY Query
- CEOI — Birthday party — Solution
func dfsFirst(vertex v): marked[v] = true for each vertex u adjacent to v do: if not marked[u]: dfsFirst(u) stack.push(v) func dfsSecond(vertex v): marked[v] = true for each vertex u adjacent to v do: if not marked[u]: dfsSecond(u) component[v] = counter for i = 1 to n do: addEdge(not x[i], y[i]) addEdge(not y[i], x[i]) for i = 1 to n do: if not marked[x[i]]: dfsFirst(x[i]) if not marked[y[i]]: dfsFirst(y[i]) if not marked[not x[i]]: dfsFirst(not x[i]) if not marked[not y[i]]: dfsFirst(not y[i]) set all marked values false counter = 0 flip directions of edges // change v -> u to u -> v while stack is not empty do: v = stack.pop if not marked[v] counter = counter + 1 dfsSecond(v) for i = 1 to n do: if component[x[i]] == component[not x[i]]: it is unsatisfiable exit if component[y[i]] == component[not y[i]]: it is unsatisfiable exit it is satisfiable exit