Certified frame-first SAT middleware — decide structured regions (2-SAT · GF(2) parity · counting) before CDCL, and independently verify every verdict (model replay · DRAT). A research harness for where SAT hardness lives.
Portable, independently re-derivable logic-equivalence receipts — DRAT checking with zero dependencies
Certified proof frontier for K_2(11,3): 112/150 normalized and 324/350 selected branch closures; the exact value remains open.
A readable, self-checking CDCL SAT solver, preprocessor and encoding library. Every answer comes with a certificate.
Exact construction and certification of a 1,435-vertex Moser-spindle-free 5-chromatic unit-distance graph, improving the audited 1,441-vertex benchmark.
No symmetric 12-face Szilassi polyhedron: a computer-assisted proof with DRAT certificates (36 SAT instances, independent encodings, one-command reproduction).
Certified prime-gate theorem for fifteen lonely runners: J(14,29) is empty via dual exact solvers and checked DRAT; full LRC(14) remains open.
Explicit group-invariant colourings improving three lower bounds in section 7.1(a) of the dynamic survey Small Ramsey Numbers: R(4,4,4;3) >= 84, R(4,6;3) >= 64, R(5,5;4) >= 36
Proves multiplier circuits correct with checkable certificates (pacheck2), plus a SAT solver with DRAT proofs for hard random 3-SAT
Order-99 Rowley template proving R_5(5) >= 44,338, plus DRAT-certified nonexistence at order 98 for phi >= 40.
A CDCL SAT solver whose UNSAT answers come with a machine-checkable proof -- and the checker too
Certified impossible placements in Eternity II under the five official clues, with reproducible SAT/DRAT certificates.
(Erdős–Lovász cover number problem)A computer-assisted determination of g(6) = 17, the smallest pairwise intersecting 6-uniform family with transversal number 6. Four papers, and an explicit 17-card witness. Research draft: not independently reviewed, no priority claimed.
A length-22 permutation that three stacks in series cannot sort, with a machine-checkable DRAT certificate. Superseded by Pantone-Vatter (2026).
Second engine for a Russian 33-letter autogram: CNF + kissat + DRAT proofs checked by drat-trim. Made by errata, an AI agent.
Check DRAT/DRUP proofs of unsatisfiability inside your Python process. Zero dependencies, optional Rust accelerator.
To associate your repository with the drat topic, visit your repo's landing page and select "manage topics."