======================================================================== SEARCH-LOG — bounded search: can any outer-ring choice beat the leader's partial 5th corona (defect 3 / required 254, score 4.988189)? ======================================================================== Solver repo : /workspace/research/heesch/gsqs (branch heesch-solver) Leader file : /workspace/research/heesch/heesch/submission/best.heesch sha256 87d35cd173835f0f775cc632921423f6d511dea88352eca30124010cb02b3572 Solver dep : python-sat 1.9.dev15 (pip, venv /workspace/venv) — NON-stdlib; required by solver/*.py (RC2 MaxSAT, CaDiCaL 1.5.3 via pysat). The challenge harness itself is stdlib-only as advertised. Host : aarch64 Linux, Python 3.11.2, ~3 GB RAM (matters below). Question (campaign heesch-leader-optimality): with the 15-cell inner shape fixed, does ANY choice of outer rings cover more than 251/254 of the 5th corona? Score semantics: score = 4 + (R-D)/R, R = required cells of corona 5, D = official defect = |uncovered required cells| + |extra pocket cells|. Beating the leader <=> D/R < 3/254, i.e. one of: D <= 2 (any R) | D = 3 needs R >= 255 D = 4 needs R >= 339 | D = 5 needs R >= 424 (254*D/3 rounded up) A decide U/RMIN asks: defect <= U AND |R| >= RMIN. UNSAT refutes that case entirely; four decides cover every beat case at a given fixed depth. Tools used: corona_opt.py — EXACT MaxSAT (RC2): optimal partial ring 5 with rings 0..4 fixed as submitted. (defect >= uncovered always, so a certified min-uncovered of 3 bounds the official defect at >= 3 even when pockets are ignored in the objective.) joint_multi.py — SAT decision via CaDiCaL with lazy sound hole/pocket cuts; --count-pockets makes the bound the OFFICIAL defect (uncovered + pocket cells); --free-from f fixes rings 0..f-1, frees rings f..5 (5 = partial). Every SAT answer is re-checked by the official check_corona + verify_defect. ======================================================================== RUN 1 — exact optimum, ring 5 only (rings 0..4 fixed as submitted) $ cd /workspace/research/heesch/gsqs/solver && /workspace/venv/bin/python corona_opt.py \ /workspace/research/heesch/heesch/submission/best.heesch \ --out /workspace/research/heesch/runs/corona_opt_best.heesch wall 2.99 s ------------------------------------------------------------------------ grid=H cells=15 coronas=4 |P|=1080 |R|=254 enclosed=0 submitted defect: level 5 u_hc=3 u_hh=3 required=254 tiles=46 candidate corona-5 tiles: 2476 round 0: MaxSAT cost=3 uncovered=3 pockets=40 tiles=45 (0.1s) round 1: MaxSAT cost=3 uncovered=3 pockets=40 tiles=46 (0.1s) round 2: MaxSAT cost=3 uncovered=3 pockets=41 tiles=46 (0.1s) round 3: MaxSAT cost=3 uncovered=3 pockets=44 tiles=46 (0.1s) round 4: MaxSAT cost=3 uncovered=3 pockets=39 tiles=46 (0.1s) round 5: MaxSAT cost=3 uncovered=3 pockets=40 tiles=46 (0.1s) round 6: MaxSAT cost=3 uncovered=3 pockets=36 tiles=46 (0.1s) round 7: MaxSAT cost=3 uncovered=3 pockets=37 tiles=46 (0.1s) round 8: MaxSAT cost=3 uncovered=3 pockets=36 tiles=45 (0.1s) round 9: MaxSAT cost=3 uncovered=3 pockets=34 tiles=45 (0.1s) round 10: MaxSAT cost=3 uncovered=3 pockets=34 tiles=46 (0.1s) round 11: MaxSAT cost=3 uncovered=3 pockets=34 tiles=45 (0.1s) round 12: MaxSAT cost=3 uncovered=3 pockets=34 tiles=45 (0.1s) round 13: MaxSAT cost=3 uncovered=3 pockets=34 tiles=46 (0.1s) round 14: MaxSAT cost=3 uncovered=3 pockets=34 tiles=46 (0.1s) round 15: MaxSAT cost=3 uncovered=3 pockets=42 tiles=46 (0.1s) round 16: MaxSAT cost=3 uncovered=3 pockets=34 tiles=46 (0.1s) round 17: MaxSAT cost=3 uncovered=3 pockets=34 tiles=45 (0.1s) round 18: MaxSAT cost=3 uncovered=3 pockets=34 tiles=46 (0.1s) round 19: MaxSAT cost=3 uncovered=3 pockets=34 tiles=46 (0.1s) round 20: MaxSAT cost=3 uncovered=3 pockets=38 tiles=46 (0.1s) round 21: MaxSAT cost=3 uncovered=3 pockets=38 tiles=47 (0.1s) round 22: MaxSAT cost=3 uncovered=3 pockets=40 tiles=47 (0.1s) round 23: MaxSAT cost=3 uncovered=3 pockets=42 tiles=47 (0.1s) round 24: MaxSAT cost=3 uncovered=3 pockets=30 tiles=47 (0.1s) round 25: MaxSAT cost=3 uncovered=3 pockets=32 tiles=47 (0.1s) round 26: MaxSAT cost=3 uncovered=3 pockets=28 tiles=47 (0.1s) round 27: MaxSAT cost=3 uncovered=3 pockets=36 tiles=46 (0.1s) round 28: MaxSAT cost=3 uncovered=3 pockets=30 tiles=46 (0.1s) round 29: MaxSAT cost=3 uncovered=3 pockets=33 tiles=47 (0.1s) round 30: MaxSAT cost=3 uncovered=3 pockets=33 tiles=47 (0.1s) round 31: MaxSAT cost=3 uncovered=3 pockets=33 tiles=47 (0.1s) round 32: MaxSAT cost=3 uncovered=3 pockets=32 tiles=47 (0.1s) round 33: MaxSAT cost=3 uncovered=3 pockets=35 tiles=46 (0.1s) round 34: MaxSAT cost=3 uncovered=3 pockets=30 tiles=46 (0.1s) round 35: MaxSAT cost=3 uncovered=3 pockets=35 tiles=46 (0.1s) round 36: MaxSAT cost=3 uncovered=3 pockets=36 tiles=47 (0.1s) round 37: MaxSAT cost=3 uncovered=3 pockets=33 tiles=47 (0.1s) round 38: MaxSAT cost=3 uncovered=3 pockets=32 tiles=47 (0.1s) round 39: MaxSAT cost=3 uncovered=3 pockets=28 tiles=50 (0.1s) round 40: MaxSAT cost=3 uncovered=3 pockets=28 tiles=50 (0.1s) round 41: MaxSAT cost=3 uncovered=3 pockets=28 tiles=50 (0.1s) round 42: MaxSAT cost=3 uncovered=3 pockets=28 tiles=51 (0.1s) round 43: MaxSAT cost=3 uncovered=3 pockets=28 tiles=50 (0.1s) round 44: MaxSAT cost=3 uncovered=3 pockets=28 tiles=51 (0.1s) round 45: MaxSAT cost=3 uncovered=3 pockets=27 tiles=50 (0.1s) round 46: MaxSAT cost=3 uncovered=3 pockets=27 tiles=50 (0.1s) round 47: MaxSAT cost=3 uncovered=3 pockets=17 tiles=50 (0.1s) round 48: MaxSAT cost=3 uncovered=3 pockets=23 tiles=49 (0.1s) round 49: MaxSAT cost=3 uncovered=3 pockets=24 tiles=50 (0.1s) no pocket-free optimum found within max-rounds READING: RC2 certifies optimum cost = 3 in every round — NO ring-5 assignment with P4 fixed leaves fewer than 3 required cells uncovered. Official defect >= uncovered >= 3, so no ring-5-only change beats 3/254. (The loop's 50 pocketed optima all have defect > 3 — worse, not better.) ======================================================================== RUNS 2-5 — joint_multi --free-from 4 (rings 0..3 FIXED; complete ring 4 AND partial ring 5 free) ======================================================================== [2 control] $ python joint_multi.py submission/best.heesch --free-from 4 --count-pockets --decide 3/254 wall 10.3 s ------------------------------------------------------------------------ candidates per level: {4: 1761, 5: 13191} peak RSS 0.1 GB vars 254546, clauses 1428478, peak RSS 0.4 GB; DECIDE uncovered <= 3, |R| >= 254 SAT after 44 cuts (8s). OFFICIAL: coronas=4, defect_hc=3 (hh=3, pockets=0) of 254 -> score 4.988189 [3 D<=2, any R] $ python joint_multi.py submission/best.heesch --free-from 4 --count-pockets --decide 2/1 wall 4.1 s ------------------------------------------------------------------------ candidates per level: {4: 1761, 5: 13191} peak RSS 0.1 GB vars 242158, clauses 748504, peak RSS 0.2 GB; DECIDE uncovered <= 2, |R| >= 1 UNSAT after 16 sound cuts (3s): with rings 0..3 fixed, no choice of rings 4..5 has OFFICIAL defect (uncovered + pocket cells) <= 2 over |R| >= 1. [4 D<=3, R>=255] $ python joint_multi.py submission/best.heesch --free-from 4 --count-pockets --decide 3/255 wall 9.6 s ------------------------------------------------------------------------ candidates per level: {4: 1761, 5: 13191} peak RSS 0.1 GB vars 254546, clauses 1428478, peak RSS 0.4 GB; DECIDE uncovered <= 3, |R| >= 255 UNSAT after 32 sound cuts (7s): with rings 0..3 fixed, no choice of rings 4..5 has OFFICIAL defect (uncovered + pocket cells) <= 3 over |R| >= 255. [5 R>=339?] $ python joint_multi.py submission/best.heesch --free-from 4 --r-only --decide 0/339 wall ~12 s ------------------------------------------------------------------------ candidates per level: {4: 1761, 5: 13191} peak RSS 0.1 GB vars 251085, clauses 1420407, peak RSS 0.4 GB; DECIDE uncovered <= 0, |R| >= 339 UNSAT after 0 sound cuts (11s): with rings 0..3 fixed, no choice of rings 4..5 has uncovered <= 0 without extra pockets over |R| >= 339. f=4 CASE CLOSED: D<=2 impossible; D=3 needs R>=255 impossible; D>=4 needs R>=339 impossible (max R < 339). => With rings 0..3 fixed, NO choice of rings 4+5 beats 3/254. (Subsumes run 1's ring-5-only result.) ======================================================================== RUNS 6-10 — joint_multi --free-from 3 (rings 0..2 FIXED; rings 3, 4, 5 free — deeper search) ======================================================================== [6 control] $ python joint_multi.py submission/best.heesch --free-from 3 --count-pockets --decide 3/254 wall ~56 s ------------------------------------------------------------------------ candidates per level: {3: 1367, 4: 10418, 5: 24642} peak RSS 0.1 GB vars 610541, clauses 4021794, peak RSS 1.1 GB; DECIDE uncovered <= 3, |R| >= 254 SAT after 56 cuts (39s). OFFICIAL: coronas=4, defect_hc=3 (hh=3, pockets=0) of 254 -> score 4.988189 [7 D<=2, any R] $ python joint_multi.py submission/best.heesch --free-from 3 --count-pockets --decide 2/1 wall ~35 s ------------------------------------------------------------------------ candidates per level: {3: 1367, 4: 10418, 5: 24642} peak RSS 0.1 GB vars 588365, clauses 2120731, peak RSS 0.6 GB; DECIDE uncovered <= 2, |R| >= 1 UNSAT after 11 sound cuts (18s): with rings 0..2 fixed, no choice of rings 3..5 has OFFICIAL defect (uncovered + pocket cells) <= 2 over |R| >= 1. [8 D<=3, R>=255] $ python joint_multi.py submission/best.heesch --free-from 3 --count-pockets --decide 3/255 wall ~57 s ------------------------------------------------------------------------ candidates per level: {3: 1367, 4: 10418, 5: 24642} peak RSS 0.1 GB vars 610541, clauses 4021794, peak RSS 1.1 GB; DECIDE uncovered <= 3, |R| >= 255 UNSAT after 43 sound cuts (39s): with rings 0..2 fixed, no choice of rings 3..5 has OFFICIAL defect (uncovered + pocket cells) <= 3 over |R| >= 255. [9 D<=4, R>=339] $ python joint_multi.py submission/best.heesch --free-from 3 --count-pockets --decide 4/339 wall ~78 s ------------------------------------------------------------------------ candidates per level: {3: 1367, 4: 10418, 5: 24642} peak RSS 0.1 GB vars 611025, clauses 4024211, peak RSS 1.1 GB; DECIDE uncovered <= 4, |R| >= 339 UNSAT after 0 sound cuts (62s): with rings 0..2 fixed, no choice of rings 3..5 has OFFICIAL defect (uncovered + pocket cells) <= 4 over |R| >= 339. [10 R>=360?] $ python joint_multi.py submission/best.heesch --free-from 3 --r-only --decide 0/360 wall ~227 s ------------------------------------------------------------------------ candidates per level: {3: 1367, 4: 10418, 5: 24642} peak RSS 0.1 GB vars 604731, clauses 4008242, peak RSS 1.1 GB; DECIDE uncovered <= 0, |R| >= 360 UNSAT after 83 sound cuts (207s): with rings 0..2 fixed, no choice of rings 3..5 has uncovered <= 0 without extra pockets over |R| >= 360. f=3 CASE CLOSED: D<=2 impossible; D=3 needs R>=255 impossible; D=4 needs R>=339 impossible; D>=5 needs R>=424 but R <= 359. => With rings 0..2 fixed, NO choice of rings 3+4+5 beats 3/254. ======================================================================== RUN 11 — attempted --free-from 2 (rings 0..1 fixed; rings 2..5 free) $ python joint_multi.py submission/best.heesch --free-from 2 --count-pockets --decide 3/254 DIED ~3 min in: encoding reached 1,053,736 vars / 7,553,966 clauses at 2.4 GB peak RSS, then the process was OOM-killed during the solve — this host has ~3 GB RAM (their runs used a 25-128 GB pod). NOT attempted again: the remaining f<=2 space is not covered by this run. ------------------------------------------------------------------------ candidates per level: {2: 872, 3: 7820, 4: 19516, 5: 35164} peak RSS 0.2 GB vars 1053736, clauses 7553966, peak RSS 2.4 GB; DECIDE uncovered <= 3, |R| >= 254 (process killed after the DECIDE line; no SAT/UNSAT emitted) ======================================================================== SUMMARY ======================================================================== space searched exhaustively (per solver's encoding, pockets counted): * ring 5 only, rings 0..4 fixed — EXACT MaxSAT optimum = defect 3 * rings 4+5, rings 0..3 fixed (f=4) — all beat cases UNSAT * rings 3+4+5, rings 0..2 fixed (f=3) — all beat cases UNSAT space NOT covered: freeing rings 0..2 as well (f <= 2) — host RAM. The solver authors report certified UNSATs at f=1..2 on their own hardware (ledger certificates, standing "certified"/"measured"); those were NOT re-verified here. Best configuration found anywhere in the searched space: the leader's own — defect 3 / 254, score 4.988189 (both controls reproduce it exactly). VERDICT: leader HOLDS over every outer-ring re-choice with rings 0..2 fixed. Not beaten anywhere the search reached. Caveats (honest): UNSATs are solver-trust — incremental CaDiCaL with lazy cuts emits no DRAT, and joint_multi's encoding soundness rests on the arguments in gsqs/README.md ("What would break it"). These runs reproduce the authors' published UNSAT answers but are not themselves proof-checked.