Formulation · random 3-SAT at the threshold

SAT Without AND and OR

A clause does not say “one of three holds”. Literally it says: this one corner pattern is forbidden. Unrolling AND and OR all the way leaves a list of forbidden blocks in the cube — and three measurements that the usual notation cannot even phrase.

As of September 3, 2026

1 AND and OR are not axioms

Explain (a OR b OR c) to a five-year-old and you say: look at them one after another; as soon as one holds you are done. That is not a primitive — it is a loop with a stopping value. AND is the same sentence with the stopping value swapped. So both can be programmed out rather than assumed.

Seven levels, each executable, all seven checked against each other on 72 320 assignments without a single disagreement:

Level	What it says	What it uses
0	the abstraction	`all(any(…))`
1	quantifiers	THERE IS / FOR ALL
2	walk with a stop value	loop, comparison, break
3	one fold	AND and OR differ in exactly three numbers
4	counting	how many literals hold
5	arithmetic	one product per clause, one sum over them
6	bit mask	`(p & fixed) == value`

Two things fall out that the abstraction had hidden. Level 4 produces the height d — the number of violated clauses, a quantity AND/OR cannot express because they only distinguish satisfied from not. And level 6 is the block picture: it was never chosen as an alternative view, it is simply what remains.

View code & data — the seven levels and their agreement

aufgerollt.py

def ebene0(klauseln, v):                 # die Abstraktion
    return all(any(literal_wert(l, v) for l in c) for c in klauseln)

def falte(werte, start, verknuepfen, abbruch):
    """Der gemeinsame Kern.  ODER und UND sind DERSELBE Code.

    ODER = falte(werte, start=0, verknuepfen=groesser, abbruch=1)
    UND  = falte(werte, start=1, verknuepfen=kleiner,  abbruch=0)
    """
    e = start
    for w in werte:
        e = verknuepfen(e, w)
        if e == abbruch:
            break
    return e

def ebene6(bloecke, p):                  # eine Bitmaske, sonst nichts
    for fest, wert in bloecke:
        if (p & fest) == wert:
            return False
    return True

output

$ python3 aufgerollt.py

Eine Klausel, sieben Mal dasselbe.   Klausel [-1, 2, -3]   Belegung [1, 0, 1]

  Ebene 0  Abstraktion    any(literal_wert(l, v) for l in c)      -> False
  Ebene 1  Quantor        ES GIBT ein Literal, das stimmt         -> False
  Ebene 2  Durchlauf      lauf durch, brich ab sobald eines stimmt-> False
  Ebene 3  Faltung        falte(werte, 0, groesser, abbruch=1)    -> 0
  Ebene 4  Zaehlen        Trefferzahl > 0 ?                       -> 0 Treffer
  Ebene 5  Arithmetik     Produkt der (1 - wert) == 0 ?           -> Produkt = 1
  Ebene 6  Bitmaske       fest=111 wert=101 p=101                 -> True

Sieben Ebenen, 200 Instanzen, 72320 Belegungen: einig
Vier Halbringe, 40 Instanzen, gegen unabhaengige Rechnung: einig

Und derselbe Auswerter mit vier Halbringen, an einem Beispiel:
    Boolesch  -> loesbar?                                    = 1
    Zaehlen   -> wieviele Loesungen                          = 13
    min-plus  -> Hoehe d (kleinste Zahl verletzter Klauseln) = 0
    max-plus  -> MaxSAT (groesste Zahl erfuellter Klauseln)  = 40

200 random instances, n ∈ {6,8,10}, α ∈ {2.0, 4.26, 6.0}; every level evaluated on every one of the 2^n assignments.

2 One program, four meanings

If AND and OR differ in only three numbers, replacing those numbers by two other operations makes the same program compute something else. A pair (plus, times) with neutral elements is a semiring. Four of them, one evaluator, each checked against an independent computation:

Semiring	Z = ⊕_assignments ⊗_clauses	Example
(max, min)	is there a solution?	1
(+, ×)	how many solutions	13
(min, +)	height d — fewest violated clauses	0
(max, +)	MaxSAT — most satisfied clauses	40

The loop knows nothing about any of this.

View code & data — one evaluator, four semirings

aufgerollt.py

HALBRINGE = {                    # (plus, mal, null, eins, wert_einer_klausel)
    "Boolesch -> loesbar?":     (groesser, kleiner, 0, 1, lambda e: 1 if e else 0),
    "Zaehlen  -> #Loesungen":   (add,      mul,     0, 1, lambda e: 1 if e else 0),
    "min-plus -> Hoehe d":      (kleiner,  add,   inf, 0, lambda e: 0 if e else 1),
    "max-plus -> MaxSAT":       (groesser, add,  -inf, 0, lambda e: 1 if e else 0),
}

def auswerten(n, klauseln, halbring):
    """EIN Programm.  Die Bedeutung steckt allein im Halbring."""
    plus, mal, null, eins, klauselwert = halbring
    z = null
    for p in range(1 << n):                       # alle Belegungen
        v = [(p >> i) & 1 for i in range(n)]
        t = eins
        for c in klauseln:                        # alle Klauseln
            t = mal(t, klauselwert(erfuellt(c, v)))
        z = plus(z, t)
    return z

output

$ python3 aufgerollt.py

Eine Klausel, sieben Mal dasselbe.   Klausel [-1, 2, -3]   Belegung [1, 0, 1]

  Ebene 0  Abstraktion    any(literal_wert(l, v) for l in c)      -> False
  Ebene 1  Quantor        ES GIBT ein Literal, das stimmt         -> False
  Ebene 2  Durchlauf      lauf durch, brich ab sobald eines stimmt-> False
  Ebene 3  Faltung        falte(werte, 0, groesser, abbruch=1)    -> 0
  Ebene 4  Zaehlen        Trefferzahl > 0 ?                       -> 0 Treffer
  Ebene 5  Arithmetik     Produkt der (1 - wert) == 0 ?           -> Produkt = 1
  Ebene 6  Bitmaske       fest=111 wert=101 p=101                 -> True

Sieben Ebenen, 200 Instanzen, 72320 Belegungen: einig
Vier Halbringe, 40 Instanzen, gegen unabhaengige Rechnung: einig

Und derselbe Auswerter mit vier Halbringen, an einem Beispiel:
    Boolesch  -> loesbar?                                    = 1
    Zaehlen   -> wieviele Loesungen                          = 13
    min-plus  -> Hoehe d (kleinste Zahl verletzter Klauseln) = 0
    max-plus  -> MaxSAT (groesste Zahl erfuellter Klauseln)  = 40

40 instances; each semiring compared against an independent brute-force computation of the same quantity. No deviations.

3 The ignition density is width-invariant

Two Attractors showed that bounded-width saturation tips rather than degrades, and Where Asymptopia Begins showed width 3 carries to n ≈ 55. The block view adds the accounting for why widening the layer does not help.

Two width-3 blocks merge back to width ≤ 3 only if they share at least two places. Those are the ignition points. Level w has O(n^w2^w) places. Ignition density × n³, median over 10 instances:

n	w = 3	w = 4	w = 5	w = 6
32	62.8	64.4	5.6	0.6
48	61.1	62.5	3.5	0.2
64	65.2	63.3	2.6	0.1
96	60.9	63.2	1.7	0.1
128	62.6	62.3	1.3	0.0

Level 4 has fifteen times the seed of level 3 at n = 32 (1 214 against 80) and a fifteen times larger stock. It cancels, to two digits, across the whole measured range. And from level 5 it gets worse: the seed saturates — two width-3 blocks with one conflicting place share that place, so every possible merge lands on level 4 anyway — while the stock keeps growing as n^w. Widening adds no ignition point, only room.

4 The seed is readable before the run

Two Attractors measures the branching factor during saturation. The same quantity is available beforehand, from the clause list alone, in O(m²) — no closure required.

20 unsatisfiable instances at n = 56; cheap quantities (0 s) against the expensive question of whether the closure ignites (up to 1 217 s):

Quantity	AUC	median igniting	median starving
seed	0.91	95	79
λ₁	0.91	0.38	0.33
λ₂	0.86	0.90	0.65
λ₃	0.85	1.06	0.68
degree spread	0.83	13.0	10.5
largest degree	0.58	22	21

Nine ignite, eleven starve. Of two instances of the same size, the one with more ignition points ignites in nine cases out of ten — so the mechanism is not an ensemble artefact. Practically: decide in O(m²) whether the polynomial method is worth running at all.

And a partial no: λ = 1 does not work as a parameter-free criterion in this round-wise form. Instance #19 has λ₃ = 1.05 and starves, #18 has 1.31 and ignites. The state-dependent formulation in Two Attractors — R as a function of the accumulated closure — is the better one.

View code & data — the seed, and what it predicts

werkbank.py

def saat(bloecke, w=3):
    """Zuendpunkte: Paare, deren Verschmelzung wieder Breite <= w hat.

    Nur diese koennen die Lawine anstossen.  O(m^2), kein Abschluss noetig.
    """
    v = 0
    for i in range(len(bloecke)):
        for j in range(i + 1, len(bloecke)):
            r = verschmelzen(bloecke[i], bloecke[j])
            if r is not None and breite(r) <= w:
                v += 1
    return v

output — instanzweise.py 56 20

  # 2  Saat   91  lam [0.38, 0.91, 0.86]  ->  ZUENDET bei |228033| nach 32 Runden  (331s)
  # 3  Saat   81  lam [0.34, 0.53, 0.67]  ->  stirbt  bei |446|    nach 11 Runden  (0s)
  # 5  Saat  110  lam [0.46, 1.21, 0.91]  ->  ZUENDET bei |228033| nach 24 Runden  (1217s)
  # 8  Saat   64  lam [0.27, 0.34, 0.36]  ->  stirbt  bei |338|    nach  5 Runden  (0s)
  #18  Saat   76  lam [0.32, 0.68, 1.31]  ->  ZUENDET bei |221982| nach 39 Runden  (242s)
  #19  Saat   92  lam [0.38, 1.01, 1.05]  ->  stirbt  bei |913|    nach 18 Runden  (0s)

  9 zuenden, 11 sterben.
    Saat             AUC 0.91   Median zuendend 95.00  sterbend 79.00
    lambda_1         AUC 0.91
    lambda_2         AUC 0.86
    lambda_3         AUC 0.85
    Gradstreuung     AUC 0.83
    groesster Grad   AUC 0.58

6 of 20 rows shown. n = 56, α = 4.26, unsatisfiable only. The seed costs 0 s, the closure up to 1 217 s.

5 The conflict graph: a structural route, and it is dominated

Blocks are jointly compatible exactly when they are pairwise compatible — for subcubes the partial assignments simply merge (3 000 samples, 0 deviations). So the consistent families are exactly the independent sets of the clause conflict graph, and the whole inclusion–exclusion series is its volume-weighted independence polynomial. That graph has 4.26n vertices at mean degree 19.0, constant from n = 16 to 256.

This suggests tractability by structure rather than by operation: small treewidth of the conflict graph would make the solution count polynomial. Measured (min-fill bound, conflict / primal):

family	n=32	n=64	n=96	satisfiable
random p=0.5	75 / 22	149 / 44	227 / 65	mixed
skewed p=0.15	35 / 22	73 / 44	108 / 66	1.00
local W=8	46 / 13	52 / 13	49 / 13	0.00
local W=16	70 / 21	99 / 26	104 / 26	0.00
local+skewed	21 / 12	21 / 13	20 / 13	1.00

The region sought — conflict graph narrow, primal graph wide — is empty, and it cannot be otherwise: 4.26n vertices at the same density against n vertices. Where the conflict graph is narrow the primal one is narrower, by 2³⁶ at n = 96. The reformulation stays correct and explanatory — it gives the third independent derivation of the 2^1.57n series cost — but as a method it is dominated.

6 What is new here, and what is not

This report was built by reconstructing the block formulation from scratch, without reading the existing corpus first. Several findings turned out to be re-derivations, and they are credited where they belong:

result	already in
the ignition spark: pairs sharing two places	Why the saturation recipe starves (ZUENDUNG)
the edge at n ≈ 48	Two Attractors — there n = 49.2, computed rather than measured
bistability of the closure	Two Attractors
the branching factor	Two Attractors, and in a better form
width 3 carries to n ≈ 55	Where Asymptopia Begins

New is what stands in sections 1–5: the block vocabulary carried through, the seven levels and the semiring, the width-invariance of the ignition density, the seed as an a-priori quantity, and the conflict graph. That the same structure produces the same findings speaks for the findings and against the procedure.

A workbench comes with it. werkbank.py holds an instance as a list of forbidden blocks and exposes both grips separately, together with seed, stock, ignition density, closure, decision, stepwise data collection and the polymorphism test:

from werkbank import Instanz
I = Instanz.zufall(n=20, alpha=4.26, saat=1)   # or .aus_dimacs("x.cnf")
print(I.bericht())