The LeanSAT package is meant to provide an interface and foundation for verified SAT reasoning. The primary contribution it contains is a verified LRAT checker, as well as an incremental version of the same checker. Both of these are included in LRAT.LRATChecker.lean
, and both of their soundness theorems are included in LRAT.LRATCheckerSound.lean
.
This is a Lean 4 project.
- If you already have Lean 4 installed, with an up-to-date version of
elan
, this project can be built by runninglake build
. - If you already have Lean 4 installed, but
elan
is not up to date (and in particular, is old enough to not be able to accesslean4:nightly-2023-07-31
), then first runelan self update
. After this command is run once, the project can be built by runninglake build
. - If you do not have Lean 4 installed, first run
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
, then the project can be built by runninglake build
. - If you do not have Lean 4 installed and the above
curl
command fails, follow the instructions underRegular install
here.
The LRAT checker can be used in a couple of different ways:
-
At the end of
LRAT.LRATChecker.lean
, there is a commandlratCheck
that takes in the path to a CNF file and a path to an LRAT file and uses the checker to confirm that the LRAT file certifies the unsatisfiability of the provided CNF formula. For this command, the standardlratChecker
is used so the LRAT file must be fully written prior to calling the command in order for the command to work as intended. -
The
main
function inMain.lean
takes in a list of strings that is expected to contain the path to a CNF file and a path to an LRAT file. Unlike thelratCheck
command,main
uses theincrementalLRATChecker
and adopts a strategy of interweaving parsing and LRAT verification (specifically, each LRAT line is verified before the next LRAT line is parsed). The benefit of this approach is thatmain
can be run on a CNF file and LRAT file in parallel to a SAT solver that is writing to the LRAT file. The downside of this approach is thatmain
will loop indefinitely on incomplete LRAT proofs (to accommodate the possibility that there is more LRAT proof to come that has not yet been written by the SAT solver). Of course, if need be,main
can be modified to add a custom timeout that will trigger an exit if elapsed, though the currentmain
code does not do this. To turnmain
into a standalone executable, it is sufficient to runlake build
. Themain
function will then be expressed as an executable inbuild/bin/defaultExe
. -
In
PHPDemo.Formula.lean
,load_php3_lrat_proof
provides an example of an IO function that takes a default formulaphp3_formula
(defined earlier in the file), writes the dimacs representation of that formula tophp3.cnf
, calls Cadical withsatQuery
to produce and write an LRAT proof tophp3.lrat
, and parses that LRAT proof to produce a list of default clause actions. That list is used to initializecertified_php3_lrat_proof
inPHPDemo.Formula.lean
, and the LRAT checker is used to verify this LRAT proof at the end ofPHPDemo.Theorem.lean
. More generally, thePHPDemo
directory serves as an example of how LeanSAT formulas can be generated, reasoned about, and verified as unsatisfiable all within Lean.
There are a couple of ways in which this project can be improved.
-
Currently, there are no specific optimizations for RAT additions. In particular, the function
ratHintsExhaustive
inLRAT.Formula.Implementation.lean
is used to check that the negative RAT hints provided by a RAT addition are exhaustive. However, the current implementation ofratHintsExhaustive
simply filters the totality of the default formula'sclauses
field and verifies that the ordered list of indices containing clauses is identical to the list of negative RAT hints provided by the RAT addition. This is inefficient because it involves a linear check over all indices inclauses
including those that have been set tonone
due to a clause deletion. One way to improve on this would be to adopt an optimization used by cake_lpr and maintain a list of indices containing non-deleted clauses. Then, it would only be necessary to iterate over this list, rather than over all the indices in theclauses
field. If such a change would be made, the resulting changes to the soundness proof should largely be localized toexistsRatHint_of_ratHintsExhaustive
inLRAT.Formula.RatAddSound.lean
, though it would probably also be necessary to add additional requirements toreadyForRupAdd
andreadyForRatAdd
. -
Currently, the LRAT parser only supports the human readable format. Given the extent to which the parser poses a bottleneck, it is extremely desirable to find a way to either improve or bypass the parser. There are two avenues that might be explored to this end:
- In addition to having a human readable format, LRAT has a compressed binary format that is designed to be significantly shorter than the human readable format. Supporting this compressed binary format would likely make efficiently reading significantly long LRAT proofs more feasible. This improvement could benefit the LRAT checker both when it is used within Lean and when it is used as a standalone executable.
- To bypass LRAT parsing entirely, it may be possible to modify Cadical (or whichever SAT solver one desires to use) to use Lean's Foreign Function Interface to have the SAT solver transform its LRAT proof into a datastructure that Lean can interact with directly. Then, rather than have the SAT solver write to a file and have the LRAT checker subsequently parse that file (slowly), the FFI could be used to send the LRAT proof to Lean directly. This would only be of benefit when the checker is being used within Lean, but I would expect it to yield greater performance benefits than the compressed binary format.