Cho công thức: f = (x1 ∨ y1) ∧ (x2 ∨ y2) ∧ ... ∧ (xn ∨ yn).
Vấn đề: f có thỏa mãn (satisfiable) không?
xi ∨ yi tương đương với ¬xi → yi và ¬yi → xi. Chuyển mỗi mệnh đề thành hai câu lệnh trên.
Xây đồ thị có 2n đỉnh. Với mỗi (xi ∨ yi) thêm hai cạnh có hướng:
- Từ ¬xi đến yi
- Từ ¬yi đến xi
f không thỏa mãn nếu cả ¬xi và xi cùng thuộc một thành phần liên thông mạnh (SCC - Strongly Connected Component).
Nếu f thỏa mãn, gán giá trị cho biến bằng cách sắp xếp topo (topological sort) các đỉnh. Nếu ¬xi xuất hiện sau xi trong topo → xi = FALSE, ngược lại TRUE.
Mã giả (Pseudo Code)
func dfsFirst(vertex v):
marked[v] = true
for each u adjacent to v:
if not marked[u]: dfsFirst(u)
stack.push(v)
func dfsSecond(vertex v):
marked[v] = true
for each u adjacent to v:
if not marked[u]: dfsSecond(u)
component[v] = counter
for i = 1 to n:
addEdge(not x[i], y[i])
addEdge(not y[i], x[i])
for i = 1 to n:
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 false
counter = 0
flip directions of edges
while stack not empty:
v = stack.pop
if not marked[v]:
counter++
dfsSecond(v)
for i = 1 to n:
if component[x[i]] == component[not x[i]]: unsatisfiable; exit
if component[y[i]] == component[not y[i]]: unsatisfiable; exit
satisfiable; exit