Efficient Minimization of Decision-DNNF Circuits via Semantic Hashing and Provenance Tracking

This directory contains the supplementary material for the experiments. Softwares Two softwares are included: decdnnf-rs: The version in which we included our approach. ddnnf-to-aig: The translator from decision-DNNF to ASCII AIG. Building the Software In order to build a software, uncompress the archive and execute: cargo build --release The binary will be created in the target/release directory. If the cargo command is not available on your system, you may need to install the Rust toolchain (see https://rust-lang.org/tools/install/). Using decdnnf-rs To reduce a formula, use the following command: BINDIR/decdnnfᵣs reduce-formula -iINSTANCES_DIR/dnnf/binary/binaryclauses01.dnnf -c INSTANCESDIR/cnf/binary/binaryclauses01.cnf --do-not-check -oINSTANCES_DIR/decdnnf_rs/binary/binaryclauses01.outdnnf Provided binaryclauses01.dnnf and binaryclauses01.cnf, this command produces the reduced decision-DNNF binaryclauses01.outdnnf. Using ddnnf-to-aig To convert a file to AIG, use the following command: "BINDIR/ddnnf-to-aig" "INSTANCES_DIR/dnnf/binary/binaryclauses01.dnnf" Provided binaryclauses01.dnnf, this command writes the corresponding ASCII AIG file to the standard output. Results Results are summed up in the results.ods file.