static-vtree-heuristics: Vtree Heuristics for Sentential Decision Diagrams

This repository contains the implementations of the static vtree heuristics discussed in my thesis, Growing Vtrees from Variable Orders: Novel Static Heuristics for SDD Compilation.

Folder structure

• /analysis contains everything related to the analysis of the results, including notebooks for plotting matplotlib graphs and data analysis scripts.
• /benchmarks contains everything related to benchmark circuits, including original files, generation scripts, and parsing scripts.
• /heuristics contains the implementation of the two static vtree heuristics discussed in the thesis: the Fan-in heuristic and the Interaction Graph heuristic.
• /output contains the results of all experiments.

The remaining files play a supporting role:

• circuit.py and vtree.py provide the custom implementations of circuits and vtrees used by the heuristics.
• sdd.py contains the compilation script that turns a circuit and a vtree into an SDD.
• experiment.py is the main entry point of the Docker container. It parses the arguments and starts the correct experiment.
• run_experiments.py starts the experiments for a given heuristic. Use run_experiments.sh to run experiments with caffeinate.

Setup and usage

Experiments are executed in Docker containers. Build the image once with:

docker build -t heuristic_experiment .

After the image has been built, experiments can be launched with:

./run_experiments.sh