Seven variables, thirty clauses, unsatisfiable. Every theorem in this project is shown as a marking on the same matrix — rows are variables, columns are clauses, green = positive, red = negative literal.
The formula
Thirty clauses over seven variables. Every column has exactly three filled cells — that is the 3-CNF condition. Everything that follows is a marking on exactly this picture.
C3 · The distance is the ground-state energy
d(F) = minx c(x) — the smallest number of sign flips that makes F satisfiable equals the smallest number of simultaneously violated clauses.
With seven variables, all 128 assignments can be shown:
Every cell is an assignment. None reaches zero — the formula is unsatisfiable. But eleven reach energy 1: they violate exactly one clause. So d(F) = 1, and a single sign flip suffices.
One of these eleven ground states, entered into the matrix — the assignment stands as a column on the left, the single violated clause is marked:
Assignment x = 0000010 (green row = true, red = false). Under this assignment, only C10 is violated: all three of its literals are false. That is exactly energy 1.
C1 and C2 · Guilty ⟺ repairable ⟺ indispensable
For unsatisfiable F, the following are equivalent: (a) there is an x with c(x) = 1 and C as the sole violated clause · (b) a sign flip in C makes F satisfiable · (c) F∖{C} is satisfiable · (d) C lies in every minimal unsatisfiable subsystem.
If you collect, across all eleven ground states, which clause is violated in each, exactly six come out:
The six marked columns are the clauses violated in the ground states — and at the same time exactly the indispensable ones. The theorem is not asserted here but counted out: both sets are {C4, C9, C10, C25, C27, C29}.
To check it yourself. Take C10. Flip one of its three signs — the formula becomes satisfiable, with exactly the assignment from above. If you instead remove C10 entirely, it is also satisfiable. Both say the same theorem.
A1 · The order certificate
If there is a variable set V with |V| = d such that all 2d assignments of V run into a contradiction under unit propagation, then F is unsatisfiable.
For this formula, d = 2 suffices. Fixing x1 and x2, propagation handles the rest — in all four cases:
Four leaves, four contradictions. Every arrow is a propagation step forced by the formula; at the bottom stands the clause where it breaks. The unsatisfiability proof needs nothing more.
The same four conflict clauses in the matrix, plus the two certificate variables as rows:
Blue rows: the two fixed variables. Red columns: the four clauses where propagation breaks each time. Two of 7 variables and four of 30 clauses carry the entire proof.
B1 · The slack
If a clause of width w is encoded as an inequality, it has slack ½w − 1 at the point x = ½ — independent of the signs.
In this formula, every column has three cells, hence width 3, hence slack ½·3 − 1 = +0.5. Not a single one is tight. Tight would mean width 2 — and that would first require a literal to be falsified:
Under each column stands its slack at x = ½. All equal, all slack. This is exactly where the cutting-plane approach fails (Theorem B3): there is no tight spot where a rounding could take hold.
C4 and C5 · The backbone as a handle
Let F be satisfiable. Then F ∧ C is unsatisfiable if and only if all three negations of the literals of C are backbone literals. Consequently |A| = C(b, 3).
Removing C4 makes the formula satisfiable — and so narrowly that all seven variables are frozen. It then has exactly one solution:
Grey column: C4 is gone. Blue rows: all seven variables are backbone, their value is fixed in every solution. After C4, there are thus C(7,3) = 35 different 3-clauses that would make this formula unsatisfiable again — C4 is only one of them.
Resolution · why saturation starves
Two clauses can be resolved if they share a literal with opposite signs. The result is usually wider than the parents. Only if they also share a literal with the same sign does it become narrower:
Every arc connects two clauses whose resolvent has width ≤ 2. At n = 7 there are 7 of them — plenty. At n = 200 there are, on average, 0.2, and from n = 200 on, not a single one. This is the ignition yield 39.3/n from ZUENDUNG.md, still in the visible range here.
What this formula cannot show. It is too small for the scaling laws: d_cert = 0.130·n, proof width 0.254·n, ignition yield 39.3/n, the avalanche distribution. Those need n in the hundreds. What it does show are the theorems — and those hold at every size.