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