No results found

LeanSAT

This package provides an interface and foundation for verified SAT reasoning

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:

  1. A verified LRAT certificate checker, used to import UNSAT proofs generated by high performance SAT solvers, like CaDiCal.
  2. 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:

  1. bv_decide, this takes the goal, hands it over to a SAT solver and verifies the generated LRAT UNSAT proof to prove the goal.
  2. 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.
  3. 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:

  1. Apply by_contra to start a proof by contradiction.
  2. Apply the bv_normalize and seval simp set to all hypothesis. This has two effects:
    1. It applies a subset of the rewrite rules from Bitwuzla for simplification of the expressions.
    2. 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.
  3. 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.
  4. 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.
  5. Turn the AIG into CNF, using the approach from the ACL2 paper to both implement and verify the translation.
  6. 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.
  7. Use an LRAT checker with a soundness proof in Lean to show that the LRAT proof is correct.
  8. Chain all the proofs so far to demonstrate that the original goal holds.