Cook-Levin says any polynomial-time check compiles into one Boolean formula. As a lead, why is that construction still the wrong way to actually build such a formula?
answer
- polynomial is growth, not size
- grid squares the time bound
- encodes a machine, not the problem
- circuits scale with gate count
- a classifier, not a compiler
basics
~20 sPolynomial is not small: the grid is quadratic in a time bound that is already a polynomial of the input length, and it encodes a tape machine rather than the problem. The theorem classifies; it does not compile.
solid answer
~60 sThe construction is a **classification instrument**, not an encoder. Its grid has roughly the square of the time bound many cells, so a cubic-time check on a thousand elements gives a bound of about a billion steps and a grid on the order of ten to the eighteenth cells - polynomial, and utterly unbuildable. Worse, what it encodes is a tape machine's step-by-step history, which has nothing to do with the structure of your actual problem, so the resulting clauses carry none of the structure that makes an encoding tractable to work with. The **circuit form** of the same theorem is the shape people really use: a polynomial-time check on inputs of a fixed length becomes a Boolean circuit, and a circuit becomes clauses with one fresh variable per gate and a constant number of clauses per gate - linear in the circuit, not quadratic in a time bound. In practice teams model the problem's own constraints directly and use the theorem only to know which family they are in.
go deeper
Take away the distinction: polynomial means the cost grows moderately as inputs grow, not that the thing is small. The construction in this theorem is both at once.
Be able to say the grid is roughly the square of the time bound, and that the circuit version of the same result gives a size that tracks the gate count instead.
Show you can separate the proof device from the engineering artefact, and explain why a hand-built model of the problem beats an encoded execution trace on every practical axis.
Own the framing: use the theorem to decide which family a requirement belongs to, and never as the justification for a delivery plan that promises to compile logic into constraints.
## The size the construction actually produces Fix an input length `n` and a check running in time `t(n)`. The tableau has about `t(n)` rows and about `t(n)` columns, so its cell count is of order `t(n)` squared, and the clause count follows. Put real numbers in it: - A check that runs in time cubic in the input, on an input of one thousand elements, has a time bound of about `1000^3 = 10^9` steps. - Squaring that gives a grid on the order of `10^18` cells, each carrying a constant number of variables and clauses. That is a polynomial of the input length, and it satisfies the definition of a polynomial-time reduction perfectly. It is also larger than anything that has ever been written down. **Polynomial is a statement about growth, not about size**, and this construction is the sharpest reminder of that distinction anywhere in the subject. ## What the theorem is actually for The construction's job is to make a *claim about a class* true, once. After it, a hardness argument never has to mention a machine again. So what a lead genuinely gets from it is: - A licence to treat one named problem as a stand-in for the whole of NP. - The guarantee that *some* polynomial encoding of any quickly-checkable requirement into clauses exists, so an encoding attempt is not doomed in principle. - A classification: knowing which side of the feasibility line a requirement sits on, before anyone designs for it. What it does **not** give is the encoding itself. The existence proof is constructive, but the thing it constructs is calibrated for a proof, not for use. ## The circuit form of the same statement There is a second, more workable way to say the same thing. For inputs of one fixed length, a polynomial-time computation can be laid out as a Boolean **circuit** of size polynomial in that length, built uniformly from the program text - each gate corresponds to a small step of work, and wires carry intermediate bits instead of a tape being rewritten. Deciding whether some setting of a circuit's free input wires makes its output true is then the natural complete problem, and it is complete for the same reason. Converting a circuit to clauses is cheap and local: 1. Give every gate a fresh variable standing for its output bit. 2. For each gate, emit a constant number of clauses forcing that variable to equal the gate's function of its input variables. 3. Add a single clause forcing the output variable true. | | tableau form | circuit form | |---|---|---| | what is encoded | a step-by-step tape history | a wiring of gates | | size driver | the square of the time bound | the gate count | | free variables | certificate cells in the first row | unconstrained input wires | | conversion to clauses | direct | one fresh variable per gate | The circuit form loses the vivid picture of a computation unfolding in time, and gains a size that tracks the work done rather than the square of a bound on it. Note that the gate-variable conversion, like the clause-splitting rewrite, introduces variables the original did not have, so it preserves satisfiability rather than producing an equivalent formula. ## Where teams go wrong with this 1. **Promising a compiler.** *Cook-Levin says we can turn our validation logic into a formula* is true and useless as a plan. Nobody encodes an execution trace; they model the problem. 2. **Reading polynomial as cheap.** A quadratic blow-up on top of an already-polynomial bound is exactly the kind of exponent that theory ignores and an engineering budget cannot. 3. **Confusing the two directions.** The theorem says any quick check can be *expressed* as constraints; it says nothing about whether the resulting constraint problem will be answered quickly. 4. **Treating a hardness classification as a verdict on your instances.** Completeness is a worst-case property of a problem; the inputs a system actually receives may be nothing like the worst case. ## The judgment call When a team proposes to express a requirement as a constraint problem, the theorem is the wrong argument to lean on, because it settles only that an encoding exists. The real questions are engineering ones: does a hand-built model of the problem's own structure stay small, does it stay correct as the requirement drifts, and can it be validated against the direct implementation on small instances. Use the theorem where it is strong - deciding whether the requirement is in the hard family at all, and licensing every hardness argument that follows - and treat the encoding as a modelling exercise that must earn its place on its own merits.
- What changes mechanically in the circuit form of the theorem?A polynomial-time computation on inputs of one fixed length is laid out as a circuit whose size tracks the work done rather than the square of a time bound. Each gate gets a fresh variable, a constant number of clauses force it to equal the gate's function, and one clause forces the output true.
- If not the tableau, what does a team actually encode?The problem's own structure: variables for the real decisions, clauses for the real constraints, validated against a direct implementation on small instances. The theorem only guarantees that some polynomial encoding exists; finding a small and maintainable one is ordinary modelling work with no shortcut.
- Does the enormous size mean the reduction is defective?No. A reduction has one job: be computable in polynomial time and preserve the answer, so that difficulty transfers. It is a proof device, and judging it by whether anyone would run it is a category error - much as a proof of existence is not an algorithm for finding the object.
saying these in an interview costs you the question
- Thinks polynomial size means the formula is practical to build.
- Claims the theorem provides a general recipe for encoding real programs.
- Believes the circuit form is a different theorem with different content.
- Assumes converting a circuit to clauses multiplies its size enormously.
- Treats a worst-case classification as a verdict on real instances.