Based on the work of Lars Arge [Arge96], Adiar1 is a BDD package [Bryant86] that makes use of time-forward processing to improve the I/O complexity of BDD manipulation. This makes it able to achieve efficient manipulation of BDDs, even when they outgrow the memory limit of the given machine.
Figure: Running time solving N -Queens (lower is better).
This project has been developed at the Logic and Semantics group at Aarhus University.
Table of Contents
The documentation is available on Github Pages.
The implementation is dependant on the the following external libraries
-
TPIE:
Framework for implementation of I/O efficient algorithms. It directly provides sorting algorithms and a priotity queue. Both are much faster than the algorithms in the C++ standard library [Vengroff94, Mølhave12].
-
Unit testing framework that is easy-to-read and write.
-
CNL:
Templated and efficient implementation of fixed-precision numbers.
These are directly imported as submodules. If you have not cloned the repository recursively, then run the following command
git submodule update --init --recursiveOther dependencies that we cannot provide as a submodule are shown below. The ticked dependencies are mandatory to install.
-
CMake and a C++ compiler
One also needs a C++ compiler that supports the 17 standard and CMake. All development has currently been with the gcc compiler, so we cannot guarantee other compilers will work out-of-the-box.
-
Boost
Furthermore, TPIE has a dependency on the Boost Library.
-
Doxygen
The documentation is created with the Doxygen documentation generator.
-
DOT
As a visual aid, the internal representation of the Decision Diagrams can be output as DOT files. These can then be turned into a graphical representation by use of a number of tools, such as graphviz.
To install all of the above then run the respective below.
| Operating System | Shell command |
|---|---|
| Ubuntu 18+ | apt install cmake g++ libboost-all-dev doxygen graphviz |
| Fedora 35+ | dnf install cmake gcc-c++ boost-devel doxygen graphviz |
The project is build with CMake, though for convenience I have simplified the CMake interactions to a single Makefile which works on a local machine. This has only been tested on Ubuntu 18.04 LTS and 20.04 LTS.
The Makefile provides the following targets
| target | effect |
|---|---|
build |
Build the source files |
docs |
Build the documentation files |
clean |
Remove all build files |
test |
Run all unit tests (with O2 optimisations) |
coverage |
Run all unit tests (with no optimisations) and create lcov report |
main M=<MiB> |
Run the main function in src/main.cpp with <MiB> MiB of memory |
The example/ folder contains examples for using the data structures in Adiar. The README.md file in said folder contains a more in-depth description of each of the examples. Even more examples and benchmarks are provided in a separate BDD Benchmarking repository.
Each example takes a set of arguments as input, which can be parsed to the
program as a makefile variable. That is, to change the value of N to to value
follow the make <target> with N=<value>.
example/queens
| variable | description |
|---|---|
| N | Board size (default: 8) |
| M | Memory in MiB (default: 1024) |
example/knights-tour/[T]
The value T can either be all or closed.
| variable | description |
|---|---|
| N | Board size (default: 8) |
| M | Memory in MiB (default: 1024) |
Adiar is not yet feature complete. If you feel anything is missing, please open an issue.
Your contribution to the project is also very welcome! Our issues list of larger student projects but also many smaller things for you to help us with. Please read our Contribution Guidelines before you start working on something.
The software and documentation files in this repository are provided under the MIT License.
Using Adiar will indirectly use TPIE underneath, which in turn is licensed under the LGPL v3 license. Hence, a binary of yours that is statically linked to Adiar will be affected by that license. That is, if you share that binary with others, then you will be obliged to make the source public. This can be resolved by using Adiar as a shared library or have it use an alternative to TPIE, such as STXXL.
If you use Adiar in some of your academic work, then please consider to cite one or more of the papers in docs/cite.md.
-
[Arge96] Lars Arge. “The I/O-complexity of Ordered Binary-Decision Diagram Manipulation”. In: Efficient External-Memory Data Structures and Applications. (1996)
-
[Bryant86] Randal E. Bryant. “Graph-Based Algorithms for Boolean Function Manipulation”. In: IEEE Transactions on Computers. (1986)
-
[Mølhave12] Thomas Mølhave. “Using TPIE for Processing Massive Data Sets in C++”. (2012)
-
[Vengroff94] D.E. Vengroff. “A transparent parallel I/O environment”. In: In Proc. 1994 DAGS Symposium on Parallel Computation. pp. 117–134 (1994)
- adiar ⟨ portugese ⟩ ( verb ) : to defer, to postpone