Binary Decision Diagrams in Lean 4
This repository contains a Binary Decision Diagrams (BDD) implementation and formalization in Lean 4.
Status
The library is ready for use, but there is one file that is still not
sorry-free, as indicated by the red circle in the following
file-level dependencies graph of the library:
Usage
To use this library in you project, add something like the following
to your lakefile.toml file:
[[require]]
name = "bdd"
git = "https://github.com/eshelyaron/lean4-bdd"
rev = "main"
Then import the library with import Bdd in your Lean file.
The main API lives in the BDD namespace. It defines the BDD type,
along with functions such as const, var, and, or, not,
restrict, bforall, bexists and relabel which let you construct
BDDs.
It also provides lemmas that you can use to reason about the Boolean
functions that the BDDs that construct represent, for example
BDD.and_denotation is a lemma that characterizes the denotation of
(the Boolean function represented by) the BDD that you get from
BDD.and.
To check whether two BDD denote the same function, use
BDD.instDecidableSemacticEquiv. To check if the denotation of a BDD
depends on a given input variable, use BDD.instDecidableDependsOn.
To find solutions, use BDD.choice or BDD.find.
Online documentation is available at: https://eshelyaron.com/man/lean4-bdd/Bdd/BDD.html
Example Application - SAT Solver
The file SatSolver.lean in the repository implements a BDD-based SAT
solver. To build it, run lake build SatSolver. Then execute it:
$ .lake/build/bin/SatSolver <number-of-variables> <input-file>
For example:
$ .lake/build/bin/SatSolver 40 /path/to/input/file/in/DIMACS/format
SAT