README.md

Sylvan dynamic variable reordering benchmarks

This repository contains the following benchmark usecases:

• DPMC: Solver that solves weighted model counting (WMC)
• Safety Game Solvers:
• cmp_hashmap: Comparison of linear probing vs chaining
• cmp_sylvancudd: Comparison of Sylvan and CUDD
• syntcomp: A simple BDD based safety game solver for the Reactive Synthesis Competition.

Usage

1. The repository contains a Docker file using which you can build a docker image sylvanbenchmarks:

   docker build --pull --rm -f "Dockerfile" -t sylvanbenchmarks:latest "." 

   The dokcer file creates new directory build (overrriden in case it already exists) and compiles all the executables into it together with the necesarry input data.
2. Run your image as a interactive container using:

   docker run -i -t sylvanbenchmarks:latest

3. inside of the image run the following shell script with all the benchmarks (work directory is set to the project working directory): or run a specific benchmark, eg.:

   cd $SCRIPTS && ./build_dmc.sh

    cd $SCRIPTS && ./test_sylvan_dmc.sh "$DMPC_TESTS/weighted/mcc21__wff.3.75.315.cnf"

    cd $SCRIPTS && ./test_cudd_dmc.sh "$DMPC_TESTS/weighted/mcc21__wff.3.75.315.cnf"