Adiar

         

Based on the work of Lars Arge [Arge96], Adiar¹ 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

• Documentation
• Dependencies
• Usage
  • Makefile Targets
  • Playground
  • Examples
• Contributions
• License
• Citing this project
• References

Documentation

The documentation is available on Github Pages. To compile it locally, you need CMake and Doxygen (see Dependencies and Usage).

Dependencies

The implementation is dependant on the following external libraries

• TPIE:

  Framework for implementation of I/O efficient algorithms. Among other things, it provides an implementation of files, streams, sorting algorithms and priotity queues. Both are much faster than the algorithms in the C++ standard library [Vengroff94, Mølhave12].

• Bandit:

  Unit testing framework that is both easy to read and write.

• CNL:

  Templated and efficient implementation of fixed-precision numbers.

All of these are included within the repository as submodules. If you have not cloned the repository recursively, then run the following command

git submodule update --init --recursive

Other dependencies that we cannot provide as a submodule are shown below. The ticked dependencies are mandatory to have installed.

• CMake (3.21+) and a C++ compiler (C++17)

  Adiar compiles with the GNU (10+), Clang (12+), and MSVC C++ compilers. We do not monitor compatibility with other compilers, so we cannot guarantee they will work out-of-the-box.

• Boost (1.74.0+)

  Furthermore, TPIE has a dependency on the Boost Library.

• Doxygen (1.8.0+)

  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 (2.40+).

To install all of the above, run the respective command below.

Operating System	Shell command
Ubuntu 22+	apt install cmake g++ libboost-all-dev doxygen graphviz
Fedora 36+	dnf install cmake gcc-c++ boost-devel doxygen graphviz
Arch Linux	pacman -S --needed cmake gcc boost-libs doxygen graphviz

Usage

For how to use Adiar in your project, see the Getting Started page in the documentation.

Makefile Targets

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.

The Makefile provides the following targets

target	effect
build	Build the source files
docs	Build the documentation files
clean	Remove all build files
test	Build and run all unit tests
test/...	Build and run a subset of the unit tests
coverage	Build and run all unit tests and create lcov report
clang/format	Format all files in src/ and test/

Playground

To quickly get started running small pieces of code, we provide in src/playground.cpp a tiny program where all of the boiler-plate is taken care of. This can be useful for trying out a feature, creating a minimal example for a bug report, and to guide development of new features.

To build and run src/playground.cpp with <MiB> MiB of memory (default: 1024 MiB), just run the following make command.

make playground M=<MiB>

Examples

The example/ folder contains larger examples for how to use Adiar. The README.md file in said folder contains a more in-depth description of each of the examples. For benchmarking Adiar against other BDD packages, see the BDD Benchmarking repository.

You can use make examples/<name> to compile and run them.

Contributions

Adiar is not yet feature complete. If you notice anything is missing, please open an issue.

Your contribution to the project is also very welcome! We list multiple “issues” where you can help - these tasks range from the smallest of tasks to entire student projects. Please get familiar with our Contribution Guidelines before you start to work on something.

License

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.

Citing this project

If you use Adiar in some of your academic work, then please consider to cite one or more of the papers in docs/papers/cite.md.

References

• [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)

Footnotes

1. adiar ⟨ portugese ⟩ ( verb ) : to defer, to postpone