This is the implemention of the cnf2syn tool used for experiments in the paper:
Tractable Representations for Boolean Functional Synthesis S. Akshay, Supratik Chakraborty and Shetal Shah submitted for review to Annals of Mathematics and Artificial Intelligence
Download the code using git clone
To make:
You will need to install the following packages if they are not already installed in your system
sudo apt install libreadline-dev libboost-all-dev libgmp-dev build-essential
To make cnf2syn, we first need to make the libraries it is dependent on. This can be done by running the install.sh script or alternatively using the following commands:
- cd dependencies/abc; make; make libabc.a; cd ../../
- cd dependencies/dsharp; make; make libdsharp.a; cd ../../
- cd dependencies/bfss; make; make libcombfss.a; cd ../../
- Finally do a make in the base directory. This will generate the binary cnf2syn in the bin directory
To run:
To run cnf2syn use the following command ${PATH-TO-cnf2syn}/cnf2syn {benchmark-name}.qdimacs
If you want the synNNF representation printed to a file please use the option --dumpResult while running the command above. The synNNF representation is printed in {benchmark-name}.syn.blif file.
To verify the {benchmark-name}.syn.blif file use: ${PATH-TO-c2syn}/verify {benchmark-name}.qdimacs {benchmark-name}.syn.blif {benchmark-name}_varstoelim.txt
Please see the script test/run-cnf2syn for more details.
Known issues:
- The generated synNNF file ({benchmark-name}.syn.blif) can be quite large.
For large representations, we are currently unable to verify these files as they are too big for ABC to read them.