SAT and 2-SAT

Given a boolean formula in conjunctive normal form, is there an assignment making it true?

$(x_1\vee \neg x_2\vee x_3)\wedge (\neg x_1\vee x_4)\wedge \dots$

The complexity cliff

Clause size	Complexity
1-SAT (unit clauses)	trivial
2-SAT	P — $O(n+m)$ via SCC
3-SAT	NP-complete
$k$-SAT, $k\ge 3$	NP-complete
Horn-SAT (≤1 positive literal per clause)	P — unit propagation
XOR-SAT	P — Gaussian elimination over $\mathbb{F}_2$
MAX-2-SAT (maximise satisfied clauses)	NP-hard

The jump from 2 to 3 is the sharpest boundary in complexity theory, and Horn-SAT and XOR-SAT are the other two tractable fragments worth recognising.

2-SAT — the algorithm

A clause $(a\vee b)$ is two implications: $\neg a\Rightarrow b$ and $\neg b\Rightarrow a$. Build the implication graph on $2n$ literal vertices, then:

Satisfiable iff no variable has $x$ and $\neg x$ in the same SCC.

Assignment: set $x$ true iff $\mathrm{comp}[x]$ is later in topological order than $\mathrm{comp}[\neg x]$.

$O(n+m)$. See 2-SAT for the code and encoding recipes.

Encoding constraints

Constraint	Clauses
$a$ true	$(a\vee a)$
$a\Rightarrow b$	$(\neg a\vee b)$
$a=b$	$(\neg a\vee b)\wedge (a\vee \neg b)$
$a\ne b$	$(a\vee b)\wedge (\neg a\vee \neg b)$
At most one of $a,b$	$(\neg a\vee \neg b)$
At most one of $x_1..x_k$	pairwise ($O(k^2)$), or prefix-OR encoding ($O(k)$)
Exactly one of $x_1..x_k$	at-most-one + $(x_1\vee \cdots \vee x_k)$ — the last needs $k\ge 3$, so not 2-SAT

The at-most-one prefix encoding: introduce $p_i$ = “some $x_j$ with $j\le i$ is true”, with clauses $x_i\Rightarrow p_i$, $p_{i-1}\Rightarrow p_i$, $p_{i-1}\Rightarrow \neg x_i$. $O(k)$ clauses instead of $O(k^2)$.

The binary-search pattern

2-SAT decides feasibility, so pair it with a binary search to optimise:

“Place $n$ objects, each in one of two positions, maximising the minimum separation.”

Binary search the separation $d$; for each $d$, add a clause $(\neg a\vee \neg b)$ for every pair of placements closer than $d$; test satisfiability. $O(n^2\log C)$.

This combination is one of the most recognisable 2-SAT problem shapes in contests.

General SAT solving

Modern CDCL (conflict-driven clause learning) solvers routinely handle industrial instances with millions of variables, despite NP-completeness. The core ingredients:

Technique	Idea
Unit propagation	a clause with one unassigned literal forces it
Clause learning	on conflict, derive and add a new clause explaining it
Non-chronological backjumping	jump back past irrelevant decisions
VSIDS branching	prefer variables appearing in recent conflicts
Watched literals	propagate without scanning every clause
Restarts	escape bad search regions, keeping learned clauses

Not a contest tool, but the reason “NP-complete” does not mean “hopeless in practice”.

DPLL — the simple version

bool dpll(Formula& f) {
    unitPropagate(f);                                   // forced assignments
    pureLiteralElimination(f);                          // literals of one polarity
    if (f.empty()) return true;                         // all clauses satisfied
    if (f.hasEmptyClause()) return false;               // conflict
    int v = chooseVariable(f);
    return dpll(f.assign(v, true)) || dpll(f.assign(v, false));
}

Unit propagation does most of the work: a clause with a single unassigned literal forces its value, which may cascade. Implementing just DPLL with unit propagation solves surprisingly large instances.

What to use when

Problem	Method
Two choices per object, pairwise conflicts	2-SAT
Optimising with a monotone threshold	binary search + 2-SAT
Implication chains only	Horn-SAT / unit propagation
XOR constraints	$\mathbb{F}_2$ Gaussian elimination
Small $n$, general constraints	backtracking with propagation
Exact cover structure	Dancing Links
Maximise satisfied clauses	SDP or local search
Genuinely need general SAT	there is probably a better formulation

If a contest problem seems to need general SAT, look again — the intended solution is almost always 2-SAT, flow, matching, or a DP.

See also: 2-SAT · NP-Completeness · Backtracking