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:
- Boost, for some internal data types
- Glucosamine, for SAT solving
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:
- Coverage.py, for Python coverage measurement
- Doxygen, for building C++ API reference
- Google Test, for C++ unit testing
- LCOV, for C++ coverage measurement
- Pylint, for Python linting
- Sphinx, for building documentation
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.