/leansat

This package provides an interface and foundation for verified SAT reasoning

Primary LanguageLeanApache License 2.0Apache-2.0

LeanSAT

Description

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.

Installation

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 running lake 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 access lean4:nightly-2023-07-31), then first run elan self update. After this command is run once, the project can be built by running lake 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 running lake build.
  • If you do not have Lean 4 installed and the above curl command fails, follow the instructions under Regular install here.

Usage

The LRAT checker can be used in a couple of different ways:

  • At the end of LRAT.LRATChecker.lean, there is a command lratCheck 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 standard lratChecker 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 in Main.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 the lratCheck command, main uses the incrementalLRATChecker 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 that main 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 that main 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 current main code does not do this. To turn main into a standalone executable, it is sufficient to run lake build. The main function will then be expressed as an executable in build/bin/defaultExe.

  • In PHPDemo.Formula.lean, load_php3_lrat_proof provides an example of an IO function that takes a default formula php3_formula (defined earlier in the file), writes the dimacs representation of that formula to php3.cnf, calls Cadical with satQuery to produce and write an LRAT proof to php3.lrat, and parses that LRAT proof to produce a list of default clause actions. That list is used to initialize certified_php3_lrat_proof in PHPDemo.Formula.lean, and the LRAT checker is used to verify this LRAT proof at the end of PHPDemo.Theorem.lean. More generally, the PHPDemo directory serves as an example of how LeanSAT formulas can be generated, reasoned about, and verified as unsatisfiable all within Lean.

Roadmap

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 in LRAT.Formula.Implementation.lean is used to check that the negative RAT hints provided by a RAT addition are exhaustive. However, the current implementation of ratHintsExhaustive simply filters the totality of the default formula's clauses 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 in clauses including those that have been set to none 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 the clauses field. If such a change would be made, the resulting changes to the soundness proof should largely be localized to existsRatHint_of_ratHintsExhaustive in LRAT.Formula.RatAddSound.lean, though it would probably also be necessary to add additional requirements to readyForRupAdd and readyForRatAdd.

  • 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:

    1. 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.
    2. 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.