← back to the board
[[12,2,4]] d =
n
12
k
2
d
4
kd²/n
2.667
w
6
X/Z
1
g
0.0631
r
3.6056
layers
1
swaps
13

Share this result

Distance

X/Z asymmetry 1 · d_X = 4, d_Z = 4 · w_X = 6, w_Z = 6 (max(d_X,d_Z)/min(d_X,d_Z); each side carries its own earned tier: = certified exact, ≤ witness upper bound)
d_X 4 · witness weight 4 (claimed upper_bound)
witness operator (support, 4 qubits)
[0, 1, 3, 6]
d_Z 4 · witness weight 4 (claimed upper_bound)
witness operator (support, 4 qubits)
[0, 3, 6, 8]
certificate exact, d = 4 · CryptoMiniSat 5.14.7 SAT
X: no logical < 4 exists; Z: no logical < 4 exists

Diagnostics

computed by the verifier from the parity checks, the layout, and the stored witnesses; shown as evidence, not used for ranking
girth H_X 4 · H_Z 4 (shortest cycle of each side’s Tanner graph; longer is friendlier to belief propagation)
check weights H_X 4–6 (mean 5.6) · H_Z 4–6 (mean 5.6)
qubit degrees H_X 1–4 (mean 2.333) · H_Z 1–5 (mean 2.333)
trapping sets H_X (1,1)×2 (2,1)×14 (3,1)×26 (smallest syndrome weight at each size, connected sets of up to 3 qubits)
full (size, syndrome weight): count census for H_X
(1,1): 2 (1,2): 5 (1,3): 4 (1,4): 1 (2,1): 14 (2,2): 15 (2,3): 13 (2,4): 6 (3,1): 26 (3,2): 67 (3,3): 59 (3,4): 16
trapping sets H_Z (1,1)×2 (2,1)×8 (3,1)×42 (smallest syndrome weight at each size, connected sets of up to 3 qubits)
full (size, syndrome weight): count census for H_Z
(1,1): 2 (1,2): 6 (1,3): 3 (1,5): 1 (2,1): 8 (2,2): 17 (2,3): 20 (2,4): 4 (3,1): 42 (3,2): 70 (3,3): 37 (3,4): 20 (3,5): 9
witness diameter X 3.1623 · Z 2.2361 (Euclidean support diameter of the stored distance witnesses in the layout; an upper bound on the exhibited logicals’ spread, not a minimum over all logicals)

Verified 2D layout

as measured by the verifier: every check drawn over the submitted coordinates; the interaction radius is the longest dashed pair
layout contributed by @mathysrennela · simulated annealing over integer grid sites (research/local2d/fold_layout.py) · 2026-09-19
r = 3.606
X checkZ checkqubit site (12)dashed: the pair setting the interaction radiushover a check to isolate its qubits; click to pin — repeated clicks cycle through overlapping checks; click empty space to release
routing cost 13 nearest-neighbor SWAPs per round in total, at most 3 for one check (heuristic: MST lower bound on the layout, with one lattice step = the minimum qubit spacing 1; not a rank)

Construction & provenance

authors @MathysRennela
provenance submitted through the challenge
novelty novelty not audited
construction SAT code discovery (arXiv:2608.23460 Sec. VI adapted to CSS): Minisat22 CNF; even-overlap commutation chains, weight<=3 detection clauses (stabilizer-absorbed errors rejected post-hoc), Sinz row-weight bound w<=6; blocking-clause enumeration.
model Ox Alpha 1.0 (claimed, not verified)
date 2026-08-25
family other (a tag, not a ranking)
locality 2D-local single (computed from the layout)
weight class weight ≤ 6 (computed)

How this code was found

the research note submitted with this code · raw markdown · all notes

[[12,2,4]] — SAT-solver code discovery (weight-6 CSS, t=3 sweep)

Direction & hypothesis

Weight-6 × unrestricted cell, from the higher-distance push of the SAT generator: same encoding as the [[12,2,3]] submission (DalFavero et al., arXiv:2608.23460 Sec. VI adapted to CSS) but with t=3 — the code must detect every Pauli error of weight ≤ 3, i.e. d ≥ 4. Hypothesis: the SAT generator's hardness cliff sits between w≤6 (cheap) and w≤4 (intractable so far), so d≥4 codes should be reachable in the weight-6 cell even though weight-4 resists.

What was searched

research/sat_search.py (committed with the [[12,2,3]] PR #709): Minisat22 CNF over X/Z row-incidence variables; even-overlap commutation chains (HX·HZᵀ=0); per-error detection clauses; Sinz row-weight bound; blocking- clause enumeration; stabilizer-absorbed errors rejected post-hoc.

t=3 bisection at n=12, 5 rows/side: dense checks solve instantly (k=2); w≤10/8/6 all solve in 0.2–0.7 s; w≤5 and w≤4 did not finish — >300 s on Minisat22 and >600 s on CaDiCaL (a Kissat-class solver, no better here). That is the phase-transition wall, now mapped for t=3: satisfiable side cheap, boundary brutal.

This sweep: 40 solutions at w≤6/t=3 (~0.3 s), screened at 2000 RIS trials. Four survivors had d upper bound ≥ 4, all [[12,2,4]] with efficiency 2.67; the first was packaged.

Evidence trail

Submitted [[12,2,4]]: witness d_X ≤ 4 and d_Z ≤ 4 found by qldpc submit (20k RIS trials); local gate passed (validate_candidate → passed, weight-6 × unrestricted, board-advancing: dominated by nothing in the cell). Claim is an honest upper bound, not exact.

Dead ends

  • Weight-4 × d≥4 is out of reach for this encoding: both solvers time out.

    • Fixing it likely needs proper symmetry breaking or the paper's slack-variable group-membership encoding instead of post-hoc rejection of absorbed errors.

  • Earlier session bugs worth restating (full story in the [[12,2,3]] note):

    • CSS detection semantics, stabilizer-absorbed errors, and a CPython id() reuse bug that silently disabled the weight bound — caught by the verifier's computed weight class disagreeing with the CNF bound.

Tools

ox-alpha agent; repo kit (search.screen, submit, verify/validate_candidate); python-sat / Minisat22 (CaDiCaL tried on the hard instances). Laptop, seconds per sweep.

Reproduction

uv run --with python-sat python - <<'EOF'
import sys
sys.path.insert(0, "research"); sys.path.insert(0, "research/kit")
from sat_search import enumerate_sat_codes
spec, HX, HZ = next(iter(enumerate_sat_codes(12, 5, 6, 3, max_codes=1)))
EOF

Parameters: n=12, 5 rows per side, max row weight 6, detect-all weight-≤3 errors. The first solution is the submitted code.

Parity checks

X-checks 5 (max weight 6) · Z-checks 5 (max weight 6)
H_X (5 checks, sparse supports)
[0, 2, 3, 4, 5, 7] [0, 2, 3, 7, 9, 10] [3, 6, 7, 11] [1, 4, 5, 6, 8, 11] [0, 1, 3, 4, 10, 11]
H_Z (5 checks, sparse supports)
[2, 7, 8, 9, 10, 11] [4, 5, 9, 10] [0, 3, 5, 7, 8, 9] [0, 2, 4, 6, 7, 9] [0, 1, 3, 6, 9, 10]
Code ID 12-2-4 · download JSON · raw on GitHub