k-SAT · Cartography · August 25, 2026

Map of the Instance Space

Not the solution space, but the space of all instances. Satisfiability is a monotone function on it — so the space has a boundary, a height, and a local geometry. All three are measured exactly. And yet membership cannot be computed; there is a measured reason for that too.

Exact over the complete cube, n = 10 … 22 · instanzraum.py · randnaehe.py

6,528

dimensions at n = 18

monotone

adding a clause can only flip SAT→UNSAT

95 %

are 1 clause from the opposite set

C(b,3)

killing single clauses, exact

1 · The space is a lattice, not a haze

With n variables there are 8·C(n,3) possible clauses — triples times sign patterns. An instance is a subset of these, so the instance space is the cube {0,1}^8·C(n,3). At n = 18 that is 6,528 dimensions.

A single fact orders the whole thing: adding a clause can only flip SAT → UNSAT, never back.

The UNSAT set is upward closed — a filter.
The SAT set is downward closed — an ideal.
The boundary is the antichain of minimally unsatisfiable formulas.
The transition at α = 4.267 is a sharp threshold of a monotone property — the setting in which Friedgut's theorem holds.

2 · A cross-section through the space

6,528 dimensions can't be drawn — a two-dimensional cross-section can. Two independent clause streams A and B; the cell at position (i, j) is the instance made of the first i clauses of A and the first j of B. So moving right and up adds clauses.

Because satisfiability is monotone, the solvable region must be connected in the bottom-left corner and the boundary must be a staircase that never runs backward. That is exactly what is seen — and the staircase is ragged, not smooth.

n = 18 · 81 × 81 grid · 6,561 instances solved individually and exactly

clauses from stream B →

clauses from stream A →

Move the pointer over the map.

The dashed diagonal is i + j = 77, i.e. α = 4.26 — the threshold. It crosses the staircase roughly where it runs, but not along it: the same clause count does not mean the same answer.

Check: d never grows backward along either axis — checked on all 6,561 cells. Monotonicity is thus not asserted but verified by computation.

3 · Why the coordinate can't be computed

If the space is ordered this cleanly — why can't one just compute the coordinates of an input instance and check whether it lies in the region? Because there are exactly two kinds of coordinates, and nothing in between.

Cheap coordinates

α, degree distribution, imbalance, front width, tree width. Computable in polynomial time — but the boundary is not a level set of any of them. Two instances can agree on every one of these numbers and still answer differently.

Exact coordinates

d, backbone, solution count. They determine membership — but computing them is at least as hard as the problem itself. Checking d = 0 is SAT.

Nothing lies between them, and that is not a lack of effort: a cheap coordinate whose level set was the boundary would be a polynomial-time algorithm for SAT. The question "why not just compute the coordinate" is the P-versus-NP question in coordinate form.

The geometric reason behind this is measurable. At the threshold, neither of the two sets has an interior:

Distance to the opposite set in clauses · n = 18 · 150 instances each
α	type	share	distance 1	distance 2+	mean distance
3.50	SAT	98 %	52 %	48 %	1.48
4.00	SAT	85 %	91 %	9 %	1.09
4.26	SAT	67 %	95 %	5 %	1.05
4.26	UNSAT	33 %	96 %	4 %	1.04
5.00	UNSAT	67 %	85 %	15 %	1.15
6.00	UNSAT	95 %	33 %	67 %	1.80

At α = 4.26, 95 % of the solvable instances lie a single clause away from the unsolvable set — and 96 % of the unsolvable ones a single clause away from the solvable set. There is no interior at the threshold to be inside of. The boundary is everywhere.

solvable unsolvable

500 instances at n = 18, α = 4.26, plotted against the two strongest cheap structural measures in this project. The degree variance is 10.873 (solvable) versus 10.889 (unsolvable) — the clouds sit on top of each other.

4 · The boundary, and how it sharpens with n

n = 10 n = 14 n = 18 n = 22 α = 4.267

The distance α_c(n) − 4.267 falls 0.719 → 0.524 → 0.447 → 0.276, the width from 1.879 to 1.599. Both fit n^−1/ν with 1/ν ≈ 0.8.

Share of solvable instances · exact · 600 / 600 / 400 / 150 instances per cell
n	3.00	3.50	4.00	4.26	4.50	5.00	5.50	6.00	α_c(n)	width
10	1.00	0.96	0.85	0.75	0.67	0.49	0.32	0.22	4.986	—
14	1.00	0.97	0.85	0.73	0.66	0.39	0.23	0.11	4.791	—
18	1.00	0.97	0.84	0.73	0.61	0.35	0.13	0.04	4.714	1.879
22	1.00	0.98	0.83	0.64	0.53	0.22	0.05	0.02	4.543	1.599

5 · The height above the boundary

d(F) = min over all assignments of the number of violated clauses

d = 0 means solvable. And d is at the same time the smallest number of clauses that must be struck for F to become solvable — the distance to the boundary in the deletion metric. A genuine height function: monotone under addition, zero exactly on the ideal.

n = 10 n = 14 n = 18 n = 22

d/n is intensive: at α = 12 we measure 0.515 / 0.514 / 0.498 / 0.503 — the same number across a doubling of n.

6 · The local geometry: how sharp is the boundary?

Upward from the SAT side

An added clause makes F unsatisfiable exactly when all solutions violate it — that is, when all solutions carry the same pattern on its three variables. Those are exactly the triples from the backbone, one sign pattern per triple.

killing clauses = C(b, 3)

Downward from the UNSAT side

The critical clauses: removing them makes it solvable. Exactly the clauses that are the sole violator of some point of the cube — the exit from the filter, one edge deep.

exits = #{c : ∃x, c is the sole violator}

Verifying the formula · all 960 clauses at n = 10 appended and checked individually
α	solutions	backbone b	C(b,3)	raw count	match
3.00	27	0	0	0	yes
4.00	8	3	1	1	yes
4.26	7	3	1	1	yes
4.60	3	4	4	4	yes

from SAT upward (share of all 6,528 clauses) from UNSAT downward (share of the instance's own clauses)

n = 18, 120 instances each. From below the boundary becomes ever sharper, from above ever thicker. The driver is the backbone: 0.05·n at α = 3, 0.84·n at α = 5.

7 · What the map says

The instance space is ordered, not diffuse. Monotonicity gives it a filter, an ideal, and a boundary antichain — and turns the threshold phenomena into theorems instead of observations.
There is a natural height. d is at once the deletion distance to the boundary and the MAXSAT deficit, and d/n is intensive.
But there is no interior. At the threshold, 95 % of instances lie one clause from the opposite set. A region without an interior cannot be bounded by coordinates.
And hardness isn't on this map at all. d, backbone, boundary distance — all properties of the instance, all cleanly ordered, and none of them says how long a solver will take.

instanzraum.py · randnaehe.py · INSTANZRAUM.md

View code & data — boundary P(solvable) and height d over α and n

instanzraum.py — boundary and height over the complete cube

"""The INSTANCE SPACE instead of the solution space.

An instance is a subset of the 8*C(n,3) possible clauses. The space is thus
the cube {0,1}^(8*C(n,3)) -- and satisfiability is a MONOTONE function on it:
adding a clause can only flip SAT->UNSAT, never back.

This means:
  * the UNSAT set is upward closed (a filter),
  * the SAT set is downward closed (an ideal),
  * the boundary is the antichain of minimally unsatisfiable formulas,
  * and there is a natural HEIGHT above the boundary:

      d(F) = min over all assignments of the number of violated clauses

  d = 0 exactly when F is solvable. d is at the same time the smallest
  number of clauses that must be struck to make F solvable -- i.e. the exact
  distance to the boundary in the deletion metric. (MAXSAT deficit.)

A  The boundary: P(solvable) over alpha, and how sharp it gets with n.
B  The height: d and d/n over alpha and n.
C  The degeneracy: how many assignments reach the minimum.
"""
import sys
import numpy as np
from streichliste import bits, rand_cnf, maske, K

def hoehe(n, B, vs, sg):
    """(d, degeneracy) -- d = min number of violated clauses.
    The violating region of a clause is a subcube: reshaped as a (2,)*n
    array that is a slice, so O(2^(n-k)) instead of O(2^n)."""
    kc = np.zeros((2,) * n, dtype=np.int16)
    leer = [slice(None)] * n
    for c in range(len(vs)):
        idx = list(leer)
        for j in range(K):
            idx[int(vs[c, j])] = 0 if sg[c, j] else 1
        kc[tuple(idx)] += 1
    d = int(kc.min())
    return d, int((kc == d).sum())

def teilA(ns, alphas, proben, seed=151):
    if not isinstance(proben, dict):
        proben = {n: proben for n in ns}
    print("== A  Der Rand: P(loesbar) ueber alpha")
    print(f"{'n':>4} " + " ".join(f"{a:>7.2f}" for a in alphas)
          + f" {'a_c(n)':>8} {'Breite':>8}")
    tab = {}
    for n in ns:
        rng = np.random.default_rng(seed + n)
        B = bits(n)
        ps = []
        pn = proben[n]
        for a in alphas:
            m = round(a * n)
            s = 0
            for _ in range(pn):
                vs, sg = rand_cnf(n, m, rng)
                d, _ = hoehe(n, B, vs, sg)
                s += (d == 0)
            ps.append(s / pn)
        tab[n] = ps
        p = np.array(ps); aa = np.array(alphas)
        def kreuz(ziel):
            for i in range(len(p) - 1):
                if p[i] >= ziel >= p[i + 1]:
                    t = (p[i] - ziel) / max(p[i] - p[i + 1], 1e-9)
                    return aa[i] + t * (aa[i + 1] - aa[i])
            return float('nan')
        ac, hi, lo = kreuz(0.5), kreuz(0.9), kreuz(0.1)
        print(f"{n:>4} " + " ".join(f"{v:>7.2f}" for v in ps)
              + f" {ac:>8.3f} {lo-hi:>8.3f}")
    return tab

def teilBC(ns, alphas, proben, seed=163):
    if not isinstance(proben, dict):
        proben = {n: proben for n in ns}
    print("\n== B/C  Die Hoehe ueber dem Rand: d = min verletzte Klauseln")
    print(f"{'n':>4} {'alpha':>6} {'m':>5} {'P(d=0)':>8} {'d Mittel':>9} "
          f"{'d/n':>8} {'d Median':>9} {'Entartung bei d':>16}")
    for n in ns:
        rng = np.random.default_rng(seed + n)
        B = bits(n)
        for a in alphas:
            m = round(a * n)
            ds, gs = [], []
            for _ in range(proben[n]):
                vs, sg = rand_cnf(n, m, rng)
                d, g = hoehe(n, B, vs, sg)
                ds.append(d); gs.append(g)
            ds = np.array(ds)
            print(f"{n:>4} {a:>6.2f} {m:>5} {(ds==0).mean():>8.2f} "
                  f"{ds.mean():>9.2f} {ds.mean()/n:>8.4f} {np.median(ds):>9.0f} "
                  f"{np.mean(gs):>16.1f}")

# ---------------------------------------------------------------- D
def lokale_geometrie(n, vs, sg):
    """How many SINGLE clause changes flip the answer?

    Upward from the SAT side: an added clause makes F unsatisfiable exactly
    when ALL solutions violate it -- i.e. when all solutions carry the same
    pattern on its three variables. Those are exactly the triples from the
    BACKBONE (variables on which all solutions agree), one sign pattern per
    triple:

        number of killing clauses  =  C(b, 3)     with b = backbone size.

    Downward from the UNSAT side: the critical clauses (removing them makes
    it solvable) -- the points that are violated only by this one clause.
    """
    from math import comb
    kc = np.zeros((2,) * n, dtype=np.int16)
    ks = np.zeros((2,) * n, dtype=np.int32)
    leer = [slice(None)] * n
    for c in range(len(vs)):
        idx = list(leer)
        for j in range(K):
            idx[int(vs[c, j])] = 0 if sg[c, j] else 1
        kc[tuple(idx)] += 1
        ks[tuple(idx)] += c + 1
    kcf = kc.ravel(); ksf = ks.ravel()
    N = 1 << n
    if (kcf == 0).any():                                   # solvable
        loes = np.flatnonzero(kcf == 0)
        b = 0
        for v in range(n):
            bit = (loes >> v) & 1
            if bit.min() == bit.max():
                b += 1
        return "SAT", len(loes), b, comb(b, 3), 8 * comb(n, 3)
    einzig = ksf[kcf == 1]
    krit = int((np.bincount(einzig, minlength=len(vs) + 1)[1:] > 0).sum())
    return "UNSAT", 0, 0, krit, len(vs)

def teilD(ns, alphas, proben, seed=181):
    from math import comb
    print("\n== D  Lokale Geometrie des Randes: kippende Einzelaenderungen")
    print(f"{'n':>4} {'alpha':>6} {'Art':>6} {'Anteil':>7} {'Rueckgrat b':>12} "
          f"{'b/n':>7} {'kippende Richtungen':>20} {'von':>9} {'Anteil':>9}")
    for n in ns:
        rng = np.random.default_rng(seed + n)
        for a in alphas:
            m = round(a * n)
            S, U = [], []
            for _ in range(proben):
                vs, sg = rand_cnf(n, m, rng)
                art, nl, b, kipp, ges = lokale_geometrie(n, vs, sg)
                (S if art == "SAT" else U).append((b, kipp, ges))
            for art, L in (("SAT", S), ("UNSAT", U)):
                if not L:
                    continue
                b = np.mean([x[0] for x in L]); kp = np.mean([x[1] for x in L])
                ge = np.mean([x[2] for x in L])
                print(f"{n:>4} {a:>6.2f} {art:>6} {len(L)/proben:>7.0%} "
                      f"{b:>12.1f} {b/n:>7.3f} {kp:>20.1f} {ge:>9.0f} "
                      f"{kp/max(ge,1):>9.2%}")

if __name__ == "__main__":
    w = sys.argv[1] if len(sys.argv) > 1 else "alle"
    A = [3.0, 3.5, 4.0, 4.26, 4.5, 5.0, 5.5, 6.0]
    if w in ("alle", "A"): teilA([10, 14, 18, 22, 26], A,
                                 {10: 600, 14: 600, 18: 400, 22: 150, 26: 40})
    if w in ("alle", "B"): teilBC([10, 14, 18, 22], [3.0, 4.26, 5.0, 6.0, 8.0, 12.0],
                                  {10: 300, 14: 300, 18: 200, 22: 80})
    if w in ("alle", "D"): teilD([14, 18], [3.0, 4.0, 4.26, 4.6, 5.0], 120)

python3 instanzraum.py B — live output, exact over 2ⁿ (n up to 22)


== B/C  Die Hoehe ueber dem Rand: d = min verletzte Klauseln
   n  alpha     m   P(d=0)  d Mittel      d/n  d Median  Entartung bei d
  10   3.00    30     0.99      0.01   0.0010         0             18.5
  10   4.26    43     0.74      0.26   0.0260         0              6.7
  10   5.00    50     0.54      0.49   0.0493         0              4.8
  10   6.00    60     0.19      1.07   0.1067         1              3.7
  10   8.00    80     0.03      2.25   0.2250         2              3.0
  10  12.00   120     0.00      5.15   0.5150         5              2.2
  14   3.00    42     1.00      0.00   0.0002         0             56.3
  14   4.26    60     0.73      0.27   0.0195         0             10.4
  14   5.00    70     0.42      0.65   0.0462         1              7.7
  14   6.00    84     0.12      1.40   0.0998         1              5.7
  14   8.00   112     0.01      3.12   0.2226         3              3.7
  14  12.00   168     0.00      7.19   0.5136         7              2.7
  18   3.00    54     1.00      0.00   0.0000         0            188.5
  18   4.26    77     0.70      0.30   0.0169         0             19.1
  18   5.00    90     0.39      0.77   0.0425         1             11.3
  18   6.00   108     0.09      1.62   0.0903         2              6.6
  18   8.00   144     0.00      3.78   0.2100         4              4.6
  18  12.00   216     0.00      8.96   0.4978         9              2.8
  22   3.00    66     1.00      0.00   0.0000         0            647.6
  22   4.26    94     0.64      0.36   0.0165         0             38.1
  22   5.00   110     0.23      0.94   0.0426         1             13.9
  22   6.00   132     0.04      1.90   0.0864         2              9.1
  22   8.00   176     0.00      4.76   0.2165         5              6.9
  22  12.00   264     0.00     11.06   0.5028        11              4.2

exact over the complete cube August 25, 2026