P59 · 2-SAT in NL

🔊 Listen

1 · Theory

Theorem · 2-SAT ∈ NL

Each 2-clause (a ∨ b) is equivalent to two implications: ¬a → b and ¬b → a. UNSAT iff some var z has paths z → ¬z and ¬z → z. Use NL = coNL: a coNL machine guesses no such cycle exists.

🔊 Listen

2 · Animated demo · auto-plays · loops

🔊 Listen

3 · Pitfalls

The implication-graph trick is specific to 2-clauses. A k-clause for k ≥ 3 has too much flexibility — multiple implications combine non-locally. Why 2-SAT is in P but 3-SAT is NP-complete.
2-SAT is in NL via NL = coNL. UNSAT is in NL (Immerman–Szelepcsényi). Both 2-SAT and ¬2-SAT in NL.
SAT-decision and SAT-search coincide for 2-SAT. Both are in P (and NL); the deterministic algorithm gives an assignment, not just yes/no.

🔊 Listen

4 · Q&A defence notes

Q1. Why does 2-SAT have a smart algorithm but not 3-SAT?
A 2-clause (a ∨ b) decomposes into exactly two implications: ¬a → b and ¬b → a. The implication structure is finite-tree-like. A 3-clause (a ∨ b ∨ c) has 3 × 2 = 6 partial implications that don't combine cleanly. The graph trick breaks down.
Q2. Why NL and not L?
PATH in the implication graph is checked nondeterministically (Problem 42). If we could check directed graph PATH in L, then L = NL — currently open.
Q3. Is 2-SAT in P?
Yes — via SCC computation in O(V + E) using Tarjan or Kosaraju. The SCC algorithm gives both decision and assignment. NL ⊆ P, consistent with 2-SAT ∈ NL.
Q4. What about Horn-SAT?
Horn-SAT (clauses with at most one positive literal) is also in P, by unit propagation. Linear-time. Both 2-SAT and Horn-SAT are "easy SAT" cases below the NP-complete general SAT.

🔊 Listen

5 · Where to read more

Sipser: §8.4 (NL). Lecture notes: Module 7 slide 2. Companion problems: P22 (SAT), P42 (PATH NL), P44 (NL = coNL).