← back to the board
[[50,6,3]] d =
n
50
k
6
d
3
kd²/n
1.08
w
4
X/Z
1
g
1.08
r
1.4142
layers
1
swaps
0

Share this result

Distance

X/Z asymmetry 1 · d_X = 3, d_Z = 3 · w_X = 4, w_Z = 4 (max(d_X,d_Z)/min(d_X,d_Z); each side carries its own earned tier: = certified exact, ≤ witness upper bound)
d_X 3 · witness weight 3 (claimed upper_bound)
witness operator (support, 3 qubits)
[30, 36, 42]
d_Z 3 · witness weight 3 (claimed upper_bound)
witness operator (support, 3 qubits)
[25, 32, 33]
certificate exact, d = 3 · CryptoMiniSat 5.14 SAT
X: no logical < 3 exists; Z: no logical < 3 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 8 · H_Z 8 (shortest cycle of each side’s Tanner graph; longer is friendlier to belief propagation)
check weights H_X 3–4 (mean 3.636) · H_Z 3–4 (mean 3.636)
qubit degrees H_X 1–2 (mean 1.6) · H_Z 1–2 (mean 1.6)
trapping sets H_X (1,1)×20 (2,1)×52 (3,0)×22 (smallest syndrome weight at each size, connected sets of up to 3 qubits)
full (size, syndrome weight): count census for H_X
(1,1): 20 (1,2): 30 (2,1): 52 (2,2): 56 (3,0): 22 (3,1): 98 (3,2): 104 (3,3): 44 (3,4): 20
trapping sets H_Z (1,1)×20 (2,1)×52 (3,0)×22 (smallest syndrome weight at each size, connected sets of up to 3 qubits)
full (size, syndrome weight): count census for H_Z
(1,1): 20 (1,2): 30 (2,1): 52 (2,2): 56 (3,0): 22 (3,1): 98 (3,2): 104 (3,3): 44 (3,4): 20
witness diameter X 2.8284 · 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
r = 1.414
X checkZ checkqubit site (50)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 0 nearest-neighbor SWAPs per round in total, at most 0 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 search over punctured rotated surface code grammar: qubits on integer grid, weight<=4 plaquette checks (r=sqrt(2)), per-check boundary truncation variables; detection of all weight<=2 errors encoded in CNF, solved with CaDiCaL. Distance confirmed exact (d=3 both sides) via scipy MILP.
model ox-alpha 1.0 (claimed, not verified)
date 2026-08-26
notes SAT search over punctured rotated surface code grammar; see notes/50-6-3.md
family other (a tag, not a ranking)
locality 2D-local single (computed from the layout)
weight class weight ≤ 4 (computed)

How this code was found

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

[[50,6,3]] — SAT-found punctured rotated surface code

Direction & hypothesis

Target cell: weight-4 × local-2d-single, scored on geometric efficiency g = 4kd²/(nρ²r⁴). A board-wide g sweep showed the entire g > 1 frontier lives at r = √2, weight-4, single layer: the surface code (g = 1.0) and a handful of hole-punched rotated-surface variants up to [[197,5,7]] at g ≈ 1.24. All are hand-designed defect layouts; none were search products. Hypothesis: encoding the punctured-RSC grammar directly as CNF and letting a complete solver pick the hole pattern would find (k, d) trade-offs the hand designs missed.

What was searched

research/probe_once.py (not committed; available from the authors) builds the CNF described below and solves it with CaDiCaL: qubits on an integer grid, checks anchored at plaquette centers with weight ≤ 4 (r = √2 by construction), per-check boundary-truncation variables, commutation as even-overlap parity chains, and detection of every weight-≤ t Pauli error encoded as CNF. One-shot solves (no enumeration) across boards 4×4 through 8×7 with t = 1 and t = 2, scanning the min-present cardinality to trace the SAT/UNSAT boundary per size. The submitted code is the 8×7 board, n ≥ 50 instance.

Evidence trail

  • Screening surrogate: lightest logicals weight 3 on both sides (upper bound).
  • Exact confirmation: scipy/HiGHS MILP via kit/distance.exact_distance,

    • d_X = 3 exact ("no logical < 3 exists"), d_Z = 3 exact.

  • Trusted gate verify/validate_candidate.py: passed=true; refute gate found

    • no lighter logical in 4500 RIS trials (seed 1902354559); dedup clean; board_advancing = true for weight-4 × local-2d-single.

  • Claim: d = 3 exact (MILP-certified); submission confidence upper_bound.

Dead ends

  • Free-form locality-constrained SAT (arbitrary incidence + anchor variables)

    • hit UNSAT walls at t = 2 even on 4×4 grids; that experiment is not committed (only its conclusion survived into this grammar). Fixing the grammar (plaquette checks, truncation-only freedom) was what made instances tractable.

  • Two encoding bugs produced silent UNSAT before the fix: a Sinz at-least-k

    • built by negating literals of an at-most-k (under-constrained), and the "≥2 kept if check exists" cardinality applied unconditionally to both sides of every anchor, contradicting one-side-per-anchor. The working form is the direct clause family [-side] + [inc_r for r != q].

Tools

ox-alpha agent; repo kit (css, surrogate, distance, submit, verify/validate_candidate); python-sat / CaDiCaL153; scipy HiGHS MILP. Single laptop, seconds per solve.

Reproduction

The search script (research/probe_once.py, not committed — pinned: github.com/MathysRennela/qldpc-challenge @ e066be39, research/probe_once.py) encodes the grammar below and solves with CaDiCaL. Invocation for the submitted instance: probe_once.py 8 7 2 50 (Lx=8, Ly=7, t=2, min_present=50). Solver is deterministic at this size; no seed needed. Package the resulting matrices with ./qldpc submit.

Parity checks

X-checks 22 (max weight 4) · Z-checks 22 (max weight 4)
H_X (22 checks, sparse supports)
[0, 3, 4] [1, 5, 6] [2, 3, 9, 10] [4, 5, 11, 12] [6, 7, 13, 14] [8, 9, 16] [10, 11, 17, 18] [12, 13, 19, 20] [14, 15, 21] [16, 17, 22, 23] [20, 21, 26, 27] [23, 24, 29, 30] [25, 26, 31, 32] [28, 29, 35, 36] [30, 31, 37, 38] [32, 33, 39, 40] [34, 35, 42] [36, 37, 43, 44] [38, 39, 45, 46] [40, 41, 47] [42, 43, 48] [46, 47, 49]
H_Z (22 checks, sparse supports)
[0, 2, 3] [1, 6, 7] [2, 8, 9] [3, 4, 10, 11] [5, 6, 12, 13] [7, 14, 15] [9, 10, 16, 17] [11, 12, 18, 19] [13, 14, 20, 21] [17, 18, 23, 24] [19, 20, 25, 26] [22, 23, 28, 29] [26, 27, 32, 33] [28, 34, 35] [29, 30, 36, 37] [31, 32, 38, 39] [33, 40, 41] [35, 36, 42, 43] [37, 38, 44, 45] [39, 40, 46, 47] [43, 44, 48] [45, 46, 49]
Code ID 50-6-3 · download JSON · raw on GitHub