Why Three Literals Is the Pivot for Satisfiability

The satisfiability problem is NP-complete when clauses are allowed to contain three literals, and solvable in linear time when they contain at most two. The gap between two and three is the sharpest phase transition in the subject, and it is not a matter of degree: 2-SAT has a decision algorithm whose running time is proportional to the number of clauses plus the number of variables, while 3-SAT is the canonical complete problem from which everything else is reduced, starting with the direct tableau encoding. The mechanism behind the gap is worth understanding in detail, because it explains why the general CNF problem can be reduced to 3-SAT at all, and why the same reduction cannot push down to 2-SAT.

The reduction from long clauses

A clause with $k > 3$ literals can be replaced by a chain of clauses with three literals each, at the cost of introducing $k - 3$ fresh variables. The construction is a Tseitin-style transformation applied to a single clause, and it works by making the fresh variables assert “the remaining suffix of this clause is satisfied”.

For a clause $(l_1 \vee l_2 \vee \cdots \vee l_k)$, introduce fresh variables $y_1, \dots, y_{k-3}$ and write:

$$(l_1 \vee l_2 \vee y_1) \wedge (\neg y_1 \vee l_3 \vee y_2) \wedge \cdots \wedge (\neg y_{k-4} \vee l_{k-2} \vee y_{k-3}) \wedge (\neg y_{k-3} \vee l_{k-1} \vee l_k).$$

The two directions are checked by following the chain. If some $l_i$ is true, set $y_j$ true for all $j < i-1$ and false for all $j \ge i-1$: each clause then has a true literal. If no $l_i$ is true, the first clause forces $y_1$ true, the second forces $y_2$ true, and induction forces every $y_j$ true, at which point the last clause is $(\neg y_{k-3} \vee l_{k-1} \vee l_k)$ with $y_{k-3}$ true and both remaining literals false, so it is unsatisfied.

The important property is that the transformation is equisatisfiable rather than equivalent. The new formula has more variables, and it is satisfiable exactly when the old one is, but a satisfying assignment to the old formula does not extend uniquely: the $y$ variables can be set in several ways. For NP-completeness that is enough, because only the existence of a satisfying assignment matters. For applications that count solutions, or that need a correspondence between assignments and models, the loss of uniqueness is a real cost and the transformation has to be modified.

The clause count grows from one to $k - 2$, and the variable count grows by $k - 3$. Since $k$ is bounded by the input length, the transformation is polynomial in the formula size, and it can be applied clause by clause. The resulting formula is in 3-CNF, and the whole reduction runs in linear time in the size of the input formula.

Why two literals is different

The same chain construction fails at $k = 2$, and the failure is structural rather than incidental. A clause with two literals is a binary constraint: it forbids exactly one combination of its two variables. A clause with three literals forbids one combination of three variables, which is a constraint of a different kind: it can encode a disjunction that is not expressible as a conjunction of binary constraints.

The linear-time algorithm for 2-SAT makes the difference concrete. Given a 2-CNF formula, construct an implication graph with two nodes per variable, one for each literal. A clause $(a \vee b)$ contributes two directed edges: $\neg a \to b$ and $\neg b \to a$. The formula is unsatisfiable exactly when some variable and its negation lie in the same strongly connected component, because then the implications force $x \to \neg x$ and $\neg x \to x$ simultaneously, and no assignment can satisfy both.

def two_sat_unsatisfiable(clauses, n):
    # nodes 2*v and 2*v+1 represent x_v and ¬x_v
    graph = [[] for _ in range(2 * n)]
    for a, b in clauses:
        graph[a ^ 1].append(b)   # ¬a -> b
        graph[b ^ 1].append(a)   # ¬b -> a
    comp = strongly_connected_components(graph)   # Kosaraju or Tarjan
    return any(comp[2 * v] == comp[2 * v + 1] for v in range(n))

The algorithm runs in time linear in the number of nodes plus edges, which is linear in the formula size. The reason it works is that implications compose: if $a$ forces $b$ and $b$ forces $c$, then $a$ forces $c$, and the transitive closure is captured by reachability in the graph. A three-literal clause does not decompose into implications of this kind. The clause $(a \vee b \vee c)$ forbids the single assignment where all three are false; expressing that as implications requires a hypergraph reachability notion, and hypergraph reachability with edges of size three is exactly the kind of problem that 2-SAT’s linear algorithm cannot handle.

Clause width	Constraint arity	Decision complexity
1	unary	linear, by unit propagation
2	binary	linear, by implication graph reachability
3	ternary	NP-complete
$k \ge 3$	$k$-ary	NP-complete, reducible to width 3

The table is the whole story in one place: the complexity jumps between width 2 and width 3 and never jumps again.

What 3-SAT’s completeness buys

The reduction from CNF to 3-CNF is what makes 3-SAT the standard starting point for gadget constructions. A gadget is easier to design when the constraint it must encode is uniform, and 3-CNF gives a uniform constraint: exactly three literals, no more and no fewer. Every NP-completeness proof that begins “reduce from 3-SAT” relies on this uniformity, and the reductions in the many-one reduction machinery are written that way for the same reason.

The cost of uniformity is the auxiliary variables. A reduction from 3-SAT to, say, graph colouring must handle formulas with auxiliary variables that have no meaning in the target problem, and the gadget has to allow them to take any value consistent with the clauses. This is usually handled by making the gadget’s constraints local, so that the auxiliary variables correspond to internal choices in the gadget rather than to global ones.

There is a second, subtler consequence. Because the transformation is equisatisfiable and not equivalence-preserving, a reduction that composes two such transformations does not compose their solution counts. If the target problem’s solutions are supposed to correspond to the source formula’s satisfying assignments, the chain of transformations breaks the correspondence, and the reduction has to be rebuilt to preserve it. Problems defined in terms of counting models, such as #SAT, are not NP-complete in the same sense; they are complete for counting classes, and the reductions between them must be parsimonious.

Random 3-SAT and the satisfiability threshold

The clause width also determines the shape of the solution space, and this is where the theory meets the behaviour of actual solvers. For random 3-CNF formulas with $n$ variables and $m$ clauses, chosen uniformly, there is a ratio $m/n$ below which formulas are almost surely satisfiable and above which they are almost surely unsatisfiable. The transition sharpens as $n$ grows. For 3-SAT the critical ratio is approximately 4.26, a value established by statistical-physics methods and confirmed by careful numerical work; for 2-SAT the corresponding threshold is exactly 1, and it can be proved rigorously by the implication-graph argument.

The existence of a threshold is not a complexity statement, and it does not contradict NP-completeness: the hardest instances for a solver tend to sit near the threshold, where both satisfiable and unsatisfiable formulas are common and local reasoning gives little guidance. What the threshold shows is that “random 3-SAT” is not a uniform difficulty class. Far below the threshold, formulas are satisfiable and easy to satisfy by greedy assignment; far above, they are unsatisfiable and easy to refute by counting arguments. The hard region is narrow.

For 2-SAT no such hard region exists in the same sense, because the linear-time algorithm does not care about the ratio. This is another way of seeing that the classes differ: an algorithm that runs in linear time on every instance has no threshold behaviour to exhibit.

The encoding conventions that matter in practice

The DIMACS CNF format, used by satisfiability solvers and competitions, encodes a formula as a header line p cnf <variables> <clauses> followed by one clause per line, each a sequence of non-zero integers terminated by 0, with positive integers for positive literals and negative for negated ones. A clause spanning several lines is legal, and so is a clause on a single line with other clauses, since the terminator is the only separator.

Two conventions in that format have consequences for reductions. Variables are numbered from 1, so a reduction that introduces fresh variables must renumber them to avoid collisions with the source formula’s variables. And the format requires the clause count in the header to match the actual number of clauses, which means a reduction that emits clauses incrementally must buffer them or count them in a first pass.

The width-3 restriction is not part of the format; a DIMACS file may contain clauses of any width, and solvers generally handle them by treating a long clause as a constraint to be watched rather than by expanding it. The expansion to 3-CNF is a theoretical device for reductions, not a preprocessing step that solvers perform, because the auxiliary variables can make the instance larger and sometimes harder.

Where the boundary actually sits

The jump from 2 to 3 is not the only boundary of this kind. Satisfiability with clauses of width 3 is complete, and so is the restricted version in which each variable occurs in at most three clauses. Restricting further does not always preserve completeness: the monotone version, in which no literal is negated, is trivially satisfiable when every clause is a disjunction of positive literals, since setting every variable true satisfies all clauses. The monotone variant that is complete requires a different condition per clause, such as exactly one true literal among the three, and that variant does not reduce to the plain monotone problem in any obvious way. Each such restriction needs its own gadget, usually one that simulates negation or fixes occurrence counts without changing satisfiability.

The boundary that does lower complexity is the one at width 2, and it is exact: 2-SAT is in NL, and it is complete for NL under the appropriate reductions, so it sits strictly below NP unless the classes collapse. The exact characterisation of which constraint languages give polynomial-time satisfiability is Schaefer’s dichotomy theorem: every constraint language over the boolean domain is either tractable, and then the problem is in P, or NP-complete, and there is no intermediate case. Clause width is one way to slice that space, and it happens to slice it at exactly the point where the implication-graph algorithm stops working.