The board as it stands: what is proved, what is measured, what remains open — and a checklist that dispatches unworkable ideas in half a minute, so that the time is left for the workable ones.
Three questions are easily confused, and the confusion costs weeks.
| Question | What would have to be shown | Our relation to it |
|---|---|---|
| P vs NP | a polynomial algorithm, or that none exists | not directly |
| NP vs coNP | a proof system with polynomial-size proofs for all tautologies (Cook/Reckhow) | this is our program |
| Random 3-SAT | that this one family is easy or hard | our measurement object |
Two consequences worth remembering. First: random 3-SAT is neither necessary nor sufficient for P vs NP. P vs NP is a statement about the worst case — were random instances easy, P = NP would not follow; were they hard, P ≠ NP would not follow either. Second: they are nonetheless the standard test family of the Cook/Reckhow program, and the road to NP ≠ coNP runs through lower bounds for ever stronger systems.
Whoever wants the big prize must show that some system has no short proofs — and the family is a free choice. We chose random 3-SAT because that is where most is known.
| System | Result for random 3-CNF | Source |
|---|---|---|
| Resolution | size 2^Ω(n) | Chvátal/Szemerédi 1988 |
| Res(k), small k | exponential | Alekhnovich 2005 |
| Polynomial calculus, any field | degree Ω(n) | Ben-Sasson/Impagliazzo 1999 |
| Sums of squares | degree Ω(n) | Grigoriev 2001, Schoenebeck 2008 |
| Rank-1 cuts at x = ½ | violation 0 | here, computed exhaustively |
Five closure spaces, all empty: literals · binary clauses · linear forms over GF(2) · LP inequalities · clauses of width ≤ w. Add to that no symmetry (orbit compression exactly 1.00 up to n = 400) and no signal from the recurrence detector (~1% versus 49–73% for Tseitin).
| System | What is missing |
|---|---|
| Cutting planes at k = 3 | Fleming et al. 2017 covers only k = log n |
| Bounded-depth Frege | only Ω(n^(1+ε)) steps known (2024) |
| Frege, extended Frege | no superpolynomial bound is known for any family |
The last point is not a gap in our own work but the open question of proof complexity for forty years.
Expansion is a GLOBAL property.
Every one of our tools is LOCAL:
fixing a variable → touches 12.8 clauses
adding a clause → touches 1
a resolution step → touches 2
Ω(n) local moves for a global property — hence all costs are linear in the exponent. Proof complexity knows three non-local tools: symmetry (measured absent), linear algebra (proved ineffective), extension (open).
Work through this in order for every new idea. A "no" doesn't mean "wrong" — it means: here is where the burden of proof lies.
The one non-local avenue still open. Introduce a fresh variable y, with defining clauses:
y ↔ (a ∨ b) → (¬y ∨ a ∨ b) , (y ∨ ¬a) , (y ∨ ¬b)
This preserves satisfiability — y is defined, not constrained. Any number of such definitions may be stacked.
Extension makes width bounds meaningless — by construction.
Our whole hardness picture hangs on width: proofs need wide clauses, wide clauses are costly. Extension lets one name a wide fact and then keep computing at width O(1). That is why it isn't merely the last door — it is the door our own argument cannot, in principle, close.
Cook's proof of the pigeonhole principle in extended resolution is polynomial, where ordinary resolution needs 2^Ω(n). The pattern: extension encodes a self-reduction — one names the instance of the smaller problem and runs an induction.
Find polynomially many definitions y₁…y_p such that the extended formula has small closed clause sets — i.e., low expansion in the extended variable space.
Because closed sets (∂S = 0) are exactly what random instances lack, and their count demonstrably predicts the ignition point (p ~ 2·10⁻¹³).
And now the trap. Compute the boundary of the extension gadget itself:
S = { (¬y ∨ a ∨ b) , (y ∨ ¬a) , (y ∨ ¬b) }
Variables: y (3×), a (2×), b (2×) → ∂S = 0
The gadget is itself a closed set. Low expansion can therefore be forged at will, without gaining anything — the defining clauses are satisfiable, no contradiction ever follows from them. Two binary clauses come free with it, but they are definitional, not constraining.
Closedness is necessary, not sufficient. Everything except the contradiction can be forged.
Anyone proposing an extension therefore has to say why the resulting closedness is load-bearing and not merely definitional. That is the sharpest test that can be formulated — it has already taken apart one idea here.
| Idea | Assessment |
|---|---|
| Name the interface of a subformula. If everything in S is resolved away, a clause over ∂S remains. Name it. | Cost 2^|∂S| = 2^εk. For k ~ log n the gadgets are polynomial. Close to what CDCL learning already does anyway. Testable. |
| Name a coarsening. Group variables into blocks, one variable per block for the block state. | Probably no — randomness is not self-similar. But testable in an hour, and the "no" would itself be informative. |
| Name learned clauses. Replace every learned clause of width w with a variable. | This is at its core "extended learning"; empirically it gives nothing on random instances. But why was never measured — with the expansion profile that's now possible. New measurement. |
| Count beyond x = ½. If a procedure cuts elsewhere, the optimum shifts. | The only one of the three open doors reachable empirically. What's missing is a measure of tightness at an arbitrary polytope corner. A tooling problem, solvable. |
| Exploit the SAT/UNSAT asymmetry. WalkSAT solves every satisfiable threshold instance. | A strong hint that the issue is the certificate, not the search. Fits squarely into the Cook/Reckhow frame. |
| A lower bound instead of an algorithm. Bounded-depth Frege on random 3-CNF. | Open, well-defined, publishable — and the expansion data are exactly the tool with which such bounds are usually established. The most realistic contribution. |
The instruments for every idea are ready to hand.
| Question | Tool | Duration |
|---|---|---|
| Does an extension actually lower expansion? | expansionsprofil | minutes |
| Does a seeded or extended formula ignite? | wechselkurs, umweg | minutes |
| How many detours does it really need? | existenz (proof DAG) | hours |
| Does a procedure reach further than n₅₀ = 52.9? | pvier, schnellp4 | minutes |
| Does a family have a small closure space? | recurrence detector | minutes |
| Does it have symmetry? | bahnen (1-WL) | seconds |
| How many binary clauses arise? | zweier | seconds |
And the rule that has saved us three times over: a negative finding without a working positive control is not a finding.
For every idea, first find a family where it must work (pigeonhole, Tseitin, 2-SAT), and check that the instrument fires there. A cutting-planes test once reported "nothing found" here — and the control revealed that the pigeonhole family had already stopped firing.