Deutsch

The Order of a Contradiction

What exactly separates propositional formulas decidable in polynomial time from random 3-SAT at the threshold? Sixteen reports from an ongoing project.

As of September 16, 2026

Four families of unsatisfiable formulas can be refuted in polynomial time: Horn, 2-SAT, Tseitin, and the pigeonhole principle. Random 3-SAT at α ≈ 4.267 cannot. Everything here revolves around the question of what causes this difference — and the reports are written so that null results are recorded just as carefully as findings. There are more null results.

Every measured number links to a “View code & data” panel: the source code that produced it, and the actual output — both visible and copyable, not merely asserted.

Where Things Stand

Where the project stands, and where to pick it up.

  1. The Order of a Contradiction The complete state of the work: what has been measured, what has been derived, and what remains open.
  2. Where One Could Start The board as it stands — plus a checklist that disposes of unworkable ideas in half a minute, so the time stays for the workable ones.
  3. The Theorems on a Single Formula Seven variables, thirty clauses, unsatisfiable. Every theorem of the project marked on the same matrix.

Learning

Explanations for anyone who wants to understand the tools themselves.

  1. How CDCL Works — and How to Measure Without Fooling Yourselfnew What modern SAT solvers actually do, one real run step by step, what each building block buys on measured instances, and the null measurements that keep an algorithm programmer honest — with code for everyday use. worked example checked against brute force · for programmers

The Axes of Hardness

What determines how hard a single instance is — and what does not.

  1. Scaffold and Sign Splitting the variance in hardness into its two components. The starting point for everything that follows.
  2. The Sign Axis Half the variance sits in the signs. Fully measured up to Fourier degree 12 — and there it turns out to be exactly two directions.
  3. The Sign Body First the bluntest attempt — the formula itself as a coordinate — which provably fails. Then the proposal that replaces it.
  4. Two-Axis Separation Why aggregates over the assignment space cannot separate SAT from UNSAT. Measured and proven — and the bound against which every approach since has been checked.
  5. Intervening on the Scaffoldnew A probe that finds critical clauses without solving, two axes of hardness that are not expansion, and the first intervention in the corpus: rewiring instances at a fixed degree sequence changes hardness as predicted — but only for solvers that react to structure. causal · pre-registered · 250,800 ablation runs · n = 100 and 130

Predicting Hardness

The narrow ridge: quantities that actually carry information about cost.

  1. d(50 %) Analysis The only quantity that predicts hardness at fixed n — why, and what follows from it. r = 0.56 · requires a solver
  2. The Shape of r(d) The shape of the ordering-rate curve carries more hardness information than d(50 %) alone.
  3. The Judo Thrownew Instead of searching for structure, take the disorder of a process as a probe. Six solver-free probes, 80,000 candidates, calibrated against permutation — and a finding that just clears everything previously solver-free — repeated on fresh instances. strict r = 0.27 · solver-free · confirmed on 900 fresh instances

Spaces and Maps

Not individual formulas, but the spaces they live in.

  1. Map of Instance Space Not the space of solutions, but the space of all instances. Satisfiability is monotone on it — the space has a boundary, a height, and a local geometry.
  2. The Feasibility Spacenew Five candidates for a structural measure, four of them toppled by their own controls. What remains: a redundancy measure with no clustering, and an exactly verified uniform sampler over the full solution space, with a rotatable 3D view of the real clusters.
  3. SAT in Phase Space Replace the truth values with real numbers, and satisfiability becomes a deterministic flow. It finds every solution — but the path there is a chaotic transient with fractal basin boundaries. 1.8 million trajectories · precursor to the judo throw
  4. Trajectories Five plates from 692 MB of raw data: up to 20,006 orderings per instance, every clause a measurement point.

Limits

Where the methods break down, and from what point on the theorems even apply.

  1. Which Lever Actually Movesnew Three places where this corpus contradicts itself — including the largest lever it has, filed as having no effect. And a rule for inventing extension variables: at identical clause and variable counts, targeted definitions rescue 13 of 20 instances where random ones rescue 0 of 23. Then the scaling closes it again. n₅₀ 52.9 → 90.9 · soundness 438/438 · and it still dies
  2. SAT Without AND and OR Unroll AND and OR all the way and a clause becomes one forbidden pattern. Seven executable levels agreeing on 72,320 assignments, one evaluator with four semirings — and two measurements the usual notation cannot phrase: the seed is readable before the run, and the conflict-graph route is dominated. Correction: the third, “the ignition density is width-invariant”, is refuted — see the lever page. AUC 0.91 · solver-free · includes a workbench
  3. Two Attractors Width-bounded resolution doesn't degrade gradually, it tips: either an avalanche of twenty thousand clauses or starvation at five hundred — practically nothing in between.
  4. Where Asymptopia Begins One theorem says proof width grows linearly with n. The measurement says it's 3. Both are right — and the reason is a number nobody had computed until now.