Three Levels of Hardness

Core idea [framework]

Hardness is considered on three separate levels. There is no intrinsic “easy” — easy problems are just as hard on level 1; they merely have a shortcut.

Criterion separating 2 from 3: the structure holds for all instances of the class — or only for a fraction.

Refinements of October 7, 2026 [framework]

• P vs NP means “in general”. The question is about any polynomial procedure, idiomatic or not. For the class question, level 2 therefore counts.
• Where the decision lies. Level 1 is always present and expensive for 3-SAT; level 3 by definition does not carry the whole class. A decision in favour of P = NP could only run through a level-2 structure for 3-SAT. The framework thus says where the only possible hit would sit — not whether it exists.
• Asymmetry of detectability. Level 1 is trivially detectable. Level 3 is verifiable in the individual case but practically impossible to rule out: the space of possible finds is unbounded, and even finding small backdoors is hard in general.
• Contained vs. accessible. Every level-2 invariant rests on information already contained in the instance, since the translation into the new representation is a computable function of the instance. It is exploitable only if that translation is cheap (polynomial). The real question is therefore: is there a cheaply computable, class-wide invariant? At its core this corresponds to the notion of polymorphism in CSP theory.

1a · Additions to the framework (M7–M10) [framework]

• Frege belongs on level 1, not on level 3. Frege is complete: for every unsatisfiable formula a Frege proof exists, as with resolution. Level 3 is the axis “works on some instances / does not work at all on others” (e.g. Gauss only for affine solution sets). Frege sits on the length axis: it always applies, the only open question is whether proofs are short. Frege is thus the strongest known level-1 procedure; its open lower bound for random 3-SAT is the actual wall.
• Seeing the structure that is there — not the one that is missing. A stronger proof system can see existing structure that a weaker one overlooks (pigeonhole principle: exponential for resolution, polynomial for Frege). It cannot see structure that does not exist. Open gap: the transfer “instance is incompressible” → “every proof is long” for strong systems (proved for resolution, not for Frege). [open]
• Three level-1 quantities that must be kept apart (from M9):
  (1) procedure cost on the whole formula — which also pays for redundancy;
  (2) core cost — effort on a minimal unsatisfiable core, without redundancy;
  (3) proof length — minimum over all proofs; only it concerns the wall.
  The level-1 slopes so far (§ 3a) measure quantity (1).
• Two notions of instability. Flip sensitivity (yes/no flips on one bit) is shared by XOR and 3-SAT alike; it only forces a proof to read all bits. The finer quantity is the movement of the solution space per formula change and its compressibility (see § 3f). It separates XOR from 3-SAT.

1b · Refinement of October 8, 2026 [framework]

The three levels, sharpened.

• Level 1 (idiomatic, direct): complete exclusion procedure — resolution, DP, up to Frege. Frege belongs on level 1 (complete, length axis); its open lower bound for random 3-SAT is the wall.
• Level 2 (idiomatic, shortcut): must follow from an idiomatic property; for constraint problems this is a polymorphism. A polymorphism belongs to the language, not to the individual formula — level 2 is therefore by definition a property of the language. For 3-SAT it is empty (no polymorphisms except projections).
• Level 3 (foreign to the problem): a property that only some instances carry and that by definition does not come from the problem. Examples: backdoors into Horn, 2-SAT or XOR (they use the polymorphism of a different language), islands (M5), affine substructures (M6).
• Consequence: the question “language versus instance” is not a gap but exactly the boundary between level 2 and level 3. The bridge of Atserias–Ochremiak (language level) thus sits on the right level. “Contained vs. accessible” lives on level 3: an instance can contain a foreign structure without one being able to find it efficiently.

Where the PC degree stands. The PC degree over GF(2) is carried as a level-2 measure: it measures whether an algebraic shortcut of bounded degree exists (the degree stays bounded no matter how large the instance gets; because PC is complete, some degree suffices for every formula). [theorem, Atserias–Ochremiak]: PC over GF(2) is at the same time a complete level-1 system with counting mod 2 built in. The characteristic is exactly the point where level-2 algebra moves into a level-1 system. A degree jump for 3-SAT is therefore a negative level-2 finding, not a cost finding on level 1.

Level 1 versus level 2 — the gap theorem. [theorem, Atserias–Ochremiak ICALP 2017 / TOCL 2019, Thm. 1, Cor. 1] A finite constraint language either has resolution refutations of constant width (exactly when it has bounded width) or neither subexponential bounded-depth Frege refutations nor PC over ℝ or SOS of sublinear degree. This holds for languages (all instances), not for PC over GF(2). Consequence: 2-SAT and Horn are already easy on level 1. The gap “level 1 hard, level 2 easy” exists only for languages whose shortcut counts (linear equations, XOR). The only level-2 shortcut that level 1 does not already see is counting.

Two separate ingredients of hardness (result from M13–M15b) [measurement]

Only 3-SAT has both ingredients.

Further development of the randomness-preservation thesis [hypothesis, partly measured] — refines the short form “2-SAT damps in volume, XOR in shape, 3-SAT lets through”, does not replace it:

• Two levels of randomness (“randomness squared”): the first randomness sits in the formula (choice of variables, signs, relations, length). The second is its projection into the solution space. For XOR, linearity catches the projection (affine space, short description); Gauss compresses the projection, not the formula. For 3-SAT there is no such constraint; the formula’s randomness penetrates into the solution space.
• Incompressibility of the instance is irrelevant, because XOR and 3-SAT instances are equally incompressible. What matters is the projection.
• Asymmetry: a 3-SAT clause allows 7 of 8 patterns (loose coupling), an XOR constraint 4 of 8 (tight coupling). [correction] Asymmetry alone does not create hardness — Horn also has 7:1 and is easy (M13/M15). What matters is asymmetry and missing order.
• Measured version (M15b): hardness means every operation has a small but nonzero defect ε per clause; the random placement of clauses makes the defects independent, so that they multiply over linearly many clauses: fidelity T ≈ ∏(1 − ε_c). Level 2 is exactly the case ε = 0. For 3-SAT the best case is majority with ε ≈ 0.01 per clause (elementary anchor without correlations: 6/343 ≈ 0.0175).
• Density version: hardness arises where locally consistent partial assignments survive longest (pebble game / resolution width). At small n this already drops off at constant density from about twice the threshold; asymptotically the width is linear for every constant density (Ben-Sasson–Wigderson), and over-determination kills the local states only at superlinearly many clauses. [correction] (K9) From Ω(n^1.4) clauses there are short TC⁰-Frege refutations (Müller–Tzameret), from c·n^1.5 polynomial-time refutation (Feige–Ofek). The thesis therefore holds only for (almost) linear density; the statement “for random 3-SAT no structure exists by a counting argument” is not tenable in this generality.

Where the gap sits now [open]

• The instance and projection level is measured; the language level is a theorem (no polymorphisms).
• What remains unproved is the upper storey of the proof architecture: “Every fast algorithm must use an idiomatic rule (operation with ε = 0).” For 3-SAT this is equivalent to P ≠ NP. The measurements show quantitatively that 3-SAT instances carry no idiomatic rule; they do not show that no other fast algorithm exists.
• For resolution the step “instance without structure → every proof is long” is proved, likewise for PC (degree), open for Frege.

The central question and its two outcomes [framework]

Is the level-1 hardness of 3-SAT and XOR-SAT the same on the same scaffold (same hypergraph, same density)?

Both outcomes are informative: the programme locates; it does not run a yes/no test. The measured outcome is in § 3a.

Instruments and status

a) ebene1_dp.py — level 1, Davis–Putnam elimination [measurement]

n = 10–20 (dense scaffold: n = 10–18) · 30–40 instances per row · time cap 30 s

Measured per instance: required information (need = n − log₂ #solutions), size of the largest intermediate clause set (log2 cnf), resolution width (widest clause produced) — in two orders: idx (strictly idiomatic) and minres (fewest resolvents first). Instances that hit the time cap count as “capped”; their cnf value is then only a lower bound, all other quantities remain fully valid.

Slope of log₂ cnf per variable, idx / minres:

• Information: 3-SAT at the threshold 0.949 bit/variable, XOR 0.929 → linear information, exponential effort.
• XOR sparse, idx: raw medians give ≈ 0.63; over uncapped instances only, 0.501 — at n = 20, 15 of 40 are capped (survivor bias).
• 3-SAT dense, idx: raw medians ≈ 0.75, matching the main run. The reported uncapped slope 0.525–0.626 is biased, since at n = 18, 24–27 of 30 are capped.
• XOR dense: at α = 4.267 always unsatisfiable; what is measured is the effort until contradiction. From n = 14 on all instances are capped → the values are lower bounds.
• Resolution width (dense), n = 10 → 18: 3-SAT idx 7 → 12 (≈ 0.5/variable), minres 6 → 10 (0.45/variable); XOR idx 7 → ≥ 10, minres 6 → ≥ 11 (≥ 0.6/variable; capped values seen only up to the abort).
• Null result: the BDD size of the intermediate projections separates nothing; it depends strongly on the number of solutions.

Caveats

• Same scaffold ≠ same information. On the sparse scaffold 3-SAT gains only 0.19 bit/variable versus 0.93 for XOR; XOR brings 4 clauses per hyperedge. Only the triad (own threshold, XOR density, OR density) is robust.
• The DP width is an upper bound on the minimal resolution width. The known Ω(n) bounds are not certified by the data, only corroborated.
• What is measured is resolution, the canonical idiomatic procedure — not every conceivable one.
• n ≤ 20.

b) m5_inseln.py — island structure of the solution set [measurement]

n = 8–14

• [pending] Detour factor (shortest path length within the island / Hamming distance), motivated by Gopalan, Kolaitis, Maneva, Papadimitriou (2006). Measurement planned below the threshold (α ≈ 3.8–4.1), since too few solutions exist at the threshold.

c) m6_affin.py — the affine route on the solution set [measurement]

n = 10–20 · 60 instances

Quantity fit: the fraction of the affine hull of the solution set that actually consists of solutions (fit = 1: the solution set is an affine space, Gauss applies exactly).

• [open] Whether the remaining ≈ 2 % goes to 0 asymptotically cannot be decided from 3 cases.
• [pending] The column “nearly affine” (fit ≥ 0.5) has not yet been split into trivial and genuine cases.

d) gauss_dp.py — the affine route during the run [measurement]

n = 10–18 · 30 instances

Three variants on the same instances: plain DP; DP with directly present units and equivalences (“local”, isolating the effect of mere unit propagation); DP with detection of complete parity patterns (up to 6 variables) and Gaussian combination over GF(2). Only what does not already lie in the span of units and equivalences counts as a genuine Gauss contribution.

• Limit: what is measured is the tool class “detect complete parity patterns + Gauss” (essentially the approach of CryptoMiniSat), not the much stronger proof system Res(⊕), which allows arbitrary linear forms in intermediate steps.

f) m7_bewegung.py — movement of the solution space [measurement]

n = 12–20

Definition: d_j = number of solutions added when unit j is removed (unit = clause for 3-SAT, whole equation for XOR). Exact by brute force, computed as the number of assignments that violate only unit j. Main measure: dist = number of distinct values of d. Design: XOR on exactly the same variable triples as the 3-SAT instance (paired, same hypergraph); the instances are bit-identical to ebene1_dp.py.

• XOR: at most 2 distinct movement values in all instances. This is a theorem, not a measurement fluke: dropping one equation either doubles the affine solution space or changes nothing.
• 3-SAT at α = 0.918: dist (median) 10, 13, 15, 17, 18 at 11, 13, 15, 17, 18 clauses (n = 12–20) — almost every clause moves the solution space by a different amount. At α = 4.267: median 6 → 9, maximum 11 → 27.
• Same number of solutions (only unsatisfiable instances comparable): 3-SAT 4, XOR 1 (median).
• Paired entropy of the movement: H(3-SAT) > H(XOR) in 98–100 % of seeds.
• Level-1 width (DP) on the same hypergraph, dense, n = 12–20: 3-SAT 7/8/8/9/10, XOR 7/8/9/11/11; XOR-DP practically always capped from n = 16. The movement separates what width and expansion by construction cannot separate: the relation on a fixed scaffold.
• Expansion (Ben-Sasson–Wigderson quantity) is not measurable at n ≤ ~30: every dense instance contains, in the median, 6, 5, 4, 3, 3 identical variable triples (n = 12–20), matching the expectation ≈ 3α²/n. Two clauses on the same triple have an empty boundary → expansion 0.

g) m8_nsgrad.py — Nullstellensatz degree over GF(2) [measurement]

n = 14–20 · 120 instances

Clause → polynomial (product of the false indicators), refutation of degree d by incremental Gaussian elimination over GF(2). Gauss “lives” in this system: the four clause polynomials of an XOR equation sum modulo 2 exactly to the linear equation. Checked: satisfiable instances are never refuted, unsatisfiable ones always, XOR always in degree 3.

• XOR: degree 3 in all 960 instances.
• 3-SAT, distribution (degree:count):

• Paired (both unsatisfiable): degree 3-SAT > degree XOR in all 464 pairs.
• Within 3-SAT (unsatisfiable only, number of solutions 0): ρ(dist, degree) positive in all 7 defined cases (+0.05 to +0.47).
• Limit: NS is weaker than Polynomial Calculus. A high NS degree does not prove a high PC degree; a small NS degree, by contrast, is a genuine refutation.

h) m9_kern.py — proof versus procedure: DP on the minimal core [measurement]

n = 14–20

For each unsatisfiable 3-SAT instance one minimal unsatisfiable core (MUS, deletion procedure); DP (minres) on the whole formula and on the core, NS degree on both. Values: median.

• Redundancy makes the DP more expensive and the proof cheaper: ρ(frac0, DP cost) is positive in 7 of 8 cases on the whole formula, negative in 7 of 8 on the core. Without redundancy the DP behaves like the NS degree. On the core both systems agree: ρ(NS degree, core DP) positive in 8 of 8 (+0.12 to +0.40).
• Inflation = log₂ cnf − log₂(number of clauses), i.e. how many clauses the DP generates beyond the starting set. 3-SAT core, median (90 % quantile) at core variables 13/15/17/19: α = 4.267: 0.00 (0.07), 0.02 (0.67), 0.08 (0.69), 0.63 (1.69); α = 5.0: 0.00 (0.38), 0.07 (0.87), 0.28 (1.10), 0.51 (1.57). The inflation sets in between 17 and 19 core variables. On the whole formula it is about 5.5 bits at n = 20, on the core about 0.6 bits: the bulk was redundancy.
• XOR cores: at the same density as 3-SAT (paired), the equation core stays at 8 equations on about 11 variables from n = 16. Reason: XOR sits there at 4.6 times its threshold and always contains small contradictions. Even just above its own threshold (α = 1.0 / 1.1, unpaired) the cores stay at 6–8 equations, 8–12 variables, without inflation. A comparison with 3-SAT is therefore not possible → § 3i.
• Fragility of level 2: on the equation core XOR always has NS degree 3, on the clause core (individual ones of the four clauses minimised away) 4–6. If a single clause is missing from an equation, the Gauss shortcut is gone; for resolution this makes hardly any difference.
• Limits: the MUS size depends strongly on the deletion order (ρ between two orders only 0.14–0.41); krit is order-free. Values at n = 20 fluctuate slightly between runs because capped DP runs are excluded.

i) m10_tseitin.py — XOR without redundancy [measurement]

12–36 variables · 60 resp. 20 formulas per size

Tseitin formulas on random connected 3-regular graphs (expanders) and on prism graphs (narrow treewidth, positive control). The whole formula is the minimal core (checked by brute force up to 21 variables: 1.00; once 0.98 at V = 10, explainable by a bridge in the graph).

• Control: from 24 variables on, expander and prism diverge. The prism stays at about 1 bit, the expander grows steadily. The inflation measures the graph structure (expansion), not the relation.
• Comparison with the 3-SAT cores from § 3h at the same number of variables, median (q90) / width:

NS degree 3 in all 420 Tseitin formulas (3-SAT cores: 6–7). No run capped.

j) Overview M7–M10 [measurement]

M7–M9: n ≤ 20 · M10: up to 36 variables

• Level 1 (resolution/DP on the core, width): XOR ≥ 3-SAT; driven by expansion.
• Level 2 (NS over GF(2)): XOR constant degree 3, 3-SAT growing.
• The movement quantity sits on the side of level 2: a class detector for the “short rule”, not an instance measure of proof effort.
• Within 3-SAT, the tightness of the core (little redundancy, many critical clauses) drives NS degree and core DP in the same direction.
• Redundancy distorts procedure costs: whoever wants to measure level-1 hardness has to subtract it.

Limits: n ≤ 20 (M7–M9), up to 36 variables (M10); DP with the fixed minres heuristic is not a shortest proof; slopes from few points.

k) m11_pcgrad.py — PC degree over GF(2) on the M9 cores [measurement]

n = 14–20 · tdc3

Convention: multilinear, multiplication x·p only for degree(p) < d. Checks clean: soundness 464/464, XOR equation core degree 3 in 960 cases, no bound violated (PC ≤ NS, PC ≤ core width), nothing capped.

• 3-SAT cores: PC degree almost always 4 (occasionally 3), constant from n = 14 to 20, both densities. NS degree on the same cores 6 → 7, core width 5–6 → 7. The gap NS − PC grows from 2 to 3.
• Whole formula: the share refutable in degree 3 falls with n (α = 4.267: 30/39 → 7/40; α = 5.0: 64/72 → 30/91) — small contradictions from redundancy become rarer.
• XOR clause core: PC degree 3 in 959 of 960 cases (NS there 3–7).
• Reading at the time: growth in M8 is a property of the weak system NS. [correction] (K2) Holds only in the measured range n ≤ 20.

l) m12_grosskern.py + m12pc.cpp — large core, first PC degree jump [measurement]

Cores 24–55 variables · tdnb1

C++ kernel: DPLL deletion MUS, PC closure with AVX2. Run: seed 11, 60 instances, dmax 4, 3 GB, 1180 tasks, 38.8 min. Checks: MUS timeouts 0; PC aborts 3 (memory, only n = 56); soundness 367/367; DP width < PC degree: 0 (DP width median 11); Tseitin 3:100; XOR clause core 3:679, 4:8. “≥ 5” means: the complete degree-4 closure does not contain the 1 — exact, not a timeout.

Main curve by number of core variables (both α together), share ≥ 5 (restricted rule):

Per α (n | UNSAT of 60 | core clauses/core var. | share ≥ 5):

Tseitin (24/30/36/42/48 variables): 3:20 in each case.

Limits: degree 4 to 5 at n ≤ 55 says nothing about proof size (d²/n < 1, [theorem] Impagliazzo–Pudlák–Sgall). Asymptotically the PC degree over GF(2) grows linearly ([theorem] Alekhnovich–Razborov 2003); M12 presumably shows the onset; the location of the jump and its independence of density are covered by no theorem.

m) m12b_konvention.py — full multiplication rule as a counter-check [measurement]

tdnb1 · seed 11, 60 instances, ns 36–52, 630 tasks, 119.5 min

Question: is the jump an artefact of the convention? restricted (M11/M12): x·p only for degree(p) < d — corresponds to the formal standard degree. full: x·p also at degree(p) = d if x occurs in every monomial of highest degree of p (multilinear with variable rule); deviates from the formal degree by at most 1 downward. (The semantically even stronger rule “times an arbitrary polynomial in the quotient ring” is not used.) Validation: exactly equal to an independent Python reference on 48 small cores; 57 satisfiable formulas never refuted. Checks: aborts restr/full 0/4; “full > restr” 0; soundness full rule 614/614; XOR clause core restr 3:379 4:6 → full 3:382 4:3; Tseitin 3:30 → 3:30.

Overall: of 232 cores “≥ 5”, 182 stay “≥ 5” also under the full rule (78 %); the full rule generated additional rows in 226 of these cores (the rule applies but is not enough). No degree-4 core drops to 3.

n) m13_durchlass.py — BDD compressibility of the solution space [measurement]

n = 12–28 · tdnb1 · seed 13, 60 instances, 12 960 tasks, 8.8 min

Measure: exact reduced BDD of the whole solution set (minimum over 6 variable orders) divided by the BDD of a truly random set of the same size (“ratio”; 1 = as disordered as random). Types: 3sat (7 of 8 patterns allowed), rel6/rel5/rel4 (6/5/4 allowed, forbidden patterns random), xor3 (4 allowed, affine), sat2, later horn3 (7 allowed, ordered, same clause count as 3sat). Densities 0.3–0.9 of the own threshold (rel thresholds estimated). Self-test against full enumeration error-free. Ratio at fixed space fraction log₂S/n ∈ [0.5; 0.7), median:

At [0.3; 0.5): 3sat 0.419/0.258/0.173/0.109/0.071; xor3 0.412/0.167/0.103/0.051/0.026 (ratio 1.0 → 2.7).

• Order 7 > 6 > 5 > 4 allowed strictly monotone; the gap between 3-SAT and all others grows with n (3sat/xor3 at [0.5; 0.7): 1.7 → 15.5).
• [correction] Confounder: a 3-SAT clause cuts 0.19 bit, a rel4/XOR constraint 1 bit; for equal volume 3-SAT needs about five times as many random clauses (n = 24: 72 versus 13).
• [correction] Horn lies practically on 3-SAT (deviation a few percent in every row), although Horn is trivially solvable. The BDD ratio measures asymmetry and clause count, not hardness.
• [correction] XOR lies above rel4: the BDD does not see Gauss (an affine space is often expensive for a BDD, tiny for a vector basis). BDD compressibility is one particular description language, not compressibility as such.
• For 3-SAT too the ratio falls with n: the strong version (“solution space as random as random”) does not hold.
• Conclusion: the compressibility that decides between easy and hard is not general description length but the idiomatic one (closure under an operation) → § 3p.
• The DP block of M13 (Davis–Putnam on unsatisfiable instances at factor 1.5, n up to 20) ran only partially (many timeouts at n = 20) and is not reported.

o) m14_dichte.py — density sweep [measurement]

tdnb1 · seed 14, 60 instances, 17 280 tasks · pebble n = 10–16 (kmax 5, older file version); follow-up “m14k”: n = 16/20/24, kmax 6

Two measures: DPLL nodes (unit propagation, no learned clauses; satisfiable and unsatisfiable) and the pebble number k*: smallest k at which strong k-consistency removes the empty assignment (Spoiler wins the existential k-pebble game; by Atserias–Dalmau this corresponds to resolution width). Density 0.5–8 of the own threshold. Self-test error-free. DPLL nodes 3-SAT (median):

XOR: peak flatter (n = 50: factor 1.15 → 15 nodes); rel5: peak just below the estimated threshold (n = 50: 20 nodes at 0.7–0.85). Pebble number k* (unsatisfiable instances, median):

• 3-SAT: n ≤ 16: 4 at factor 0.85–1.15, from 1.3 consistently 3. Follow-up: factor 1.3 at n = 16/20/24: 4/4/4; factor 1.6: 3/3/4; factor 2.0: 3/3/3.
• XOR: 4 from factor 1.0 to 2.0 (n = 16/20/24 consistently 4), from 3.0 then 3.
• rel5: 3 everywhere, also at the threshold. k* > 4 never occurred.

Limits: k* has only the steps 3 and 4 at n ≤ 24; “high density” here means high density in α, not the n^1.4 regime.

p) m15_abschluss.py — closure of the solution space [measurement]

n = 12–28 · tdnb1 · seed 15, 60 instances, factors 0.3–0.9, 7200 tasks, 0.6 min

For each satisfiable instance draw solutions uniformly (exactly from the BDD) and apply bitwise AND, OR, majority, minority (x⊕y⊕z); fidelity = share with which the result is again a solution (distinct, non-trivial tuples only). Baseline: random set of the same size (practically 0). Self-test: drawing exact and uniform; polymorphism controls = 1. Share of instances with exactly closed operation:

Best fidelity per instance (median): 3sat 0.710/0.720/0.649/0.604/0.569 (n = 12/16/20/24/28); horn3, sat2, xor3 consistently 1.000; rel5 0.887 → 0.761; rel4 1.000 → 0.888. 3-SAT at space fraction [0.5; 0.7): AND 0.306 → 0.155, OR 0.339 → 0.128, majority 0.648 → 0.516, minority 0.118 → 0.007 (n = 12 → 28).

q) m15b_defekt.py — defect per clause [measurement]

n = 12–28 · Claude’s sandbox, 1 core · seed 15, 20 instances, factors 0.3–0.9, 4487 measurement rows · script not yet filed

Per instance and operation: ε_c = share of tuples whose result violates clause c; prediction under independent defects T_pred = ∏(1 − ε_c). Types 3sat, rel5, horn3. 3-SAT, majority:

Controls: horn3 AND: ε = 0 in every clause, T = 1 for all n. horn3 majority: ε ≈ 0.0033 constant, T 0.915 → 0.800, T/prediction 1.01. rel5 majority: ε ≈ 0.006, T/prediction 1.00. For AND/OR/minority on 3-SAT, T/prediction is 1.2–2.1 (defects pile up on the same tuples).

• For majority the product model holds almost exactly: the defects are independent.
• ε is constant ≈ 0.01 from n = 16; with m ≈ α·n this gives T ≈ e^−0.01·m, at the threshold a halving about every 16 variables. [extrapolation, not measured] At n = 100 about 1 %.
• Elementary anchor: if the three solutions at a clause were independently uniformly distributed over the 7 allowed patterns, majority violates it with probability 6/343 ≈ 0.0175 (exactly when the three inputs are the three patterns with one true literal each). Measured 0.010–0.015, because real solutions are correlated.
• What decides is not small-or-large but whether some operation has ε = 0 (Horn also has ε > 0 under majority, but 0 under AND).
• Limit: shows quantitatively that 3-SAT instances carry no idiomatic rule; does not show that no other fast algorithm exists (§ 1b).

r) Overview M11–M15b [measurement]

The affine route at a glance [measurement]

n ≤ 20

Place in the literature

The three-way split as a coherent classification is not documented as known in this form; each level, however, has an established research field.

The verification grades [V]/[A]/[S]/[N] and the full text on the state of the literature (beweisgeruest.md, beweisgeruest.bib, luecken.md) are not yet in the repo; the subpage “Proof scaffold / state of the literature” is therefore [pending]. The sources above come from the brief of October 8 and have not been individually checked here.

By Schaefer, 3-SAT as a language has none of the closure properties that yield a level-2 shortcut in the algebraic sense. What remains open is only whether a class-wide shortcut exists beyond that — which is P vs NP itself. [open]

Open points

• [pending] Detour factor as an M5 column, measured below the threshold (α ≈ 3.8–4.1).
• [pending] Splitting “nearly affine” (fit ≥ 0.5) into trivial and genuine cases.
• [pending] Count indep for XOR per equation instead of per clause — a clean synergy quantity.
• [pending] Larger samples (M6 with 200 instances) and a longer time cap (60 s) for n = 18–20.
• [pending] Further algebraic routes besides the affine one.
• [open] The remaining ≈ 2 % of genuinely affine 3-SAT instances: limit 0 or positive?
• [pending] Explain the coupling movement ↔ DP cost for satisfiable instances (§ 3f).
• [pending] Measure core tightness order-free (krit instead of MUS size) and check against NS degree.
• [pending] Polynomial Calculus degree instead of NS degree; check the literature on PC degree bounds for random 3-CNF before claiming anything about it.
• [pending] 3-SAT cores with more than 21 variables (needs MUS extraction without brute force), to continue the Tseitin comparison up to 36 variables.
• [pending] DP comparison additionally in idx order (strictly idiomatic).
• [open] Transfer “instance is incompressible” → “every proof is long” to strong systems (Frege), see § 1a.
• [open] Outcome “same” in § 3a: whether 3-SAT has a shortcut beyond the routes measured remains untouched by it.
• [open] The upper storey: “fast forces idiomatic” (§ 1b) — equivalent to P ≠ NP for 3-SAT.
• [open] Frege, bounded-depth Frege, DAG-Res(⊕) on random 3-CNF of linear density.
• [pending] M15b on the server with 60 instances and n up to 36; explain ε directly from the solution space against 6/343 and against the correlation of the solutions.
• [pending] Pebble number at n = 28/32 (expected: k* = 5 first at the threshold).
• [pending] PC degree 5 exactly on large cores (--dmax 5, few jobs, large --mem); runtime split by 4 vs. ≥ 5; position of the XOR fours by n.
• [pending] Renewed M12 run with the current m12_grosskern.py (expansion block: expansion against 4/≥ 5).
• [pending] M13 DP block with a longer time cap or without n = 20.
• [pending] Subpage “Proof scaffold / state of the literature” and downloads m15b_defekt.py, ref_voll.py: files are not in the repo, to be supplied.
• Done by M11: “Polynomial Calculus degree instead of NS degree” (point above). The older points remain valid.

Corrections [correction]

Earlier versions are not silently overwritten. What changed relative to the state of October 6, 2026: