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:

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.

1-SAT

Note: This doesn't really exist, I define it cause it help understanding 2-SAT.

Consider f = x₁ ∧ x₂ ∧ ...  ∧ 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.

2-SAT

Consider f = (x₁ ∨ y₁) ∧ (x₂ ∨ y₂) ∧ ...  ∧ (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

1. From ¬x_i to y_i

2. 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.

Some problems:

• 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

Pseudo Code

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