A lightweight implementation of a DRAT proof checker for validating unsatisfiability proofs of SAT instances.
This project implements the DRAT (Deletion Resolution Asymmetric Tautology) proof checking algorithm, which is commonly used to certify the correctness of SAT solver results. It was developed for learning and experimentation purposes while studying proof logging and certification techniques in SAT and SMT solving.
- CI
- CLI
- Parser for DIMACS CNF inputs
- Parser for DRAT proof files
- Proper error handling (thiserror, anyhow, etc)
- Unit propagation
- DRAT addition checking
- Clause deletion handling
- Unit tests
- Support for DRUP and LRAT checking
- Benchmark set
- Performance comparison with drat-trim
cargo run path/to/formula.cnf path/to/proof.dratIf the proof is valid, the checker confirms that the proof derives a contradiction from the input formula. Otherwise, it reports an error indicating where verification failed.
Feel free to open issues or submit pull requests if you'd like to contribute to this project.
This project is licensed under the MIT License.