3-SAT Reduction, in depth: proving SAT reduces to 3-SAT by clause splitting, witness mapping both ways, a brute-force test and the restricted variants that stay hard

Definitions: what must be preserved

A literal is a variable or its negation. A clause is an OR of literals, and a CNF formula is an AND of clauses. An instance of CNF-SAT is any CNF formula, with clauses of any length; 3-SAT restricts every clause to at most three literals. Some texts require exactly three, which is no harder to reach, as shown below. A reduction from SAT to 3-SAT is a polynomial-time function f that maps a formula F to a 3-CNF formula f(F) such that F is satisfiable if and only if f(F) is. The two formulas need not be equivalent, because f(F) has extra variables; they need only be equisatisfiable, and for practical use we also want to translate satisfying assignments both ways.

Input in CNF is assumed. If your formula is an arbitrary circuit or expression, convert it with the Tseitin transformation first, as described in SAT solving, in depth; distributing OR over AND instead can blow the formula up exponentially and the reduction would no longer be polynomial.

The construction and its proof

Handle each clause independently, with fresh variables that belong to that clause alone. Let the clause have k literals.

The padding rows only matter if you want exactly three literals per clause. They work because the four (or two) clauses together cover every assignment of the fresh variables, so they are all satisfied exactly when the original literals are. With at-most-three semantics you can keep short clauses unchanged.

The chain for long clauses is the heart of the proof. If the original clause is satisfied, pick a true literal li. Set every y before it, y1 to y(i-2), true, and every y from y(i-1) on false. Each clause to the left of li is satisfied by its positive y, the clause containing li is satisfied by li, and each clause to the right is satisfied by its negated y. If every li is false, the head clause forces y1 true, the next clause then forces y2 true, and so on, until the tail clause needs ¬y(k-3), which is false. So no assignment of the fresh variables satisfies the chain. Clauses do not share fresh variables, so the argument applies to each clause separately and the formula is satisfiable exactly when the original is.

Size: a clause of length k becomes k - 2 clauses of length 3, so the output has at most 3 times as many literal occurrences as the input plus a constant per clause. The reduction is linear time, which is better than polynomial.

Diagram

Code and a brute-force test

Represent literals as nonzero integers in the DIMACS style: 3 means x3 and -3 means ¬x3. The function returns the new clauses and the number of variables, and keeps the original variables at their original numbers so a witness maps back by truncation.

from itertools import product

def sat_to_3sat(clauses, n):
    out, nxt = [], n + 1
    def fresh():
        nonlocal nxt
        nxt += 1
        return nxt - 1
    for cl in clauses:
        cl = list(dict.fromkeys(cl))                 # drop duplicate literals
        if any(-l in cl for l in cl):
            continue                                 # tautology: always true
        k = len(cl)
        if k == 0:
            return [[]], n                           # empty clause: unsatisfiable
        if k <= 3:
            out.append(cl)
            continue
        y = fresh()
        out.append([cl[0], cl[1], y])
        for lit in cl[2:-2]:
            y2 = fresh()
            out.append([-y, lit, y2])
            y = y2
        out.append([-y, cl[-2], cl[-1]])
    return out, nxt - 1

def satisfies(clauses, a):                           # a[v] is True/False, 1-indexed
    return all(any(a[abs(l)] == (l > 0) for l in cl) for cl in clauses)

def brute(clauses, n):
    for bits in product([False, True], repeat=n):
        a = (None,) + bits
        if satisfies(clauses, a):
            return a
    return None

def extend_witness(clauses, n, a):
    """Forward map: a witness of F -> a witness of f(F), in one linear pass."""
    out, m = sat_to_3sat(clauses, n)
    b = list(a) + [False] * (m - n)
    for cl in out:                                   # chain order: head, middles, tail
        if cl and cl[-1] > n:                        # clause ends in a fresh link y
            b[cl[-1]] = not any(b[abs(l)] == (l > 0) for l in cl[:-1])
    return tuple(b)

The test is the proof's two directions made executable: for random small formulas, the original is satisfiable exactly when the output is, a witness of the output truncated to the first n variables satisfies the original, and every witness of the original extends to the output.

import random
for trial in range(2000):
    n = random.randint(1, 6)
    F = [[random.choice([1, -1]) * random.randint(1, n) for _ in range(random.randint(1, 7))]
         for _ in range(random.randint(1, 6))]
    G, m = sat_to_3sat(F, n)
    assert all(len(cl) <= 3 for cl in G)
    wf, wg = brute(F, n), brute(G, m)
    assert (wf is None) == (wg is None)
    if wg is not None:
        assert satisfies(F, wg[: n + 1])             # backward map: truncate
        assert satisfies(G, extend_witness(F, n, wf))  # forward map: extend
print("ok")

The forward map keeps each link y true for as long as no true original literal has been seen along its chain, then false from the first true literal on, which is exactly the assignment used in the proof. The brute-force side of the test does not rely on that argument, so a wrong rule makes the assertion fail rather than pass silently.

Worked example

Take F = (x1 ∨ x2 ∨ x3 ∨ x4 ∨ x5) ∧ (¬x1 ∨ x2) ∧ (¬x2). The first clause has k = 5, so it becomes three clauses with fresh y1 = x6 and y2 = x7: (x1 ∨ x2 ∨ x6), (¬x6 ∨ x3 ∨ x7), (¬x7 ∨ x4 ∨ x5). The two short clauses pass through. The output has 5 clauses over 7 variables.

F is satisfiable: ¬x2 forces x2 false, then ¬x1 ∨ x2 forces x1 false, and x4 true satisfies the long clause. Mapping forward, the true literal x4 sits at position i = 4, so y1 and y2 are both true: (x1 ∨ x2 ∨ x6) holds by x6, (¬x6 ∨ x3 ∨ x7) by x7, and (¬x7 ∨ x4 ∨ x5) by x4. Had only x3 been true instead, y1 would be true and y2 false, and the tail would hold by ¬x7. Mapping backward, drop x6 and x7.

Now check the unsatisfiable direction on the long clause alone. If x1 to x5 are all false, (x1 ∨ x2 ∨ x6) forces x6 true, then (¬x6 ∨ x3 ∨ x7) forces x7 true, and (¬x7 ∨ x4 ∨ x5) has three false literals. No choice of x6 and x7 escapes, which is the chain argument in miniature. Running the code on F produces exactly these five clauses with the fresh variables numbered 6 and 7.

Why the trick stops at three

Why stop at three? A chain clause needs one original literal plus a link in and a link out, which is three literals; with two there is no room for the literal. That is not just a failure of this construction: 2-SAT is solvable in linear time with an implication graph and strongly connected components, as shown in 2-SAT, in depth, so a polynomial reduction from 3-SAT to 2-SAT would prove P = NP. The optimisation version MAX-2-SAT, which asks for the most satisfied clauses, is NP-hard, which shows how thin the line is.

Restricted variants that stay hard

Reductions out of 3-SAT get shorter when the source is more restricted, so it pays to know which restrictions stay hard.

To reduce the occurrence count, the usual step replaces a variable appearing m times by m copies linked in a cycle of implications, x1 implies x2 implies ... implies x1, which uses two-literal clauses; that is why Tovey's hard version allows clauses of size two.

Using 3-SAT as a source

A reduction from 3-SAT to a target problem almost always has three parts: a variable gadget with exactly two good states (true and false), a clause gadget that is satisfied only if at least one of its three connected literals is in the true state, and a budget or threshold that prevents cheating. The Independent Set and CLIQUE reductions on this site, in Clique NP-hardness reduction, are clean examples. Write the backward direction first: assume a solution to the target and show how to read off an assignment, because that is where proofs usually break.

Failure modes

• Sharing fresh variables between clauses, which lets one clause's chain satisfy another and breaks the proof.
• Forgetting tautological or duplicate-literal clauses, which produce clauses like (x ∨ ¬x ∨ y) that a target gadget may not expect.
• Starting from a non-CNF formula and distributing, which makes the reduction exponential.
• Proving only the forward direction; equisatisfiability needs both.
• Using a restricted variant that is actually easy, as Tovey's exactly-three, at-most-three case shows.
• Feeding the 3-CNF output to a real solver: modern solvers handle long clauses natively and the extra variables usually slow them down.

Trade-offs

The reduction exists for proofs, not for solving. In practice you encode problems directly into CNF and hand them to a CDCL solver; splitting long clauses only adds variables and weakens propagation. Where 3-CNF does matter in practice is benchmarking: random 3-SAT near 4.26 clauses per variable is the standard hard distribution, discussed in NP-complete problems, in depth.

What to do next

1. Type in the reduction and the test above and run it until it prints ok; then break it by sharing one fresh variable across clauses and watch the test fail.
2. Replace the brute-force forward map with the direct chain rule and test it the same way.
3. Add the padding rules so every output clause has exactly three distinct literals.
4. Implement the occurrence-reduction step and check that no variable appears more than three times.
5. Pick one target problem, write its variable and clause gadgets, and prove the backward direction first.
6. Write a DIMACS writer and confirm a real solver gives the same answers as your brute force on small cases.