Algorithms / Two Sat

Least You Need to Know: 2-SAT, Implication Graphs, and SCC-Based Solving

2-SAT is a special satisfiability problem where each clause has two literals. Unlike general SAT, 2-SAT is solvable in polynomial time using an implication graph and strongly connected components. The signature theorem is that a formula is unsatisfiable exactly when some variable and its negation lie in the same SCC.

The least you need to know

A 2-SAT instance has clauses of size two, such as `(a or b)`.
Each clause `(a or b)` is encoded by implications `not a -> b` and `not b -> a`.
The implication graph has one vertex for each literal.
A 2-SAT instance is unsatisfiable iff some variable and its negation are in the same SCC.
2-SAT is polynomial-time solvable even though general SAT is believed hard.

Key notation

2-SAT SAT where every clause has exactly two literals in the standard model

implication graph directed graph of literal implications

SCC strongly connected component

Tiny worked example

For a clause `(x or y)`, add edges `(not x -> y)` and `(not y -> x)`.
Build the implication graph for all clauses.
Compute strongly connected components.
If `x` and `not x` fall in the same SCC for some variable `x`, the formula is unsatisfiable.

Common mistakes

Students often overgeneralize 2-SAT techniques to arbitrary CNF formulas.
The SCC criterion is exact and algorithmic, not just a heuristic.
Implication graphs are directed; strongly connectedness matters.

How to recognize this kind of problem

Every clause has two literals.
The prompt suggests implications between choosing one literal and forcing another.
SCC-based reasoning or contradiction cycles are central.