Reservoir

joehendrix/lean-sat-checker

A work in progress proof checker for LRAT files written in Lean.

GitHub Link Documentation

Pick a version!

TODO: should show a time axes that allows the users to view, filter and click copy the lakefile config.

README

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