vi. Satisfiability

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.

Proof: Horn-SAT and XOR-SAT are polynomial

Horn-SAT. Every clause has at most one positive literal, so each clause is either a pure negative clause ($\neg a\vee \neg b\vee \dots$, i.e. “not all of these”) or an implication $a_1\wedge a_2\wedge \cdots \Rightarrow b$ (rewriting the single positive literal $b$ and negated literals as a conjunction of premises). Unit propagation — repeatedly finding a clause whose premises are all already satisfied and forcing its conclusion — can only set variables to true (never needs to guess), so it runs to a unique fixed point in $O(nm)$ (or $O(n+m)$ with a counter-based queue); the formula is satisfiable iff this fixed point violates no purely negative clause, since the fixed point is the minimal model (setting as few variables true as forced) and if any model exists, the minimal one — a subset of any other satisfying assignment’s true variables — also satisfies every clause (a Horn clause with extra false premises or an already-true conclusion stays satisfied when fewer variables are set true).
XOR-SAT. Each clause $x_1\oplus x_2\oplus \cdots =c$ (or derived from $\vee$/$\wedge$ structure restricted to parity constraints) is a linear equation over ${\mathbb{F}}_2$. The whole formula is a linear system, solvable (or shown inconsistent) by Gaussian elimination in $O(n{m}^2/64)$ with bitset rows — satisfiability is exactly solvability of the linear system, a standard fact of linear algebra over any field. $■$

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, the full correctness proof, 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)$.

Proof: the at-most-one prefix encoding

The clauses force $p_i$ to be true whenever any of $x_1,\dots ,x_i$ is true: $x_i\Rightarrow p_i$ handles $x_i$ itself, and $p_{i-1}\Rightarrow p_i$ propagates it forward once set, so by induction $p_i⟺$ “some $x_j$, $j\le i$, is true” is forced in the "$\Leftarrow$" direction by these two clause families (a satisfying assignment with some earlier $x_j$ true must set every $p_i$ for $i\ge j$ true, since the implications chain forward). The third clause $p_{i-1}\Rightarrow \neg x_i$ then says: if some earlier variable was already true (forcing $p_{i-1}$ true), $x_i$ cannot also be true — directly preventing two variables from being simultaneously true, since the later one’s clause fires against the earlier one’s already-forced $p$. Together these $3(k-1)$ clauses (roughly) enforce “at most one of $x_1,\dots ,x_k$ is true” using $O(k)$ clauses and $O(k)$ auxiliary variables, instead of the $\left(\genfrac{}{}{0ex}{}{k}{2}\right)=O(k^2)$ pairwise clauses $(\neg x_i\vee \neg x_j)$ needed without the prefix trick. $■$

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.

Proof: the binary search is valid

Binary search requires the feasibility predicate (“can every pair be placed with separation $\ge d$?”) to be monotone in $d$: if $d_1<d_2$ and separation $d_2$ is achievable, then $d_1$ is too, using the same assignment (every pair that was at least $d_2$ apart is automatically at least $d_1$ apart). So the set of feasible $d$ is a prefix $[0,d^{\ast }]$ for some threshold $d^{\ast }$, and binary search finds $d^{\ast }$ in $O(\log C)$ feasibility checks, each an $O(n^2)$ clause-construction plus an $O(n^2)$ 2-SAT solve. $■$

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.