n
36
Cell: weight-6 x local-2d-single. The t=2 SAT method (one CNF per grid, check count, and weight bound, with detection of every weight <= 2 Pauli error encoded as clauses) had placed codes/36-12-3.json at G=12 checks per side, and the same session recorded G=11 (which forces k >= 36 - 22 = 14) as budget-walled at interactive budgets. The column-count bound says G=11 is the smallest G that is not trivially UNSAT for weight 6 at n=36 (G >= 2n/7), so the instance was worth one moderate-budget solve rather than a label.
research/local_sat.py build_local_cnf(6, 11, 6, 2, 2.0, shared_t3=True): qubits on the 6x6 integer grid, 11 X-checks and 11 Z-checks, each anchored at a grid site and acting only on qubits within Euclidean distance 2.0 of its anchor (interaction radius at most 4.0 by construction), row weight at most 6 by a sequential counter, even overlap between every X- and Z-row, and nonzero syndrome for every Pauli error of weight at most 2. Solver CaDiCaL 1.5.3 through python-sat, conflict cap 20,000,000 per solve. The first solve returned SAT after 138.4 s and 949,826 conflicts; the model passed the post-check (no weight <= 2 stabilizer) and has k = 14 exactly (rank 11 on each side).
Packaged with research/kit/submit.make_submission (coordinates = the grid sites, layers = 1), which searched 20,000 RIS trials per side and embedded witnesses: a weight-3 X-logical and a weight-3 Z-logical, so d <= 3. verify/validate_candidate.py: verifier ok (weight class weight-6, locality class local-2d-single, measured interaction radius 4.0), refutation found no lighter logical in 3,940 RIS trials, no exact or WL-equivalent board duplicate, label "advances the weight-6 x local-2d-single board". Since every weight <= 2 error has nonzero syndrome, d >= 3 as well, so d = 3 is exact for this code; the submission carries confidence upper_bound as the kit labels it. Check weights: ten X-rows of weight 6 and one of weight 5; eleven Z-rows of weight 6.
An exhaustive check after staging, plain GF(2) arithmetic outside the repo, enumerated every X-type and every Z-type error of weight at most 2 (666 supports per side) and found none with zero syndrome, so d >= 3 holds independently of the SAT encoding and its post-check; with the weight-3 witnesses, d = 3 exactly. The JSON keeps confidence upper_bound.
The same instance family at G=10 would force k >= 16 but violates the column-count bound (10 < 2n/7 = 10.3), so it is UNSAT without solving. The t=3 (d >= 4) instances at the same grid and weight, G=12 and G=13, did not return within the same conflict cap and 3 h wall cap in the triage run of issue #2024.
research/local_sat.py (encoder), research/kit/submit.py, research/kit/surrogate.py, verify/validate_candidate.py. CaDiCaL 1.5.3 via python-sat 1.9.dev15, CPython 3.12, one core, about 2 min for the solve and about 3 min for packaging and the gate. Driver: a thin loop around build_local_cnf that records SAT, UNSAT, or conflict-cap exhaustion per solve; equivalent to enumerate_local_sat_codes with the arguments below.
from local_sat import enumerate_local_sat_codes
gen = enumerate_local_sat_codes(6, 11, 6, 2, 2.0, max_codes=1,
solver="cadical", conf_budget=20_000_000, stream=True, shared_t3=True)
spec, HX, HZ, coords, ax, az = next(gen)
# make_submission(HX, HZ, ..., coordinates=coords, layers=1)
CaDiCaL is deterministic for a fixed clause order, so the first model is the code in this file (fingerprint bd07122378713f2d).