skip to content

The formula Cook-Levin builds has long clauses; how do you shrink them to three literals without changing satisfiability?

level: seniorimportance: should knowfreq 38%

answer

  1. chain the clause together
  2. fresh variables link the pieces
  3. k literals, k minus two clauses
  4. all false forces the chain true
  5. satisfiability preserved, not equivalence

basics

~20 s

Chain the clause through fresh variables: a clause of k literals becomes k-2 three-literal clauses linked by k-3 new variables. Every solution of the original extends to one of the rewrite, and every solution of the rewrite restricts back.

solid answer

~40 s

Take a clause of `k` literals with `k` above three and split it along a chain of brand-new variables `y1 ... y(k-3)`: emit `(L1 or L2 or y1)`, then `(not y(i-2) or Li or y(i-1))` for the middle literals, and finally `(not y(k-3) or L(k-1) or Lk)`. That is `k-2` clauses using `k-3` fresh variables. If some original literal is true, set the chain variables before it to true and the rest to false and every clause holds; if all the originals are false, the first clause forces `y1` true, which forces `y2` true, and so on until the last clause has nothing left to satisfy it. The rewrite is therefore **satisfiability-preserving**, not an equivalence - it has variables the original does not - and it grows the formula only linearly.

code

pseudocode · 9 lines
pseudocode
split(clause L[1..k], fresh):
    if k <= 3:
        return pad_to_three(clause, fresh)     // 2 literals -> 2 clauses, 1 fresh
    y := fresh.take(k - 3)                     // brand-new, used by this clause only
    out := [ (L[1] OR L[2] OR y[1]) ]
    for i := 3 to k - 2:
        out.append( (NOT y[i-2] OR L[i] OR y[i-1]) )
    out.append( (NOT y[k-3] OR L[k-1] OR L[k]) )
    return out                                 // k - 2 clauses, k - 3 fresh variables

go deeper

for a junior

Know that the raw formula has clauses of all widths and that a standard rewrite turns them into three-literal clauses without changing the yes or no answer.

for a middle

Be able to write the chain: first two literals plus a new variable, one clause per middle literal, and the last two literals closing the chain. Say why the counts come out as they do.

for a senior

Argue both directions, including the case where every original literal is false and the chain forces itself into contradiction, and be precise that this preserves satisfiability rather than producing an equivalent formula.

for a principal

Recognise the pattern: introducing auxiliary variables to flatten a wide constraint into narrow ones, at linear cost, is a standard modelling move whenever a target form has a fixed arity.

## Why the shrink is needed at all The formula that comes out of the tableau construction is in conjunctive normal form, but its clauses have no fixed width: the clause saying *an accepting marker appears somewhere* runs over the whole grid, and a window clause expands into a disjunction over every legal pattern. Plenty of later hardness arguments are far easier to state against a clause set where **every clause has exactly three literals**, so the standard next move after the theorem is to convert the formula into that shape. The conversion must be cheap - polynomial time - and it must not change the yes/no answer. ## The chain construction For a clause `(L1 or L2 or ... or Lk)` with `k` greater than three, introduce fresh variables `y1 ... y(k-3)` used by **this clause only**, and emit: - `(L1 or L2 or y1)` - `(not y1 or L3 or y2)`, `(not y2 or L4 or y3)`, ... one per middle literal - `(not y(k-3) or L(k-1) or Lk)` Walk `k = 5` by hand: you get `(L1 or L2 or y1)`, `(not y1 or L3 or y2)`, `(not y2 or L4 or L5)` - three clauses, two fresh variables. In general the counts are: | Original clause width | Clauses produced | Fresh variables | |---|---|---| | 1 | 4 | 2 | | 2 | 2 | 1 | | 3 | 1 | 0 | | k above 3 | k - 2 | k - 3 | ## Why satisfiability is preserved, in both directions 1. **Original satisfied implies rewrite satisfied.** Suppose literal `Li` is true. Set `y1 ... y(i-2)` to true and every later chain variable to false. Each clause before the one containing `Li` is satisfied by its own positive chain variable; the clause containing `Li` is satisfied by `Li`; each clause after it is satisfied by its negated chain variable, which is false and therefore appears as a true literal. Every clause holds. 2. **Rewrite satisfied implies original satisfied.** Contrapositive: suppose every `Li` is false. The first clause then forces `y1` true; the next forces `y2` true; inductively every chain variable is forced true; and the last clause `(not y(k-3) or L(k-1) or Lk)` has all three literals false. So the rewrite is unsatisfiable whenever the original clause cannot be satisfied. Together these say the rewritten set is satisfiable exactly when the original is, and moreover any solution of the rewrite, restricted to the original variables, satisfies the original. That is stronger than bare equisatisfiability and weaker than logical equivalence - the two formulas cannot be equivalent, because one of them has variables the other has never heard of. ## Two details that are easy to get wrong - **The fresh variables must be fresh per clause.** Reusing one chain across two long clauses couples them: a chain variable forced true by one clause would leak in as a satisfied or falsified literal in the other, and the two-way argument above collapses. - **Short clauses need padding only if the target form insists on exactly three literals.** Some statements of the problem allow *at most* three, in which case a one- or two-literal clause is already legal. Where exactly three is required, pad with fresh variables: a two-literal clause `(L1 or L2)` becomes `(L1 or L2 or p)` and `(L1 or L2 or not p)`; a one-literal clause `(L1)` becomes the four clauses over fresh `p`, `q` covering all four sign combinations. Both are satisfiable precisely when the original literal set is. ## Cost, and why the shrink stops at three Each original literal contributes a bounded number of new literals, so the total size grows **linearly** in the size of the input formula - nothing here threatens the polynomial bound the reduction needs. Combined with the tableau construction, this gives a polynomial-time mapping from any language in NP into three-literal satisfiability, which is why the three-literal form is the usual starting point for later hardness proofs rather than the raw formula the theorem produces. The chain cannot be pushed one step further, down to two literals per clause. Satisfiability of two-literal clause sets is decidable in polynomial time, so a satisfiability-preserving polynomial rewrite into that form would put every language in NP into P and settle an open question. Three is therefore not an arbitrary convention but the narrowest clause width the construction can reach without proving something nobody has proved.

  • What happens if the same fresh variables are reused across two different long clauses?
    The two clauses become coupled and the argument breaks. A chain variable forced true by one clause appears as a false negated literal in the other, so an assignment satisfying the original formula may no longer extend. Each long clause needs its own private chain.
  • How do you handle a clause that has only one literal?
    Pad it if the target form demands exactly three literals: with two fresh variables `p` and `q`, emit the four clauses that pair the literal with every sign combination of `p` and `q`. Whatever `p` and `q` are set to, one of those clauses can only be satisfied by the original literal.
  • Does the rewrite risk blowing the formula up?
    No. Every original literal contributes a bounded number of new literals, so the rewritten formula is linear in the size of the original. The polynomial bound the reduction depends on survives comfortably, which is why the conversion is treated as a routine post-processing step.

saying these in an interview costs you the question

  • Says the rewritten clauses are logically equivalent, ignoring the fresh variables.
  • Believes the split can blow the formula up exponentially.
  • Thinks the same fresh variables can be shared across different long clauses.
  • Claims the rewrite can turn an unsatisfiable formula into a satisfiable one.
  • Assumes a one-literal clause needs no padding under an exactly-three convention.