Hackathon (#1155) SAT-search. Prior SAT campaigns mined t=3 (d≥4) at small grids and walled. Hypothesis: t=2 (d≥3) is a much cheaper encoding that still finds board-advancing codes in the sparse weight-6 × local-2d-single cell, where the frontier at n=36 was [[36,6,4]] (k=6, d=4). A higher-k d=3 point would be a new nondominated frontier record.
local_sat.py `enumerate_local_sat_codes(n_side=6, G=12, w=6, t=2, radius=2.0, shared_t3=True, solver="cadical")`. 120 codes enumerated; the highest-k (k=12) code with d≥3 was picked. G=12 is the minimum that satisfies t=2 detection at n=36 (G=11 is budget-walled; G=13+ drops k).
Witness-backed upper_bound d=3 (weight-3 logicals on both X and Z sides). validate_candidate: passed=true, verify.ok=true, refute.refuted=false, dedup clean, board_advancing=true (label: "advances the weight-6 x local-2d-single board"). Interaction radius 4.00 (hackathon-eligible).
t=3 (d≥4) at n=36 w6 is budget-walled in-session (needs overnight). Weight-8 t=3 at n=36 (radius 2.0) is empty; radius 4.0 is budget-walled. n=49 (7×7) w6/t2 is budget-walled.
local_sat.py (shared_t3, cadical, per-solve budgets), kit {css,surrogate,submit}, verify/validate_candidate.py (untouched). Model: DeepSeek V4 Flash.
from local_sat import enumerate_local_sat_codes
gen = enumerate_local_sat_codes(6, 12, 6, 2, 2.0, seed=7, max_codes=120,
solver="cadical", conf_budget=1_000_000, time_budget=90.0,
stream=True, shared_t3=True)
# pick highest-k code, package with make_submission(coordinates=..., layers=1)