Expressing Symmetry Breaking in DRAT Proofs

This page will provide access to proofs and tools presented in our CADE-25 paper.

Ramsey number four

CNF formula
DRAT proof (bubble sort)
DRAT proof (Batcher's Merge-Exchange)

Erdos Discrepancy Conjecture

CNF formula
DRAT proof
DRAT proof (trimmed)

Two-Pigeons-Per-Hole

6: CNF formula DRAT proof optimized DRAT proof
7: CNF formula DRAT proof optimized DRAT proof
8: CNF formula DRAT proof optimized DRAT proof
9: CNF formula DRAT proof optimized DRAT proof
10: CNF formula DRAT proof optimized DRAT proof
11: CNF formula DRAT proof (zipped) optimized DRAT proof
12: CNF formula DRAT proof (zipped) optimized DRAT proof

Proof checking tools

DRAT-trim, visit the homepage for download and usage.
The zip file containing the files used to verify DRAT proofs in ACL2.