The Complexity of Theorem-Proving Procedures

How to read the original

1. Read Tautologies and Polynomial Re-Reducibility and note that the paper defines an oracle-based reduction.
2. Follow Theorem 1’s computation encoding before translating the result into modern SAT terminology.
3. Distinguish a polynomial-size encoding, a polynomial verifier, and an efficient algorithm for finding a satisfying assignment.

Read the historical reduction correctly

Cook’s paper connects polynomially bounded nondeterministic computation with propositional reasoning. Its original presentation uses tautologies and an oracle-style notion of reducibility. Modern courses commonly present the Cook-Levin theorem as SAT being complete for NP under polynomial-time many-one reductions. These are related formulations, but one should not silently replace the original definitions or call tautology NP-complete under the modern many-one convention without qualification.

The central mechanism is to describe an accepting computation by a finite collection of Boolean constraints. A satisfying assignment acts as a witness that the local conditions fit together. The important bound is that the representation grows polynomially with the bounded computation, not that a particular solver happens to finish one example quickly.

Encode a small object before a whole machine

Use an original graph-coloring example. For each vertex v and each color r,g,b, introduce a Boolean variable X(v,color). Require at least one color with the clause X(v,r) OR X(v,g) OR X(v,b). Require at most one color with the three pairwise clauses NOT X(v,r) OR NOT X(v,g), and the corresponding pairs. For each edge (u,v) and each color c, add NOT X(u,c) OR NOT X(v,c).

For a triangle with vertices A,B,C, an assignment choosing A red, B green, and C blue satisfies every clause. An assignment making A and B both red violates the red clause for edge AB. The formula encodes the specification, not the search strategy. A verifier simply checks clauses once a proposed assignment is supplied.

There are three variables per vertex, four vertex clauses per vertex, and three edge clauses per edge. With three fixed colors, both formula size and construction time are polynomial in the graph representation. If the encoding duplicated a huge search tree, it might preserve the answer but fail the efficient-reduction requirement.

Explain both directions

If a proper coloring exists, set exactly its chosen color variable true at each vertex. The vertex and edge constraints all hold. Conversely, a satisfying assignment selects exactly one color per vertex, and no edge has equal selected colors at both endpoints. It therefore describes a proper coloring. Both implications are necessary; an encoding allowing every variable to be false would satisfy only the at-most-one and edge clauses without describing any coloring.

The computation-tableau idea applies similar discipline to time, tape position, symbols, and machine state. Constraints specify a valid initial configuration, legal local transitions, and acceptance within the bound. Local consistency must be designed so it implies one coherent global accepting history. That is the proof burden behind the memorable completeness statement.

Keep complexity claims bounded

NP means that yes instances have polynomial-length certificates verifiable in polynomial time under the usual formulation. It does not mean not polynomial. A polynomial algorithm for SAT would yield polynomial algorithms for all NP decision problems; the theorem does not prove that no such algorithm exists. Worst-case classification also does not imply every instance is difficult.

SAT and tautology are different decision questions. A formula is satisfiable when some assignment makes it true; it is a tautology when every assignment does. Negation connects satisfiability with failure of tautology, but complementing an oracle answer differs from an ordinary yes-preserving many-one reduction. Keeping that distinction visible makes the original paper more instructive and prevents a historically important theorem from becoming an inaccurate slogan.

Reconstruction exercise

Encode two-colorability of a three-vertex path A-B-C using variables for red and blue. List the at-least-one, at-most-one, and edge constraints. Give one satisfying assignment, then add edge AC and prove no assignment can satisfy the resulting formula. Count variables and clauses for a general graph with n vertices and m edges. Explain why showing a fast verifier for this encoding does not itself show a polynomial-time algorithm for every graph-coloring variant.

Worked solution

For each vertex v use variables Rv and Bv, clauses (Rv OR Bv) and (NOT Rv OR NOT Bv). For each edge uv add (NOT Ru OR NOT Rv) and (NOT Bu OR NOT Bv). The path is satisfied by A red, B blue, C red. Adding AC forbids the equal red endpoints. More generally, if A and B differ and B and C differ with only two colors, A and C must agree, so the triangle is impossible. The encoding has 2n variables and 2n+2m clauses, hence linear size for this fixed-color construction. Checking an assignment is efficient because each clause is small, but finding one is a different problem. This particular two-coloring problem has a separate efficient graph algorithm; that fact must not be generalized to every coloring variant merely from the existence of a verifier.

Test the limits and transfer the idea

1. Construction and exhaustive check · allow 55 minutes

Encode a circuit without exponential expansion

Build a CNF formula for the circuit u = a OR b, z = u AND NOT c, with output z required to be true. Introduce variables for both gate outputs and encode each equivalence using clauses of at most three literals. Count variables and clauses.

Enumerate all 32 assignments to verify that the satisfying assignments project onto precisely the inputs making (a OR b) AND NOT c true. Then delete the clause (NOT z OR u) and find a spurious assignment. Explain why bounded clauses per gate keep the encoding polynomial in circuit size, and distinguish this modern circuit exercise from Cook's original query-machine formulation.

Get a starting hint

For u ↔ (a OR b), encode both implications. For z ↔ (u AND NOT c), do the same. Requiring z is a separate unit clause.

Compare your reasoning with the worked solution

The first gate needs (¬a ∨ u), (¬b ∨ u), and (a ∨ b ∨ ¬u). The second needs (¬z ∨ u), (¬z ∨ ¬c), and (z ∨ ¬u ∨ c). Add the unit clause (z). There are five variables and seven clauses.

If the clauses hold, the first three force u to equal a ∨ b and the next three force z to equal u ∧ ¬c. The final clause therefore forces the circuit output true. Conversely, evaluate a satisfying circuit input, assign each gate variable its evaluated output, and every clause holds. The satisfying input triples (a,b,c) are (0,1,0), (1,0,0), and (1,1,0); each has the unique extension u = z = 1.

Deleting (¬z ∨ u) admits a = b = c = u = 0, z = 1. The remaining first-gate clauses hold, (¬z ∨ ¬c) holds because ¬c is true, and (z ∨ ¬u ∨ c) and (z) hold because z is true. But the circuit's actual output is false. One missing implication broke soundness.

With fan-in-two gates, a constant number of clauses and one fresh variable per gate avoids expanding shared subcircuits into repeated formulas. Literal names still require an encoding, but the total remains polynomial. Cook's 1971 paper uses its own definition of polynomial query reducibility and a computation encoding; this exercise explains a related modern mechanism, not an assertion that this exact gate list appears in the original text.

Check your reasoning

• Produces seven correct clauses and proves both directions of the encoding.
• Finds exactly three satisfying inputs and the specified missing-clause counterexample.
• Explains polynomial size and distinguishes the modern construction from the historical reduction definition.

2. Logic and source interpretation · allow 40 minutes

Keep the reduction direction honest

Suppose TAUT(G) answers whether a propositional formula G is true on every assignment. Design a one-query algorithm deciding SAT(F). Apply it to F₁ = (a OR b) AND (NOT a OR b), F₂ = a AND NOT a, and F₃ = a OR NOT a.

Explain why the transformation F ↦ NOT F alone is not a yes-preserving many-one reduction from SAT to TAUT. Identify the language to which it is a yes-preserving reduction. Finally, explain what follows if TAUT has a polynomial-time decision algorithm, and what does not follow from the 1971 paper about P versus NP.

Get a starting hint

The condition that some assignment satisfies F is equivalent to NOT F failing to be a tautology. A query algorithm may branch on either oracle answer; a many-one reduction must preserve yes answers without that final negation.

Compare your reasoning with the worked solution

Query TAUT(¬F), then return the opposite answer. For F₁, the original simplifies to b and is satisfiable. Its negation simplifies to ¬b, which is not a tautology, so the algorithm returns yes. F₂ is always false; ¬F₂ is a tautology, so the algorithm returns no. F₃ is always true; ¬F₃ is always false and hence not a tautology, so it returns yes.

The map F ↦ ¬F reverses, rather than preserves, the SAT-to-TAUT answer. It is a yes-preserving many-one reduction from SAT to NONTAUT, the set of formulas that are not tautologies. A polynomial query reduction can ask about TAUT and negate the answer, which is why reading the historical definition matters. The extra negation symbol increases formula length only by a constant under an ordinary syntax-tree encoding.

If TAUT could be decided in polynomial time, this one-query procedure would put SAT in polynomial time. Combined with the modern NP-completeness theorem for SAT, that would imply P = NP. Conversely, an efficient SAT decider can decide TAUT by testing satisfiability of the negation and reversing its answer. Neither direction proves that such a decider exists or that it cannot exist. Cook explicitly supplies a hardness relationship, not a superpolynomial lower bound. The three truth-table cases check the mechanism, while the quantified equivalence proves it for every propositional formula.

Check your reasoning

• Negates both the formula and the oracle answer in the correct places.
• Distinguishes a query reduction from a yes-preserving many-one reduction.
• States the conditional complexity consequence without claiming a P versus NP resolution.

Check your understanding

An encoding omits every at-least-one-color clause. What spurious assignment can satisfy the remaining constraints?

• All color variables false.
• Every vertex uses all colors.
• No Boolean assignment can exist.

Explanation

At-most-one and edge exclusions alone do not require any color to be chosen.

What does Cook’s theorem prove about P versus NP?

• P is different from NP.
• Every SAT instance needs exponential time.
• It establishes completeness relationships, not a resolution of P versus NP.

Explanation

The theorem transfers efficient solvability between problems but does not settle the open separation.

Original paper and sources

Stephen A. Cook. The Complexity of Theorem-Proving Procedures. Proceedings of the Third Annual ACM Symposium on Theory of Computing, 1971, pp. 151-158. Linked academic copy is Tim Rohlfs’s identified transcription of the original paper.

Read the original paper →

Read the primary paper: Carnegie Mellon University

• The Complexity of Theorem-Proving Procedures: Carnegie Mellon University