First the bluntest attempt: the formula itself as coordinate. It fails, and provably so. Then the proposal that replaces it — hold the scaffold fixed and span only the signs. The resulting body really is a body. But its coordinate system is fixed before you ever step into it.
n = 14, m = 60 (α = 4.29) · everything exact over the full assignment cube · koordinate.py · vorzeichenkoerper.py
The coordinates of the Map of Instance Space — imbalance, degree spread, height d — are computed quantities. The obvious counter-proposal: take the formula itself. Clauses sorted, per literal a variable index and a sign. It doesn't get more idiomatic, and it doesn't get cheaper either — the coordinate is the input.
Canonical form: within every clause, the three literals sorted by (variable, sign), then the clauses sorted lexicographically. That yields 180 literal slots, each with a pair drawn from 2n = 28 possibilities. It carries the full information — losslessly, because it is the formula.
And it does not classify. Nearest neighbor on this list, 120 exactly solved instances, leave-one-out:
| Quantity | Value | Remark |
|---|
The gain over "always say SAT" is negative. The nearest neighbor sits, in the median, 129 of 180 slots away — it is just some other instance, its label a coin flip.
The reason fits in a single picture. Three distance distributions lie on top of each other: the distance to the nearest neighbor in the sample, the distance to one's own renamed copy (same answer, guaranteed), and the distance to a foreign random instance. And all the way on the left, at 1, sits the scale on which the answer actually tips.
Two random formulas share, in the median, 59 of their 60 clauses not at all. That is counting, not bad luck:
All 180 one-literal neighbors of every instance, checked exactly. Below, the tipping map of a single instance: 60 clauses of 3 literal slots each, marking the slots where flipping a sign overturns the answer.
| Class | Instances | with ≥ 1 tipping neighbor | tipping neighbors on average |
|---|
Small distance ⇏ same label. 82 % of all instances have a direct neighbor with the other label — a single flipped sign in a single clause.
Large distance ⇏ different label. The distance of a formula to its own renamed copy is 149; to a total stranger, 150. The answer is guaranteed to be the same in the first case — verified, 120 out of 120.
The distance in this coordinate is thus independent of the label on both sides. No procedure that relies on neighborhood — 1-NN, kernel, embedding, interpolation — can gain anything from it. Not because the information is missing: it is fully present. But because the metric has nothing to do with it.
This also settles what a usable coordinate has to bring along: it must share the symmetries of the answer. The blunt list shares not a single one — neither the renaming of variables (n! = 1010.9 variants per formula) nor the recalibration of the signs.
The next step therefore does not run over the whole formula, but over the part that carries a symmetry group along with it.
The proposal: hold the scaffold fixed — which variables sit in which clause — and take only the signs as coordinates. The origin is the formula without signs, every literal positive. Each individual sign is its own direction, and the body builds up until every sign has been set.
That is a cleanly defined object: the cube {+,−}180. The origin is always solvable — set everything true. And then the symmetry that determines everything else follows immediately.
Flipping every occurrence of one variable is the same as renaming that variable. x ↦ ¬x. The answer stays. That is a group of 2n = 16,384 calibrations that acts freely on the cube — verified on 1,000 of 1,000 recalibrations.
In particular for g = −1: "all literals negative" is the same point as "all literals positive". Both are trivially solvable. The path "until every sign has been set" therefore ends where it began — it is a closed ring, not a diameter.
The first question to ask of a body is its shape from the outside: how solvable is a shell with r negative literals? Six scaffolds, 60 samples per shell, every instance solved exactly.
Now the construction itself, step by step: starting at the origin, flip one sign after another until all 180 are set. Both ends are the same solvable point — so the number of crossings must be even. Measured: in 100 % of the 120 paths. That is the calibration check.
A ball would have exactly two crossings and a single connected hole.
180 dimensions cannot be drawn, but 16 can. Sixteen sign slots left free, the other 164 held fixed, all 65,536 points solved exactly, one by one. The surface below is this sub-cube in Gray code: adjacent image points are always neighbors in the cube, so they differ in exactly one sign.
| Quantity | measured | random function of the same balance |
|---|
The same 65,536 values, Fourier-transformed. The weight Wk says how much of the answer falls on interactions of exactly k signs. A random function puts its weight in the middle, on degree 8.
Mean degree 1.33 of 16, against 8.0 for noise; the solvable set has exactly one connected component. The intuition behind the proposal is thereby confirmed — it really is a body, not dust.
Now the calibration from §4 applied to the spectrum. A character χS(x) = ∏i∈S xi survives the recalibration of a variable v exactly when S contains an even number of v's slots — otherwise it flips sign while the answer does not move, and its coefficient is exactly zero.
So exactly the sets that hit every variable an even number of times survive: the cycles of the incidence graph. That is a prediction with sharp zeros, and it can be checked against its own noise floor — 3 scaffolds × 6,000 exactly solved points:
| Character class | Scaffold 1 | Scaffold 2 | Scaffold 3 | Prediction |
|---|
Of the C(180,2) = 16,110 pairs, 1,118 (6.9 %) survive — exactly those on the same variable. And their unweighted sum is an old acquaintance of this project:
| Coordinate | Degree | AUC | Correlation | Verdict |
|---|
The naive radius is provably blind. "How many signs have I set" is a degree-1 quantity, hence exactly zero. Correlation with the answer: −0.006 / −0.005 / −0.002 across three scaffolds, AUC 0.508. That is not a weak measurement, it is a theorem — and it is exactly why the radial profile in §5 is exactly mirror-symmetric.
The sign body is not a new door. It is something rarer: the derivation of the door this project had previously only found empirically. The search space on the sign axis is thus not conjectured but proven closed — whoever looks for something there is looking for a function of the cycles, because there is nothing else.
| Degree | Characters | Name | Status |
|---|
And the finding additionally says where the remaining 85 % of the sign axis cannot sit: in any quantity that is not calibration-invariant. Any candidate quantity that changes under the renaming of a variable is finished before the first measurement.
The obvious first move — "(a ∨ b ∨ c) and (¬a ∨ ¬b ∨ ¬c) say the same thing" — holds globally and not individually. Complementing all clauses at once is the calibration g = −1 from §4: the solution is complemented along with it, verified on 400 of 400 instances. Complementing one clause tips the answer — on random instances at the threshold, in of cases.
And there is a counterexample with four variables that can be checked by hand:
The seven clauses over {a, b, c} rule out every assignment except a = b = c = 1; after that, (a ∨ b ∨ d) and (a ∨ b ∨ ¬d) are satisfied by a = 1. After the swap, only 000 remains instead of 111, so a = b = 0 — and then the two d-clauses demand d = 1 and d = 0 at once.
This matches the known extreme case: for Tseitin formulas over a 3-regular graph, the scaffold statistics are independent of the charges, and the sign pattern alone decides satisfiability. Signs cannot be cancelled away — only their orbit can.
What remains are two kinds of redundancy: that of notation (orderings, duplicates) and that of the group (renaming, recalibrating). Both complete, with an exact factor:
| Stage | Bar | Remainder | Factor | Price |
|---|
From 10255 down to 10111. Of that, notation carries 10129 and the group 1015. There is no more group redundancy to be had: Sn ⋉ {±1}n is the full automorphism group of the literal space.
Blocked clauses (BCE) are the strongest polynomial-time-recognizable elimination rule; pure literals are its special case. At α = 2 it removes almost half the formula. At the threshold, less than 1 % remains.
Sorting takes care of notation. For the group, a rule is needed that picks exactly one representative from each orbit. It lives in redundanz.py:
| Check | Result | Meaning |
|---|
Discrete also means: the stabilizer is trivial. The orbit thus has full size 2n·n!, and the quotient in §12 is exact, not an upper bound. The expensive case — refinement fails to discretize, which would require individualization and, in the worst case, graph isomorphism — never occurs for random instances at the threshold.
§3 had diagnosed two ailments. The same 120 instances, now canonicalized:
| Quantity | raw sorted | canonicalized |
|---|
Ailment 1 is cured. "Large distance ⇏ different label" no longer holds — one's own renamed copy now sits at distance zero, without exception.
Ailment 2 is untouched. "Small distance ⇏ same label": 82 % of instances still have a neighbor at distance 1 with the other label. That is a property of the answer, not of the representation, and no canonicalization can change anything about it.
The upshot in one sentence: canonicalization removes redundancy, it does not create structure. The space shrinks by 144 orders of magnitude and stays exactly as disordered.
Twenty-one sign slots left free, in three groups of seven. Each group is one axis, on 128 steps in Gray code: adjacent cells differ in exactly one sign, in all three directions. All 2,097,152 cells solved exactly, one by one, at n = 20 variables and α = 4.25.
This is made possible by an incremental solver: along a snake path through the grid, exactly one sign changes per step — hence exactly one clause — so instead of solving anew, two cuts in the violation field are re-booked and the solution count is carried along. 43 µs per cell on 24 cores, cell by cell checked against the reference solver.
| Quantity | measured | random function of the same density |
|---|
The same picture as in §6, now spatial — and the random control is what sharpens it. The solvable set holds together, where a random set of the same density would fall into tens of thousands of pieces; the unsolvable set tears apart, where randomness would give a single lump. The deviation runs in both directions.
And the last row of the table is the sharpest structure number on the whole page: merging the surface into the largest possible rectangles shrinks it by more than a factor of twenty — for a random function, by a factor of one and a half. The surface consists almost entirely of large flat plates. Why, is in §16.
The cube is visibly structured — plates, bars, columns, stairs, all axis-aligned. There are two possible causes for this, and they can be separated: the function (a few signs carry almost everything) and the arrangement (Gray code puts equal bit values into contiguous stripes). The counter-check is simple: the same set with axis positions shuffled at random, and a random function of the same density on the same grid.
| Case | Surface (faces, with border) | merged rectangles | run length x · y · z |
|---|
Both contribute, but not equally — and the mesh column separates it most sharply. The real body needs 56,839 rectangles. The same set with shuffled axis positions needs 5.6 times as many, a random function on the same grid 36 times as many. The shapes are thus mostly real — Gray code makes them visible, it does not invent them.
The actual reason is found in the influences: how often does the answer tip when exactly this one sign is flipped and all others are left alone? For a random function, all 21 values would be equal.
This is the mechanism behind the steps: a sign that tips the answer in only one direction cuts a half-space out of the body. Several of these give plates, bars, and stairs — never scattered speckles.
With that, every visible shape can be assigned to a sign. Gray code fixes what stripe width results: the highest bit divides the axis a single time, the lowest into 32 narrow bands.
| Rank | Axis · Bit | Shape in the image | Influence | one-sided |
|---|
The third cause holds only for this cube, and that is itself a finding: the three axes are unevenly populated here — influence , spread . The weakest axis has a mean run length of cells against . Those are the long columns in the image. Which axis it falls on is pure chance of assignment: in the comparison cube at n = 22 the three axes are almost equally strong (spread 1.2×), and there the columns don't appear in this form.
All three findings point where the spectrum in §8 already pointed: total influence of 21 against for noise, mean Fourier degree . The shapes are the low order, made visible.
The question remains whether all this hinges on this cube — on the small n, on the resolution, on the number of signs released. So two more runs: the same setup at n = 22 (α = 4.27, again 2,097,152 cells, 597 s instead of 89), and an eight-times finer cube — 256 × 256 × 256 = 16,777,216 cells with 24 free signs, 1,631 seconds.
The core holds across all three. Total influence sits at 1.99 / 1.93 / 1.53 — always at a sixth to an eighth of what noise would give. An approximation from twelve signs hits 97.8 / 99.0 / 97.5 %, and mesh compaction sits at 22.5 / 11.2 / 47.8× against 1.3–1.5× for randomness. The two control factors stay stable too.
Two statements, however, are cube-specific and must not be generalized. Axis asymmetry varies (5.3× / 1.2× / 2.2×) — the long columns in the image are a property of the assignment, not of the body. And the relationship between influence and one-sidedness even changes sign: +0.312 / −0.048 / −0.747. Signs are one-sided everywhere — which ones especially are, is chance of the cube.
And one restriction the large cube forces. At 50 % and 60 % solvability, the solvable set largely held together and the unsolvable one fell apart; at 19.3 % it is reversed — the largest solvable component holds only 5.9 % any more. That is not a difference between SAT and UNSAT, but percolation: below the threshold of the cube lattice (about 31 %), any set of this density falls apart.
The comparison with randomness survives this easily though, and is the real point: at 19.3 % density, a random set falls into 1,442,302 pieces with the largest share 0.0 % — the measured solvable set into 94. That is a factor of 15,000 less fragmentation at the same density.
Concentration and one-sidedness have so far been measured on one cube. The counter-check: 30 freshly drawn cubes at n = 18, 32,768 cells each solved exactly — 450 sign slots.
| Quantity | Mean ± spread | what follows from it |
|---|
And with that the question that decides whether this is a tool: can one tell in advance which signs will be the influential ones — from cheap local properties of the slot? Also checked are two expensive features (does the variable lie in the backbone, does the literal agree with its backbone value) and a null control that must come up empty: the Gray bit position, pure arrangement.
| Feature | Kind | r | in σ |
|---|
And with that, it is not a procedure. Which signs are influential depends on the instance — and computing the influence of a sign means solving the formula on both sides of it. The structure is there, visible and measurable; the path to it runs through the answer one is looking for.
The cube looks strikingly symmetric. There are two reasons for this, and only one of them lives in the body.
The mirrored Gray code satisfies an identity one can verify directly:
Mirroring one axis is thus exactly flipping one sign — the one on that axis's top bit. From this follows a sharp prediction: the agreement of the image with its mirror image must equal 1 − influence(top bit).
| Cube · Axis | Mirror agreement | 1 − influence(top bit) | Deviation |
|---|
Deviation exactly zero, on every axis of every cube. Mirror symmetry is the top bit — a finding about the map, not about the body. Re-laying out the same data with the strongest signs on the top bits, the agreement drops to — the symmetry disappears, without anything about the body having changed at all.
Some of the released signs change the answer in not a single cell. Not rarely, not almost never: exactly never. Every such sign doubles the image without adding anything.
| Cube | released | effective | ineffective | lossless reduction |
|---|
| Explanation | Hits | Assessment |
|---|
And what this means for instance space: nothing. These signs are ineffective in this cutout — their clause is already satisfied by the fixed remainder. It is not a symmetry of the formula but a property of the context, and recognizing it requires the backbone, i.e. the solution. The balance from §12 therefore stands: 10111, and the space does not get any smaller because of it.
What does get smaller is the image: the 256³ cube is in truth a 14-dimensional object, repeated 1024-fold on the grid.
Completeness also means saying what does not exist.
| Proposal | Status | Reason |
|---|