n
72
Cell: weight-8 x local-2d-bilayer. At n <= 72 and d >= 3 the cell's best k was 22 (codes/64-22-3.json, weight 6, one layer; 24 in the single-layer [[64,24,3]] submitted from this campaign), with the two-layer codes/65-17-3.json and codes/58-16-3.json below it. For a full-rank model k = n - 2G, so the weight-8 ladder at n = 72 was run downward from G=23: G = 23, 22, 21, 20, 19, 18, 17, and 16 (k floors 26 through 40). The column-count bound G >= 2n/(w+1) = 16 makes G=16 the last rung that can hold a t >= 2 code.
research/local_sat.py build_local_cnf with the grid site list repeated twice (each of the 36 sites of the 6x6 integer grid carries two qubits at the same coordinate, n = 72; in code, local_sat._grid_sites is replaced by a version that yields every site twice, the one-line layers extension of the single-layer encoder), G=17 checks per side anchored at a grid site and acting within anchor radius 3.5 of it (check diameter at most 7.0, the bilayer cap; on the 6x6 grid the farthest sites are 7.07 apart, so the radius excludes only checks that would span opposite corners), row weight at most 8, CSS commutation, nonzero syndrome for every Pauli error of weight at most 2. CaDiCaL 1.9.5 via python-sat, conflict cap 20,000,000 per solve, 6 h wall cap per solve, CNF streamed into the solver. First solve SAT after 409.7 s and 805,963 conflicts; ten distinct models in 935 s (2,173,282 conflicts), all k = 38 with d_ub = 3. Model 0 is the code here.
Every weight <= 2 error is detected by the CNF, and an exhaustive enumeration after staging of every X-type and every Z-type error of weight at most 2 (2,628 supports per side, plain GF(2) column sums) found none with zero syndrome, so d >= 3 holds independently of the SAT encoding. research/kit/submit.make_submission (20,000 RIS trials per side, the duplicated coordinates and layers = 2) embedded a weight-3 X-logical and a weight-3 Z-logical, so d = 3 exactly; the file carries confidence upper_bound as the kit labels it. verify/validate_candidate.py: verifier ok (weight class weight-8, locality class local-2d-bilayer, two qubits per site, measured interaction radius 5.83), no lighter logical in 5,380 RIS trials, no exact or WL-equivalent board duplicate, label "advances the weight-8 x local-2d-bilayer board". Check weights: X-rows seventeen of weight 8; Z-rows one of weight 5, one of weight 7, and fifteen of weight 8. kd^2/n = 4.75. It raises k at (n <= 72, d = 3) in the weight-8 bilayer cell from 24 to 38.
The rungs above gave [[72,26,3]], [[72,28,3]], [[72,30,3]], [[72,32,3]], [[72,34,3]], and [[72,36,3]], every one dominated by this code. The rung below, G=16 (k >= 40), is the column-count minimum and exhausted the 20,000,000-conflict cap in 4,826 s with neither a model nor an UNSAT proof, so k = 40 is open rather than excluded. At weight 6 the same grid closes at G=21 with [[72,30,3]], submitted separately.
research/local_sat.py, research/kit/submit.py, research/kit/surrogate.py, verify/validate_candidate.py. CaDiCaL 1.9.5 via python-sat 1.9.dev15 (Cadical195), CPython 3.12, one core, 6.8 min to the first model.
import local_sat
from pysat.solvers import Cadical195
local_sat._grid_sites = lambda side: [(float(x), float(y))
for y in range(side) for x in range(side) for _ in range(2)]
s = Cadical195(bootstrap_with=[])
cnf = local_sat.build_local_cnf(6, 17, 8, 2, 3.5, sink=s, shared_t3=True)
s.conf_budget(20_000_000); assert s.solve_limited()
model = {abs(m) for m in s.get_model() if m > 0}
# HX[g, q] = cnf["xr"][(g, q)] in model; HZ likewise from cnf["zr"];
# coordinates = cnf["sites"] (each grid point twice), layers = 2.
CaDiCaL is deterministic for a fixed clause order; the first model is the code in this file (fingerprint 587e2266c6562a70).