The Order of a Contradiction

What exactly distinguishes propositional formulas decidable in polynomial time from random 3-SAT? This text summarizes what has been measured, what has been derived, and what remains open — complete enough to be read without prior context.

01 The question, and why it is hard to pose

Four families of unsatisfiable formulas can be refuted in polynomial time: Horn, 2-SAT, Tseitin (parity equations over GF(2)), and the pigeonhole principle. Random 3-SAT at the threshold α ≈ 4.27 cannot. What is it missing?

Nine candidate criteria were tested and all rejected — core size, tear order, circularity, locality, branching degree, clause width, compressibility, Horn-closeness, backdoors. They all fail on the same counterexample pair, and the reason is structural: the governing quantity is continuous, and the cost depends on it exponentially. A yes/no criterion cannot capture that.

02 The order

Order d*. The number of literals that must be fixed before unit propagation, without any further decision, runs into a contradiction.

2-clauses and Horn clauses force; a general 3-clause leaves a choice and forces nothing. The order measures how far one must guess before propagation takes hold again.

Family	Order d_cert	corresponds to
Horn 3-SAT	0	propagation alone suffices
2-SAT	1	exactly the Aspvall/Plass/Tarjan criterion
random 3-SAT	0.13·n + 3	— measured · code & data
pigeonhole	0.909·n − 7.2	r = 1.000

Theorem. If there is a variable set V with |V| = d such that all 2^d assignments of V run into a contradiction under unit propagation, then F is unsatisfiable; and conversely such a V exists for every unsatisfiable formula. proven The order is thus a sound and complete certificate, checkable with 2^d propagation runs — without having to trust the solver at all. And it yields an executable resolution proof: the conflict analysis of every assignment, resolved backward through the justifications, produces a clause over V alone.

03 The recipe behind all four P cases

None of the four solve by search; all solve by saturation: apply an inference rule to a fixed point, read off the result. This runs in P because the closure lives in a space of polynomial size.

Family	Closure space	Size	for random 3-SAT
Horn	literals	≤ 2n	empty
2-SAT	binary clauses	≤ 4n²	empty
Tseitin	linear forms over GF(2)	rank ≤ n	degree Ω(n) proven
pigeonhole	inequalities (LP)	polynomial	identical to propagation
—	k-DNFs, Res(k)	n^O(k)	exponential proven (Alekhnovich 2005)
—	clauses of width ≤ w	O(n^w)	holds up to n ≈ 53 (w=3) resp. 108 (w=4)

Two 3-clauses resolve to a 4-clause — the class is not closed under its own rule. Forcing closure through a width bound w gives, for fixed w, a genuine polynomial-time procedure, since there are only O(n^w) clauses of width ≤ w. This exact procedure is the object of measurement in the following sections.

04 Three widths that must not be confused

This was a correction to an earlier finding: the number 0.2125·n + 4.09, which had been reported as "proof width," measures w_cert. The true value of w* is 3, the smallest possible for a 3-CNF. An independent reimplementation in Rust confirms w* exactly (2-SAT → 2, pigeonhole → 2/3/4), but does not reproduce d_cert and w_cert — the former is a property of the formula, the latter are properties of the construction.

05 The transition, and the constant within it

The two half-value points are two support points of the inverse function of w*(n):

w*(n) ≈ 3 + (n − 52.9) / 54.6 ≈ 0.0183 · n measured

Ben-Sasson and Wigderson proved that w* for random 3-SAT must grow linearly in n; their constant is hidden inside the Ω-notation. This is its measured value. And it also explains why the polynomial procedure cannot be rescued: n^O(w*) with w* = 0.018·n is n^(0.018n), i.e. exponential.

The estimator, checked against ground truth

The p₄ curve was measured using a shortcut: because the closure is bimodal (section 06), one need not compute it to completion, only determine on which side of the separatrix an instance starts — 480 times cheaper. This estimator was not fitted to p₄ but derived from the feedback mechanism, and it predicted n₅₀(4) = 108.2 in advance. The full computation, run in parallel, has since converged at all eleven support points and gives 107.5 ± 1.1.

This is the sharpest confirmation of the mechanism in this text: a prediction derived from it, independently verified.

The transition also moves with the density, n₅₀ = 16.5·α − 18.0 (r = 0.9976 across four densities). More clauses thus extend the validity of the polynomial procedure — denser instances are easier, and here "easier" means the ignition holds longer.

06 The mechanism: a bistable system

The reason is a feedback loop. A resolvent of width ≤ 3 arises only when two clauses share a literal besides the pivot literal — the fuller the closure, the more partners each new clause finds. The reproduction number R thus depends on what has already accumulated, and the system is autocatalytic.

07 Supply and demand — the matter in three numbers

Raw material  E[P2] = C(m,2)·3(n−3)/C(n,3)  =  164          constant in n
Yield         what an instance accumulates  ≈  500          constant in n
Demand        |A|*(n)                       =  23.3·n − 649  linear in n

The raw material is the clause pairs sharing exactly two variables — these give rise to the width-3 resolvents. Their expected count is available in closed form and does not depend on n: the prediction 164 matches the measurement at all six points (161–168). The yield — what a starving instance actually accumulates — is likewise constant (382–592 over n = 40…90, no trend). Only the demand grows.

What the formula assembles on its own stays the same. What it needs to ignite grows. The transition is the crossing.

Addendum, and it corrects this section. The seeding experiment in section 08 tested whether an instance ignites as soon as its closure reaches |A| *(n) — and the answer is no. With random detours the closure can be driven to 2466 clauses, far past |A| *(60) = 749, without anything igniting. The crossing correctly describes why the transition sits at n ≈ 50; but it is not a threshold one crosses simply by filling up. What actually matters is in the next section.

It sits at n = 49.2 — and with that, three independent measurements point to the same spot: the fraction of ignited instances (52.9), the zero crossing of R at |A| = 500 (49.6), and this crossing (49.2).

And a reformulation of the earlier finding

It used to read: „The search space is not too large to search. It is too small to contain the proof.“ The second sentence is not quite right. The maximum of R stays above 1 up to n ≈ 87 — the self-sustaining regime keeps existing, only no path leads there from the start. At n = 80, an instance is missing roughly 700 clauses, and that is a linear quantity. Notably, a completely different measurement in this project arrived at the same shape — 0.8 binary clauses per variable make the hardness collapse.

08 The exchange rate — what ignition costs

Up to here everything has been observation. This section is the first attempt that fixes a number in advance and lets it be wrong if it is wrong: seed a starving instance with k additional clauses and search for the smallest igniting k.

The delicate point is where the seed clauses are allowed to come from. The instance is unsatisfiable, so every clause is logically implied — the empty one included. "Valid" would thus be an empty criterion, and one could win the test with k = 1 by inserting ⊥. The usable criterion is derivability: the seed clauses must be genuine resolution steps. The source is the width-4 closure, restricted to width ≤ 3 and minus what width 3 reaches on its own — exactly what the stronger prover has and the weaker one could write down.

Wrong at first, then something better found

The separatrix grew clearly linearly (r = 0.911), but with slope 16.2 ± 2.0 instead of 23.3 — 3.6 σ too shallow. The reason is a confound whose direction was known before the measurement: seeding raises the density, denser instances are easier, and at large n more must be seeded. Measured, α rises from 4.27 to 5.24 at n = 70.

Regressing it out — n_eff = n − 16.5·(α_eff − 4.27) — reveals something that was not being searched for:

Ignition does not happen once enough clauses are on hand, but once the instance has been pushed back onto the critical line. measured

n_eff at the moment of ignition, derived clauses, n ≥ 58:  54.0 ± 1.5
n_eff at the moment of ignition, random clauses, n = 60…120: 52.8 ± 0.9
                                       against n₅₀(3)   =   52.9

From this follows a law for the price that contains no new quantity: 52.9 comes from the p₃ curve, 16.5 from the density series, both measured earlier and for other purposes.

And a side result that weighs more heavily for interpretation than the test itself: at n = 70, seeding with derived clauses needed k* = 68, seeding with random ones 63.3. Derivable material is worth no more than freshly rolled material. What is missing is not specific information — it is density.

09 Does reordering help?

The most obvious idea, when the space forms unfavorably: build it differently, the most conflict-rich clauses first. Part of the answer can, exceptionally, be proven here rather than measured.

Width-bounded saturation is a monotone closure operator. Its fixed point is unique. Ordering changes when a clause appears, not whether. proven

This sharpens the main finding: the missing information at width 3 is genuinely missing, not merely poorly ordered. For search the opposite holds — but that is already exploited: VSIDS in CDCL is "most conflict-rich first," and that is where the factor of 1.9 in the exponent comes from. Ordering cannot shorten a proof that must be long.

The one place where selection does decide

Uniqueness holds only at fixed width. If one mixes — width 3 plus a budget of B intermediate width-4 clauses — the procedure is not confluent, and which B detours one takes decides everything. The resulting proof remains ordinary resolution in which all but B clauses have width 3; the space stays O(n³) + B.

Selection measure	what it counts	budget until ignition
random	—	> 150, without exception
yield	released clauses of width ≤ 3	> 150, without exception
fresh	of those, only the not-yet-present ones	1 … 35 at n ≤ 55

Conflict-rich does not mean high yield, but high new yield.

Raw yield behaves exactly like random selection — the richest clauses mostly re-derive what is already present. A deep run over 2000 rounds shows three distinct failure modes: random lets the closure grow steadily to 2466 and never ignites; yield freezes at 496 and stays there for 2000 rounds; fresh reaches 719 and then freezes too.

It does not carry far: between n = 55 and n = 60 it stops working. The wall shifts, it does not disappear. What remains is the best question from this branch — the needed material is tiny (1 to 35 detours out of 5,000 to 29,000 candidates). It is there. Nobody just finds it reliably.

10 Skeleton or signs

A 3-CNF decomposes into the skeleton (which variables occur together) and the signs. For satisfiability the split is known: the skeleton determines how expensive a refutation is, the signs determine whether one exists at all. For ignition it was measured — one skeleton, sixty sign draws, 144 skeletons, 3,456 unsatisfiable instances:

logit p₃ = +5.515 − 0.2772·n + 0.2205·double-triple + 0.05545·pair2
             (9.6σ)   (29.7σ)        (5.2σ)                (15.8σ)

Both contribute, and they can be separated. The ignition rate scatters between skeletons 2.8 to 7.3 times more strongly than the signs alone could explain — so the skeleton contributes too. Within a fixed skeleton, though, the rate is never 0 and never 1 — the signs contribute as well. Converted into variables: a double-triple weighs 0.80 variables, a pair2 weighs 0.20. Since pair2 counts scatter by ±13, their contribution is the larger one.

The n-coefficient −0.277 of this fit reproduces the independently measured p₃ slope −0.2387 — two completely different experiments, the same quantity.

11 What it costs when P stops working

12 What has been proven against us

System	random 3-CNF	source
Resolution	size 2^Ω(n)	Chvátal/Szemerédi 1988
Res(k), k ≤ √(log n/log log n)	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
Cutting planes, k = 3	open	Fleming et al. 2017 only for k = log n
Bounded-depth Frege	open	only Ω(n^(1+ε)) steps, 2024
Frege, extended Frege	open	—

One result of this compilation surprised us: random 3-CNF is already open at bounded depth — precisely where pigeonhole and Tseitin have been settled for years. The two families this project uses as negative controls are, for the Frege hierarchy, the understood cases.

13 The cutting-planes door, and why it closed

At the point x = ½, a clause of width w has slack w/2 − 1. From this it follows immediately:

Tightness at x = ½ is the same as clause width 2, violation the same as width ≤ 1. proven

For {0,½} multipliers the slack of a Chvátal-Gomory cut can be computed in closed form, and for a 3-CNF it is always ≥ ½ — except when two clauses sit on the same variable triple. That is exactly the ignition spark. The cutting-planes route at x = ½ is not a different route from the resolution route. Incidentally, this yields the expected number of ignition sparks, C(m,2)/C(n,3)·3/8 ≈ 20.5/n — a law that had previously only been fitted.

What remains open: the argument hinges on one point. If a procedure cuts elsewhere, the optimum shifts, and about the tightness structure there we know nothing.

14 A detector for unknown closure spaces

The conflict sequence of CDCL can be read as its own object of measurement. Two quantities: recurrence (does the solver return to the same variable supports?) and reach (how far back does a conflict reach?).

Family	small space	symmetry	recurrence	random baseline
pigeonhole	no (for resolution)	yes, maximal	0.2–0.6%	0.00%
Tseitin, grid	yes, GF(2)	yes	49–73%	0.07%
Tseitin, 3-regular	yes, GF(2)	no	51–60%	0.01%
random 3-SAT	no	no	~1%	0.00%

The third row is the separation test: a family with a small closure space and without symmetry. The detector fires there just as it does for the symmetric grid. So it sees the space, not the symmetry — making it a candidate for the task of detecting an unknown closure space before knowing which one it is. For Tseitin it did. For random 3-SAT it stays silent.

An honest limit: both positive controls are GF(2) families, and the pigeonhole principle, with its counting space, triggers nothing. "No signal" therefore does not mean "no space," but "no space of the kind this measure sees."

15 The two resources

There are exactly two properties known to carry short proofs: a small closure space, or symmetry that lifts one case to all cases (this is how Buss's polynomial Frege proof of the pigeonhole principle works).

Family	small closure space	nontrivial orbits	short proof known
Horn, 2-SAT	yes	no	yes, via saturation
pigeonhole, Tseitin	no (for resolution)	yes	yes, Frege resp. Gauss
random 3-SAT	no	no	none

Orbit compression (color refinement on the incidence graph) is, for random 3-SAT, exactly 1.00 up to n = 400 — the automorphism group is provably trivial. For the pigeonhole principle, all variables lie in one orbit.

This is not a lower bound: symmetry is not necessary — Horn and 2-SAT have none. It is the most precise description of the situation available from measurement. What stands out: a short proof that neither saturates a small closure space nor lifts through a symmetry has never been constructed for any family.

16 Conjectures

Explicitly unsubstantiated, but suggested by what has been measured:

• conjectured The width-4 saturation has the same bistable structure as width 3, with a reservoir roughly 50 times larger. The bimodality repeats there (10,000–33,000 versus 0.6–4.0 million); the bifurcation diagram has not been measured.
• conjectured The increment n₅₀(w+1) − n₅₀(w) is roughly constant (55), so w*(n) is linear with 0.018. Two support points; a third would need width 5, whose space already has 1.1·10⁸ clauses at n = 55.
• conjectured The 0.8 binary clauses per variable from one measurement, and the deficit from the other, are the same fact seen twice.
• conjectured The critical law from section 08 also holds for width 4, with n₅₀(4) = 107.5 in place of 52.9. Testable with the same cheap setup, just more expensive saturations — and a hit would show that "pushing back onto the critical line" is not tied to width 3, but is the mechanics of every width stage.
• conjectured The refuting width-4 closure grows like n^3.04 — cubic, even though its space is quartic. The step to width 4 thus buys not a larger proof object but a larger reservoir. The exponent is measured (r = 0.9988); the interpretation is the conjecture.

17 Where it can go from here

1. The remaining skeleton scatter. Double-triples and pair2s together explain part of the skeleton effect. What explains the rest? Candidate: the local expansion of the hypergraph — exactly the quantity the lower width bound comes from.
2. Finding the few good detours cheaply. From section 09: 1 to 35 intermediate width-4 clauses suffice to ignite a starving instance at n ≤ 55 — out of 5,000 to 29,000 candidates. The material is there and tiny; nobody just finds it reliably, and from n = 60 onward not at all anymore. If this succeeds, it stops being a comment on the mechanism and becomes a procedure: width-3 saturation with a polynomial detour budget. If it fails, one knows why — and it would be the first place where hardness has been pinned down as a pure search problem.
3. The critical law beyond n = 120. k*(n) = n(n − 52.9)/16.5 is confirmed up to n = 120. It predicts k* = 285 at n = 100 and 1,782 at n = 200. The test is cheap (seconds per instance), and a break at large n would matter more than any further confirmation.
4. Cutting planes away from x = ½. The only one of the three open doors reachable empirically — but a measure for tightness at an arbitrary vertex of the polytope is missing.
5. The detector on unknown terrain. Let recurrence loose on instances from verification, planning, cryptography. It found a space at Tseitin without knowing it was there; where else does it fire?
6. The fifth closure space. Four are measured empty, one (Res(k)) is proven empty. The list of candidates is not formalized — a single new, serious one would be worth more than any refinement of the existing ones.

18 How measurement is done here

Three rules, all born from mistakes:

• A negative finding without a working positive control is not a finding. A cutting-planes test once reported "nothing found" — and the control revealed that the pigeonhole instance had already stopped firing.
• Compute first, then write. Fitted values were written down more than once before the fit had actually run.
• Intermediate snapshots are selection-biased. A starving closure finishes in tenths of a second, a refuting one takes hours. Anyone who counts midway sees too many starving ones. This error occurred three times within a single measurement, each time in the same direction.

In addition: a complete staged SAT solver in Rust, whose four stages are the four procedures of this project, with a test suite — over 700 instances checked against brute force, and the classification of the measurement instances checked against an independent solver (170 instances, zero discrepancies).