## LeanSAT (deprecated)

### Deprecation

This package has been merged into Lean 4 core as `Std.Tactic.BVDecide`

with the
`leanprover/lean4:nightly-2024-08-29`

nightly release.

### Description

The LeanSAT package is meant to provide an interface and foundation for verified SAT reasoning.

The things of interested for most external users are:

- SAT tactics for automatically discharging goals about boolean expressions, using a SAT solver.
- (WIP) bitblasting tactic for automatically discharging goals about bitvector expressions, using a verified bitblaster + a SAT solver.

These tactics are driven by two components that might be of interested for further work:

- A verified LRAT certificate checker, used to import UNSAT proofs generated by high performance SAT solvers, like CaDiCal.
- A verified AIG implementation, used to exploit subterm sharing while turning the goals into SAT problems.

### 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.

Additionally the project requires a SAT solver, capable of emitting LRAT UNSAT proofs. The one that is used by default is CaDiCal. CaDiCal can usually be installed from Linux package repositories or built from source if necessary.

### Usage

The package offers three different SAT tactics for proving goals involving `BitVec`

and `Bool`

:

`bv_decide`

, this takes the goal, hands it over to a SAT solver and verifies the generated LRAT UNSAT proof to prove the goal.`bv_check file.lrat`

, it can prove the same things as`bv_decide`

. However instead of dynamically handing the goal to a SAT solver to obtain an LRAT proof, the LRAT proof is read from`file.lrat`

. This allows users that do not have a SAT solver installed to verify proofs.`bv_decide?`

this offers a code action to turn a`bv_decide`

invocation automatically into a`bv_check`

one.

There are also some options to influence the behavior of `bv_decide`

:

`sat.solver`

: The name of the SAT solver used by LeanSAT, default "cadical". Currently LeanSAT only guarantees compatability with CaDiCal but if CaDiCal has a non default name this option is still useful.`sat.timeout`

: The timeout for waiting for the SAT solver in seconds, default 10.`sat.trimProofs`

: Whether to run the trimming algorithm on LRAT proofs, default true.`sat.binaryProofs`

: Whether to use the binary LRAT proof format, default true.`trace.bv`

and`trace.sat`

for inspecting the inner workings of LeanSAT.`debug.skipKernelTC`

: may be set to true to disable actually checking the LRAT proof. LeanSAT will still run bitblasting + SAT solving so this option essentially trusts the solver.

### Architecture

`bv_decide`

roughly runs through the following steps:

- Apply
`by_contra`

to start a proof by contradiction. - Apply the
`bv_normalize`

and`seval`

simp set to all hypothesis. This has two effects:- It applies a subset of the rewrite rules from Bitwuzla for simplification of the expressions.
- It turns all hypothesis that might be of interest for the remainder of the tactic into the form
`x = true`

where`x`

is a mixture of`Bool`

and fixed width`BitVec`

expressions.

- Use proof by reflection to reduce the proof to showing that an SMTLIB-syntax-like value that represents the conjunction of all relevant assumptions is UNSAT.
- Use a verified bitblasting algorithm to turn that expression into an
And Inverter Graph. This AIG is designed and
verified similarly to AIGNET from Verified AIG Algorithms in ACL2
and uses optimizations from Local Two-Level And-Inverter Graph Minimization without Blowup.
The bitblasting algorithms are collected from various other bitblasters, including Bitwuzla and Z3
and verified using Lean's
`BitVec`

theory. - Turn the AIG into CNF, using the approach from the ACL2 paper to both implement and verify the translation.
- Run CaDiCal on the CNF to obtain an LRAT proof that the CNF is UNSAT. If CaDiCal returns SAT instead the tactic aborts here and presents a counter example.
- Use an LRAT checker with a soundness proof in Lean to show that the LRAT proof is correct.
- Chain all the proofs so far to demonstrate that the original goal holds.