Tree-of-BDDs Library: Tools, Instances and Presentations.

Tree-of-BDDs

The above archive contains the source code of a C++ library for building Tree-of-BDDs (ToB). The current library can compile both fomulas in CNF and CP-format into a ToB.

The ToB library uses TreeD library for obtaining tree decompositions, and BuDDy library for building BDDs. In the case, the input formula is given in CP-format, the ToB library uses the CLab library to compile a BDD representing each constraint in the input formula. The source code of all these three used external libraries are also distributed above. Note: the distributed externals libraries are modifications to their original distributions, hence, the above ToB library works well only with the modified externals libraries distributed above.

The following sections specify the organization of the files in the zip-archive distributed above, and then give hints about some of the examples distributed in the archive.

Organization

The files in the distributed zip-archive belong to four categories: external-libraries, source-files, example-tools, instance-files and miscellaneous.

-External-libraries: As mentioned above, the ToB distribution above contains modifications of three external libraries: TreeD, BuDDy, CLab. The TreeD library is present in the directory "./TreeDecomposer/". The BuDDy library is in the directory "./TreeOfBDDs/buddy20/". The CLab library is in the directory "./CLab11/". Note, the CLab in turns has it own copy of BuDDy distributed with it, and I never managed to remove this redundancy from the above distribution.

-Source-files: The source files of the ToB library are those in the directory "./TreeOfBDDs/src/". This directory contains the C++ source code for the classes implementing the ToB compilation methods heavily using the external libraries.

-Example-files: The example files are those in the directory "./TreeOfBDDs/examples". Each sub-directory of "./TreeOfBDDs/examples" contains an example tool implemented using the source files. The example tools specify how to use the library while creating tools using it.

-Instance-files: Several input instances in CNF and CP-format are distributed along with the library. The instances are scattered in the directory "./TreeOfBDDs/instances/". This directory also contains some tools and scripts for converting ISCAS format files into CNF format.

-Miscellaneous: There are miscellaneous files scattered in different places of the archive, and they are like scripts and data-files, used during some experiments.

Compiling Source Files

To compile the ToB library, the externals libraries needs to be compiled first and then the ToB files. The source files can be compiled by using the make command in five directories in the order:

(1) "./Clab11/buddy20/src/",
(2) "./Clab11/src/",
(3) "./TreeDecomposer/src/",
(4) "./TreeOfBDDs/buddy20/src/", and
(5) "./TreeOfBDDs/src/"

Examples Directory

As mentioned above, all the example tools using the library are located in the "./TreeOfBDDs/examples/" directory.

Before compiling any example tool, the source files should have been compiled as specified above. To compile an example tool, just use the make command in the sub-directory corresponding to the tool. In most cases, executing an example tool without parameters will print the usage hint.

Some of the important example tools are:

-tob: This example tool can be used to compile a CNF instance into a ToB. It prints the statistics like compilation time and space.

-cp2tob: This example tool can be used to compile a CP-format instance into a ToB.

-simulate: This example tool can be used to compile a CNF instance into a ToB and then to perform simulation of random CE and IM queries. It prints the statistics like the mean response time and percentage of queries requiring more than one second and so on.

-cpsimulate: This example tool can be used to compile a CP-format instance into a ToB and then to perform simulation of random CE and IM queries. It also prints the statistics of the simulations.

[1]. Sathiamoorthy Subbarayan, "Integrating CSP Decomposition Techniques and BDDs for Compiling Configuration Problems", CPAIOR 2005, pp 351-365, Prague (PPT Presentation Slides)
[2]. Sathiamoorthy Subbarayan, Henrik Reif Andersen, "Integrating a Variable Ordering Heuristic with BDDs and CSP Decomposition Techniques for Interactive Configurators", Research Note, April-2005
[3]. Sathiamoorthy Subbarayan, Lucas Bordeaux, Youssef Hamadi, "Knowledge Compilation Properties of Tree-of-BDDs", AAAI 2007, Vancouver (Instances used in the experiments of this paper) (PPT Presentation Slides)