Chapter 14 · Special Topics
2-SAT
The implication graph, the "x and not x in one SCC" criterion, and the assignment read off the condensation order — with the linear-time proof.
#The problem
Variables x1..xn, clauses (a ∨ b) where each literal is xi or ¬ xi. Decide whether a satisfying assignment exists (and produce one). **3**-SAT with the same shape is NP-complete (The NP-complete Graph Problems Worth Knowing); the difference is exactly what makes 2-SAT linear.
#The implication-graph criterion
Rewrite each clause (a ∨ b) as the two implications (¬ a → b) and (¬ b → a). The formula is satisfiable iff no variable xi has xi and ¬ xi in the same strongly connected component of that digraph.
Necessity. If xi ⇝ ¬ xi ⇝ xi, then in any assignment xi ⇒ ¬ xi and ¬ xi ⇒ xi must both hold, which is impossible — every implication on the cycle must be satisfied, and a cycle through both polarities forces a contradiction.
Sufficiency. Contract to the condensation DAG and number the components in topological order. Define
This is well defined: no component contains both literals, so exactly one of the two orders holds. The key structural fact is that the implication graph is skew-symmetric: negating every literal is an anti-automorphism, u → v iff bar v → bar u. Hence on the condensation, C ≤ D iff bar D ≤ bar C (where bar C is the component of the negated literals).
Now suppose a clause (a ∨ b) is falsified by this assignment: a and b are both false, i.e. bar a, bar b both true. Truth of bar a means scc(a) < scc(bar a)... precisely, "bar a true" is the rule applied to the literal bar a, so scc(bar ā) = scc(a) comes before scc(bar a):
The clause's own implications give bar a → b, so scc(bar a) ≤ scc(b), and bar b → a gives scc(bar b) ≤ scc(a). Chaining:
a strict cycle in a DAG — impossible. So no clause is falsified. ∎
#Reading the assignment off the components
After Tarjan/Kosaraju, sat = (comp[2i] != comp[2i+1]) for all i; the assignment is
// literal encoding: 2*i = "x_i is true", 2*i+1 = "x_i is false"
int neg(int l) { return l ^ 1; }
void add_or(int a, int b) { // clause (a or b) as two implications
adj[neg(a)].push_back(b);
adj[neg(b)].push_back(a);
}
// comp[] = component number in REVERSE topological order (Kosaraju's second pass gives it free)
vector<char> sat_ok(2 * n); // ... compute comps first, then:
for (int i = 0; i < n; i++)
if (comp[2*i] == comp[2*i+1]) return false; // x_i and ¬x_i together
for (int i = 0; i < n; i++)
ans[i] = comp[2*i] > comp[2*i+1]; // true iff its SCC is lateri.e. set xi true when its own SCC is later than the SCC of ¬ xi. The comparison uses component numbers from Kosaraju's second pass, which are already in reverse topological order, so no extra sorting is needed.
#Modelling: the clause types you need
Modelling: the three clause types you will actually need
- (¬ a ∨ ¬ b) = "not both": add a → bar b and b → bar a — a conflict edge; this is the "choose an independent set of size..." pattern restricted to pairs,
- a → b (an implication "if x then y") is (¬ a ∨ b): both directions of an equivalence a rightarrow b are two clauses ⇒ a, b in the same SCC, so equality of variables is just SCC merging, and "exactly one of a,b" is (a∨ b)∧(¬ a∨¬ b),
- "at most one of x1..xk is true" needs O(k2) pairwise clauses — quadratic blowup is normally avoided with a chain of auxiliary variables (prefix counters): O(k) clauses, which is the trick used in "sudoku-like grid constraints" and "at most one rectangle per row".
#Four ways 2-SAT solutions die
- Encoding literals as ± i and then mixing "index by |i|" with "index by literal" — use the 2i/2i{+}1 encoding above everywhere, including in
add_or, - forgetting the second implication of each clause (only a → b, not b → a) — satisfiability answers then differ from the truth on formulas with a single unit clause,
- unit clauses (a): must be encoded as (a ∨ a), giving ¬ a → a; a solver that only handles two-literal clauses silently ignores these,
- recursion depth in Tarjan on 2n vertices with n ≤ 106 (Walks, Trails, Paths, Cycles), and using Kosaraju's second-pass order wrongly (it must be reverse finish order of the transposed-first pass, Strongly Connected Components).
#A worked instance
(x1 ∨ x2) ∧ (¬ x1 ∨ x2) ∧ (¬ x2 ∨ ¬ x3) ∧ (x3). Implications: bar 1 → 2, bar 2 → 1, 1 → 2, bar 2 → bar 1, 2 → bar 3, 3 → bar 2, bar 3 → 3. From bar 2 → bar 1 and bar 1 → 2 → bar 3 → bar 2 we get a cycle through bar 2, so scc(bar 2) = scc(bar 3) and 2 forces nothing; no variable and its negation share an SCC, so it is satisfiable, and the topological rule gives x2 = true (its negation's SCC is earlier), x3 = true (unit clause ⇒ bar 3 → 3 forces it), x1 free ⇒ true by the rule. Check: clause 2 is (¬ x1 ∨ x2) = (F ∨ T) ✓.