A preprocessor for CNF-to-BDD compilation featuring: Backbone identification, occurrence reduction, and vivification via the external PMC tool (see the research paper) ONE-HOT and XOR recovery Multiple variable and clause ordering heuristics, including a re-implementation of MINCE (paper) using the hypergraph cutter KaHyPar (paper) Artifact Contents This artifact consists of multiple components split into different archive files: src.zip: the source code of the reusable Dimagic tool, along with scripts to evaluate the various options Dimagic provides docker-image.tar.zst: a Docker image with all the relevant tools installed, also including the input CNFs of the benchmark suite input-cnfs.tar.zst: a benchmark suite containing 49 models from the test suite of the UnWise feature model sampler (paper) 116 models corresponding to the targets of the embedded configurable operating system (eCos, v3.0) (paper), already converted to DIMACS CNF using FeatureIDE (paper) preprocessed.tar.zst: the input CNFs after preprocessing using Dimagic compilation-logs.tar.zst: log files produced by the BDD compilers OxiDD (paper) and Logic2BDD (paper) when compiling the preprocessed (X)CNFs to BDDs results.zip: tables and figures of the experiment results compiler-bin.tar.zst: binaries of oxidd-cli, Logic2BDD, and Logic2BDD’s version of CUDD from the Docker image (for running the benchmarks outside the container) .zip files can be unpacked with unzip , .tar.zst files can be unpacked using tar --zstd -xvf . When unpacking all archives except docker-image.tar.zst, your directory tree should look like this: . ├── bench-gen source code of dimagic-bench-gen, the tool used to preprocess all CNFs (part │ └── ... of src.zip) ├── bin (compiler-bin.tar.zst) │ ├── Logic2BDD │ └── oxidd-cli ├── data │ ├── compilation-logs (compilation-logs.tar.zst) │ │ ├── ecos │ │ │ └── │ │ │ └── │ │ │ └── ------t.log │ │ └── unwise │ │ └── ... │ ├── preprocessed (preprocessed.tar.zst) │ │ ├── ecos │ │ │ └── │ │ │ └── │ │ │ └── ----.dimacs │ │ └── unwise │ │ └── ... │ └── results (results.zip) │ ├── plots │ │ └── ... │ └── ... ├── dimagic source code of dimagic (src.zip) │ └── ... ├── eval evaluation scripts (src.zip) │ └── ... ├── experiments experiment definitions used by run-all.sh/run.py (src.zip) │ └── ... ├── input-cnfs benchmark suite (input-cnfs.tar.zst) │ ├── ecos │ │ └── .dimacs │ └── unwise │ └── .dimacs ├── kahypar source code of our Rust bindings for KaHyPar (src.zip) │ └── ... ├── kahypar.ini KaHyPar preset (src.zip) ├── lib (compiler-bin.tar.zst) │ ├── libcudd-3.0.0.so.0 │ └── libcudd-3.0.0.so.0.0.0 ├── mt-kahypar source code of our Rust bindings for Mt-KaHyPar (src.zip) │ └── ... ├── patches (src.zip) │ ├── logic2bdd patch for Logic2BDD to allow negated literals in ONE-HOT groups │ │ └── 0001-negated-one-hot.patch │ └── sharpsat-td patch for SharpSAT-TD to allow running it from any location │ └── 0001-flow-cutter-from-path.patch ├── pp-all.sh script to preprocess all CNFs for our experiments (src.zip) ├── run-all.sh script to run the BDD compilation experiments (src.zip) ├── run.py runner script used by run-all.sh (src.zip) └── ... (src.zip) Depending on your use case, you will only want to run a selection of the steps listed below. Especially the larger components (docker-image.tar.zst, preprocessed.tar.zst, compilation-logs.tar.zst) are needed for certain steps only. We indicate the respective prerequisites below. (Re-)using Dimagic Requires: dimagic (either in the Docker container or installed from source, see below) Dimagic generally takes a DIMACS (X)CNF as input, preprocesses it, applies ordering heuristics, and outputs it either as (X)CNF, as circuit (for use with oxidd-cli), or in Logic2BDD’s input format. For instance, you can run: RUST_LOG=info dimagic --pmc --recover-one-hots --var-heuristic=remince --var-kahypar-preset=kahypar.ini --clause-heuristic=remince --clause-kahypar-preset=kahypar.ini input-cnfs/unwise/automotive2_4.dimacs automotive2_4.nnf Here, input-cnfs/unwise/automotive2_4.dimacs is the input file and automotive2_4.nnf is the output. Dimagic will run PMC and recover ONE-HOT clauses, then it will determine variable and clause orders using ReMINCE with the KaHyPar preset from the kahypar.ini file (in the current working directory). Our evaluation indicates that this set of command line options yields very good results. Setting the RUST_LOG environment variable to info is optional and will make Dimagic print some statistics. The input DIMACS CNF file used in the command above as well as kahypar.ini are included in the Docker container (paths relative to the home directory /root) as well as in input-cnfs.tar.zst or src.zip, respectively. The command above takes roughly half a minute to execute on a recent laptop. You can use oxidd-cli to compile the circuit in the NNF file into a BDD using the command below (which should take less than a second). oxidd-cli is included in the Docker container. With a recent Rust installation, you can also install oxidd-cli on your host system via cargo install oxidd-cli@0.3.0. oxidd-cli --read-var-order --count-models automotive2_4.nnf Dimagic has a quite a few other command line options. To list them all, run: dimagic --help Reproducing the Experiments For longer running tasks we give rough time estimates based on our benchmarking system, an 16-core AMD Ryzen 9 5950X CPU with 128 GiB RAM running Ubuntu 24.04 (Linux 6.8). Loading & Running the Docker Image Requires: docker-image.tar.zst, an x86_64 system with Docker or Podman installed (for use with Podman, replace docker by podman in the commands below) To load the Docker image, run: docker load -i docker-image.tar.zst Create a folder data in the current working directory if you have not done so. Then, run the Docker container as follows: docker run --rm -it --name=dimagic -v ./data:/root/data:z --memory=7g --memory-swap=7g dimagic:2.0-jss Note that Docker may require super user privileges, so you may need to prepend sudo to all docker commands. The options of docker run command have the following effects: --rm means that the container (i.e., all the changes made on top of the image) will be removed after exiting the container -i and -t are relevant for interactive access --name=... assigns a name to the container. This may be useful if you want to access the container via an extra shell. -v ./data:/root/data:z mounts the path ./data into the Docker container at /root/data. The directory data on your host system will be created if not existent. z is relevant on some systems with mandatory access control (e.g., SELinux). --memory=... limits the RAM available for the container. If you want to run the benchmarks from within the Docker container, you can use this flag to enforce the memory limit of 7 GiB we used in the benchmarks. --memory-swap=... limits the amount of memory including swap space. Setting this to the same value as --memory disables the use of swap space. Installing Dimagic from Source Requires: src.zip, a recent Rust installation (1.84 and higher should work), CMake 3.26 or newer, a C/C++ compiler supporting C++20 Note that we tested this on an x86_64 Linux system only. macOS should work similarly (but there is no support for the original MINCE tool), Windows is unsupported (there is no PMC build available). First, build and install KaHyPar as described on GitHub (currently, that is steps 1-3 in the section “Building KaHyPar” plus the install command for using the C-style interface). Additionally or alternatively, you can also use Mt-KaHyPar as the hypergraph cutter in ReMINCE. However, preliminary experiments indicated that KaHyPar yields better results than Mt-KaHyPar. (Note that when trying to run dimagic on macOS, it might be necessary to set DYLD_LIBRARY_PATH=/usr/local/lib.) With src.zip unpacked in the current working directory, run: cargo install --path dimagic If you want to enable support for Mt-KaHyPar, append --features mt_kahypar to the command line. If you do not want KaHyPar support, you can use --no-default-features. When running Dimagic with the --pmc option, it will look for the pmc executable in your path. Download pmc (Linux, macOS) and either move it to some location in your path (run echo $PATH to list the respective directories) or place it in some directory and add that directory to your path via export PATH="/path/to/your/pmc/dir:$PATH". Note that the latter is not persistent; for every new shell you will need to run export PATH="/path/to/your/pmc/dir:$PATH" again. Also note that the downloaded file will probably be called pmc_linux or pmc_mac. You must rename it to pmc. Make the binary executable by running chmod +x /path/to/pmc. Similarly, Dimagic will look for an executable called MetaPlacerTest0.exeS in your path when using the option --var-heuristic=mince or --clause-heuristic=mince. This executable is included in the tar file of the MINCE tool. To ease the preprocessing with multiple different options as we used them in our evaluation, we implemented another executable called dimagic-bench-gen. You can install it via cargo install --path dimagic-bench-gen Preprocessing All Input CNFs Requires: the Docker container (alternatively dimagic-bench-gen—see Installing Dimagic from Source—, Python 3.12+, and GNU parallel installed as well as src.zip and input-cnfs.tar.zst extracted in the current working directory) The following command preprocesses the input CNFs with various different options as described in the paper: ./pp-all.sh The resulting (X)CNFs are placed in data/preprocessed and should be equivalent to those in preprocessed.tar.zst. The generation takes roughly three hours with 32 processes running in parallel within the Docker container on our benchmarking system. The generated (X)CNF files use the following naming scheme: ----.dimacs  may contain any combination of the three flags p for PMC, o for ONE-HOT recovery, and x for XOR recovery. The ordering heuristics may be either of r for random, f for FORCE, m for MINCE, or rm for ReMINCE, our re-implementation of the MINCE heuristic. In , we also encode the weights for the different clause kinds. E.g., f+1+2+3 denotes the FORCE heuristic with weight 1 for OR clauses, weight 2 for ONE-HOT clauses, and weight 3 for XOR clauses. For ReMINCE, we also encode the imbalance parameter ε, e.g., rm+1+1+1+0.1 stands for clauses weight 1 for all clause kinds and ε = 0.1.  contains the ordering heuristic, only followed by the ε value in case of ReMINCE. dimagic-bench-gen (which is used by pp-all.sh) will create symbolic links if certain preprocessing techniques are ineffective. For instance, you will find that all files with pox (i.e., PMC preprocessing as well as ONE-HOT and XOR recovery) are symbolic links to the respective file without x: All XORs in the CNFs of our benchmark set are ONE-HOTs as well. Also, dimagic-bench-gen will create a link from a file with clause weights 1+2+2 to 1+1+1 if the given CNF does not contain any ONE-HOT or XOR clauses. However, dimagic-bench-gen will not create links if two different ordering heuristics lead to the same ordering. Additionally, dimagic-bench-gen generally avoids to recompute comparatively expensive preprocessing steps. If the output file for some step is already present, it will not overwrite that file. To aggregate parameters of all (X)CNF files into a table, run: eval/cnf_props.py This takes roughly eight minutes. Besides (X)CNF files, the directory data/preprocessed will also contain logs as well as CSV files showing the running times of the various preprocessing steps. To concatenate the CSV files into one large table, run: eval/cat_pp_times.py All the resulting tables (cnf-props.csv, pp.csv, and pp-links-resolved.csv in data/results) are included in the results.zip file. Running the Benchmarks There are two ways to benchmark the compilation of preprocessed (X)CNF files into BDDs, either inside or outside the Docker container. Running the benchmarks from within the container has one major drawback compared to running them natively on a Linux host: Parallel execution without interferences between processes requires some way to limit their resources. The run.py script can achieve this using systemd-run, which in turn uses Linux’ CGroups, but systemd-run cannot simply be installed in the Docker container. Thus, we do not support parallel benchmark execution in the Docker container, meaning that the execution of all benchmarks will take multiple weeks in total. In the native setup on our benchmarking system, the benchmarks take about a week to complete. Still, the Docker container might be a bit more portable. In both cases, you will run the run-all.sh script, which writes the outputs of oxidd-cli or Logic2BDD, respectively, to the data/compilation-logs directory. run-all.sh is just a simple wrapper around the run.py and eval/sat_count.py scripts. run.py runs the experiments defined in the experiments directory (included in both the /root directory of the Docker container and src.zip). The experiment files correspond to the following research questions / experiments in the paper: preprocessing.toml: RQ1a / E1 remince.toml: RQ1b / E2 ordering.toml: RQ1a-c / E3 multithreading.toml: RQ1d / E4 size.toml: RQ1c / E4 ecos.toml: RQ2 run.py copies the final BDDs in DDDMP format to data/compilation-logs. In a subsequent step, eval/sat_count.py computes SAT counts from the DDDMP files and stores them in data/results/bdd-sat-counts.csv. Since all DDDMP files together consume quite some disk space, the script directly deletes DDDMP files once the SAT count has successfully been computed—unless you set the environment variable KEEP_DDDMP=1. If you plan to use KEEP_DDDMP=1, you should have at least 500 GiB free disk space, otherwise it should be at least 90 GiB. Note that separating BDD compilation and SAT counting is mainly motivated by the fact that we are using arbitrary precision integers for the #SAT computation. The current implementation caches the SAT count for every node, and each SAT count may easily have more than a thousand binary digits, i.e., require a lot more space than the BDD node. Separating BDD compilation and SAT counting allows us to specify different memory bounds. In fact, the eval/sat_count.py script attempts to schedule as many #SAT computations in parallel as there is space available. You can interrupt the experiments at any point in time (using CTRL-C). When restarting it later, the script will automatically continue where it stopped (re-running the aborted BDD compilations). The timings and node counts can be extracted from the compilation logs using the script eval/logs2csv.py. It combines the data with the SAT counts from data/results/bdd-sat-counts.csv and the (X)CNF properties from data/results/cnf-props.csv computed in the previous step. eval/logs2csv.py will create two files, data/results/benchmarks.csv and data/results/benchmarks-links-resolved.csv. The rationale for the latter is the following: run.py will not execute the BDD compilation for input files that are symbolic links, instead it will run the compilation of the original file exactly once. data/results/benchmarks.csv only contains data for the actual compilations whereas data/results/benchmarks-links-resolved.csv also contains the entries for symbolic links. As a preparation step to the benchmark execution, you can tell a Linux system to always use transparent hugepages (THPs), by running the following command on your host system: echo always | sudo tee /sys/kernel/mm/transparent_hugepage/enabled For many Linux distributions, the default value is madvise, which means that programs explicitly need to call the madvise function to enable THPs for a memory region. By using always, the number of TLB cache misses can be reduced significantly, leading to lower BDD compilation times. The value persists only until the next reboot of your host system. Inside the Docker Container Requires: The Docker container The data/preprocessed directory and data/results/cnf-props.csv from either preprocessed.tar.zst and results.zip, or the Preprocessing all Input CNFs step Just run: ./run-all.sh eval/logs2csv.py Note that the #SAT computations will likely fail for some larger models if you enforce a memory limit of 7 GiB only (using the flags --memory=7g and --memory-swap=7g for docker run). You can restart the docker container later without a memory limit to re-run the failed #SAT computations. Natively on a Linux System Requires: A sufficiently recent x86_64 Linux system (e.g., Ubuntu 24.04 or newer). Different processor architectures might work as well, but you would need to build the BDD compilers on your own (i.e., you cannot use the pre-built ones from compiler-bin.tar.zst). systemd-run (should typically be installed already, check via command -v systemd-run) Python 3.12 or newer and the Python package psutil (can be installed via sudo apt install python3-psutil on Ubuntu; we used psutil version 5.9.8) src.zip and compiler-bin.tar.zst extracted in the current working directory The data/preprocessed directory and data/results/cnf-props.csv from either preprocessed.tar.zst and results.zip, or the Preprocessing all Input CNFs step Now run: PATH="$(pwd)/bin" LD_LIBRARY_PATH="$(pwd)/lib" ./run-all.sh eval/logs2csv.py CNF SAT Counting Requires: the Docker container To check for preprocessing or BDD compilation errors, we computed the counts of satisfying assignments using the #SAT solver SharpSAT-TD (paper). The following commands will run SharpSAT-TD on all input CNFs in parallel and aggregate the results in the CSV file data/results/sat-counts.csv: parallel --timeout 600 --results sat-counts sharpSAT -tmpdir /tmp -decot 5 -decow 100 -cs 8192 ::: input-cnfs/*/*.dimacs mkdir -p data/results (cd sat-counts/1 && grep -r "^c s exact arb int" .) | sed 's|+z|/|g;s|^./input-cnfs/||;s|\.dimacs/stdout:c s exact arb int |,|' > data/results/sat-counts.csv The timeout of 10 min per process is sufficient for all models except unwise/linux-2.6.33.3.dimacs. However, we were not able to compile a BDD for that model in any configuration either. Overall, executing the commands does not take much longer than 10 min on our benchmarking system since the huge models can be processed in parallel. Evaluation Requires: a system with Python 3.12+ as well as the Python packages pandas (tested with 2.1.4), scipy (1.11.4), and matplotlib (3.6.3) installed, e.g., the Docker container, additionally results.zip extracted as data/results or the respective CSV files in data/results from the steps Preprocessing All Input CNFs, Running the Benchmarks, and CNF SAT Counting To check that the SAT counts computed by the BDD compilers match the SAT counts of the #SAT solver, run: eval/check_sat_counts.py If all SAT counts match (as expected), the last line printed by the script will be “success.” For 80 of our benchmark runs, we observed that the process reached the memory limit during the DDDMP export. The script will warn about such issues. The script eval/size_profile_collection.py selects the models and seeds for the size profiles (of which some are presented in Figure 9 in the paper). The selection is solely based on the compilation times for the left-deep construction scheme in single-threaded execution, since left-deep generally has the least compilation successes. Unless you wish to conduct more advanced experiments, we recommend to not re-generate the selection. However, if you run this script and the resulting selection differs from the previous one, then you need to enter the paths from data/results/size-profile-models.txt in experiments/size.toml and re-run the experiment. All the remaining scripts in the eval directory print some data summaries, and generate tables or plots (in the data/results directory): preprocessing.py is concerned with the compilation times for different preprocessing configurations (RQ1/E1). It prints the data for Table 1 in the paper and generates the tables pp-construction-times.csv and pp-construction-times-median.csv, as well as the plots in the plots/pp subdirectory of data/results, where plots/pp/summary. corresponds to Figure 5. preprocessing_times.py prints summaries about the time required by preprocessing techniques (RQ1/E1). Further, it generates vo-time.csv and vo-time-rel.csv, which detail the time requirements for variable ordering heuristics in the po (PMC & ONE-HOT) preprocessing configuration co-time.csv and co-time-rel.csv, like above but for clause ordering, as well as pp-time-per-conf.csv and pp-time-per-conf-median.csv, that show the overall preprocessing times per configuration. remince.py deals with the compilation times for MINCE and multiple ReMINCE configurations (RQ1/E2). It prints the data for Table 2, and generates the tables remince-construction-time-agg.csv, remince-construction-time-no-agg.csv, remince-bdd-nodes-agg.csv, and remince-bdd-nodes-no-agg.csv, where agg refers to the aggregation over multiple runs with different seeds, as well as Figure 6 in plots/mince-vs-remince.. ordering.py is concerned with the compilation times for different ordering heuristics (FORCE/ReMINCE), BDD engines and construction schemes (RQ1/E3). It prints Table 3, also as TeX code in plots/ordering-oxidd-balanced.tex, and draws the plots in Figure 7 (plots/ordering-*). var_order_quality.py relates the quality of variable orders via different metrics (cutwidth, total span, nodes in final BDD). It generates plots/bound-vs-actual-* and plots/var-heuristic-quality-*. multithreading.py generates plots/mt-left-deep. and plots/mt-balanced., which are presented in Figure 8 (RQ1/E4). size_profile.py draws the plots in plots/size-profiles, of which some are presented in Figure 9, and prints some details used in the discussion of E4 (RQ1). ecos.py generates the plots and prints the table for Figure 10 (RQ2). The plot files are plots/ecos-p-min. and plots/ecos-po-min.. For all the scripts above generating plots, there are two settings exposed via environment variables. You can set them, e.g., as follows: PLOT_FORMAT=pgf PLOT_PAPER=1 eval/ordering.py PLOT_FORMAT influences the format of the plot files and defaults to pdf, but can, e.g., also be pgf (for inclusion from LaTeX), or png. Setting PLOT_PAPER=1 removes the title and legends from a figure and adjusts its size for embedding it in the paper. Changelog Notable changes since the previous revision of this artifact include: Adjustments to the experiment definitions. Using ReMINCE or a balanced construction scheme instead of FORCE or left-deep, enables us to see some effects for larger models, which just could not be constructed using the previous base configuration. dimagic now takes the minimum of the ONE-HOT and XOR clause weight for two-literal ONE-HOT/XOR clauses. Previously, we used a configuration with ONE-HOT weight 2 and XOR weight 4. Since every two-literal XOR is also a ONE-HOT, a two-literal ONE-HOT was given weight 4 while a three-literal ONE-HOT was only given weight 2. The change led to performance improvements. A newer build of oxidd-cli, which includes an important bugfix in one of OxiDD's dependencies Separate #SAT computation and DDDMP export. The rationale is described in Running the Benchmarks. Additions to the evaluation scripts for more plots. License The contents of src.zip (as well as the source repository) are MIT/Apache-2.0 dual-licensed, see LICENSE-MIT and LICENSE-APACHE. Third-party software included in docker-image.tar.zst is provided under its original licenses. The CNFs in input-cnfs.tar.zst and preprocessed.tar.zst come under their original licenses, see https://zenodo.org/records/10303558 and https://github.com/AlexanderKnueppel/is-there-a-mismatch. Data in compilation-logs.tar.zst and results.zip is provided under CC-BY-4.0. All licenses permit the evaluation of this artifact. Acknowledgements This work is partially supported by the German Research Foundation (DFG) under the projects TRR 248 (see https://perspicuous-computing.science, project ID 389792660) and EXC 2050/1 (CeTI, project ID 390696704, as part of Germany’s Excellence Strategy), and by the NWO through Veni grant VI.Veni.222.431.