This package has been merged into Lean 4 core as Std.Tactic.BVDecide
with the
leanprover/lean4:nightly-2024-08-29
nightly release.
The LeanSAT package is meant to provide an interface and foundation for verified SAT reasoning.
The things of interested for most external users are:
These tactics are driven by two components that might be of interested for further work:
This is a Lean 4 project.
elan
, this project can be
built by running lake build
.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
.curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
,
then the project can be built by running lake build
.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.
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.bv_decide
roughly runs through the following steps:
by_contra
to start a proof by contradiction.bv_normalize
and seval
simp set to all hypothesis. This has two effects:
x = true
where x
is a mixture of Bool
and fixed width BitVec
expressions.BitVec
theory.