Introduction

BoolExpr is an open source C++ library for symbolic Boolean algebra. It implements a C foreign function interface (FFI), and has a Python binding.

The underlying data structure is a directed, acyclic graph. Leaf nodes are referred to as atoms, and branch nodes are referred to as operators. With the exception of unknown constants (similar to Boolean “don’t care”), graph nodes have both a negative and positive form. So instead of having a separate “NOT” operator, you have NOR/OR, NAND/AND, XNOR/XOR, etc. This also applies to literals, the name given to a Boolean variable or its complement.

Do not confuse this implementation with Randal Bryant’s seminal work on symbolic Boolean manipulation of ordered decision diagrams [1]. They are very different things.

The majority of this documentation is oriented to the Python API, because the Python REPL is a nice way to demonstrate concepts.

Features

  • Integration with the advanced, high performance Glucosamine SAT solver library
  • Tseytin transformation
  • Formal equivalence checking
  • Expression simplification
  • Optimistic X propagation

Dependencies

This section lists all of BoolExpr’s dependencies.

If you want to compile from source, you will need the CMake build system installed.

The following third party libraries are included with the repository:

There are a few ways to install the Python package, but I recommend using a virtual environment and pip. Running pip install boolexpr will install the following dependencies:

The following tools are required for development and testing:

Influences

The design of BoolExpr has been influenced by many things.

The original inspiration (circa 2012) was Sympy, a much more comprehensive symbolic mathematics library. Sympy is a pure Python library, so it isn’t free to pursue some performance optimizations that are only possible when using C/C++.

Other notable inspirations are the Boolean libraries in Maple and Mathematica. Their online documentation can be useful as a guide, but the author does not have a license for these commercial tools.

Mostly, the implementation of BoolExpr has been derived from PyEDA. Its C boolexpr library had some value, so it was pulled out as an independent library. The author decided to migrate from C to C++ to take advantage of the new C++11 language features, and the impressive landscape of tooling and libraries. Since BoolExpr has a much narrower focus than PyEDA, it is possible to correct some of the klunky design decisions, and focus like a laser on performance.

Goals

BoolExpr exists for its own sake. It could accurately be described as a yak shaving exercise. One day it might be useful for something, but until that time its main goal is educational. Use it to learn about Boolean algebra, C/C++/Python, software engineering, CFFI usage, etc.

Free Software

BoolExpr is free software. You can use, reproduce, and distribute it under the terms of the Apache-2.0 software license.