Lean SAT Proof Checker
This is an exploratory effort to build a proof checker for various formats used by the SAT community. Currently, we have focused on the LRAT SAT Proof format.
Building
To build the tool, you should follow the instructions in the
Lean manual for installing
Lean 4 including the lake
build tool.
The main binary can then be built by running:
% lake build
This will put the binary in ./build/bin/sat-checker
.
Checking a DIMACS file
To check if a dimacs file is valid, you can use the dimacs
command:
% ./build/bin/sat-checker dimacs
Checking a lrat proof
To check a proof, use the lrat
command:
% ./build/bin/sat-checker lrat
As an example, this checks one of the handcrafted proofs:
% ./build/bin/sat-checker lrat examples/handcrafted/lrat-fig1.dimacs examples/handcrafted/lrat-fig1.lrat