CFLOBDDs: Context-Free-Language Ordered Binary Decision Diagrams

CFLOBDD Paper: https://arxiv.org/abs/2211.06818

Weighted CFLOBDD Paper: https://arxiv.org/pdf/2305.13610

CFLOBDDs are data structures that provide double-exponential compression of Boolean functions in the best case (and exponential compression over BDDs). They can be used as a plug-compatible replacement for BDDs. In this paper, we have used them to simulate quantum algorithms.

More recently, Weighted CFLOBDDs (WCFLOBDDs) have also been added to the repository.

Installation

1. Git clone this repository (git clone https://github.com/trishullab/cflobdd.git .)
2. Install Boost C++ from https://www.boost.org/users/download/ (any version should work). The version used in the paper is 1.80.0.
3. Change the directory to the CFLOBDD subfolder (cd CFLOBDD/). The other folders contain code for testing the baselines mentioned in the paper.
4. Compile using the command (creates a.out executable): g++ -g -std=c++17 -w -I. -I.<path_to_boost> -I.Solver/uwr/bit_vector/ -I.Solver/uwr/assert/ -I.Solver/uwr/matrix/ -I.Solver/uwr/parsing/ -lm .cpp Solver/uwr/bit_vector/.cpp Solver/uwr/parsing/*.cpp

Code Structure:

• The main CFLOBDD class is present in cflobdd_t.h with definitions of internal groupings and other classes in cflobdd_node.cpp.
  
• The matrix and vector operations are present in files matrix1234_* and vector_*.
  
• As all the classes are templatized, the classes are instantiated with different types (int, double, float_boost -> arbitary precision floating point).
  
• A CFLOBDD object (say 'int') generally follows :-> cflobdd_int.cpp, cflobdd_top_node_int.cpp (deals with terminal values) and then the core operations are in cflobdd_node.cpp.
  
• cflobdd_node.cpp (or matrix1234_node.cpp) is common to all data types are they handle proto-CFLOBDDs (see the paper for more details).
  
• All the tests are done via runTests function in tests_cfl.cpp which is the only function called in main.cpp.
  
• InitModules in tests_cfl.cpp should be run before creating any CFLOBDD object. InitModules initializes the cache. ClearModules should be invoked before exiting the program.
• Weighted CFLOBDDs have weighted_* or wmatrix_* type of prefix to the files. The structure is similar to CFLOBDDs, except for the edge weights.

Cite

You can cite our work using the following:

• CFLOBDD Work:
  

  @article{sistla2024cflobdds,
    title={CFLOBDDs: Context-free-language ordered binary decision diagrams},
    author={Sistla, Meghana Aparna and Chaudhuri, Swarat and Reps, Thomas},
    journal={ACM Transactions on Programming Languages and Systems},
    volume={46},
    number={2},
    pages={1--82},
    year={2024},
    publisher={ACM New York, NY}
  }
  

• WCFLOBDD work:

  @article{sistla2024weighted,
      title={Weighted context-free-language ordered binary decision diagrams},
      author={Sistla, Meghana and Chaudhuri, Swarat and Reps, Thomas},
      journal={Proceedings of the ACM on Programming Languages},
      volume={8},
      number={OOPSLA2},
      pages={1390--1419},
      year={2024},
      publisher={ACM New York, NY, USA}
    }