A Compiler for Weak Decomposable Negation Normal Form
Authors: Petr Illner, Petr Kučera
AAAI 2024 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Our experiments demonstrate that w DNNF circuits are suitable for configuration instances. For the experiments, we considered the same data set... All the experiments were conducted on a Linux (Debian 11) machine using an AMD EPYC 7543 2.8GHz processor and 512 Gi B of RAM. |
| Researcher Affiliation | Academia | Petr Illner, Petr Kuˇcera Department of Theoretical Computer Science and Mathematical Logic, Faculty of Mathematics and Physics Charles University, Czech Republic illner3@gmail.com, kucerap@ktiml.mff.cuni.cz |
| Pseudocode | Yes | Algorithm 1: Bella(φ, cut) |
| Open Source Code | Yes | Bella (w DNNF circuits) and footnote 1https://github.com/Illner/Bella Compiler |
| Open Datasets | Yes | For the experiments, we considered the same data set7 which is used in (Lagniez and Marquis 2017). The data set, which contains 701 instances, consists of the following instance types: Bounded model checking (BMC), Bayesian networks (BN), circuit, configuration, handmade, planning, quantitative information flow analysis security (QIF), and random. and footnote 7http://www.cril.univ-artois.fr/kc/benchmarks.html |
| Dataset Splits | No | The paper mentions a dataset of 701 instances but does not provide specific train/validation/test dataset splits, percentages, or explicit sample counts for reproduction. |
| Hardware Specification | Yes | All the experiments were conducted on a Linux (Debian 11) machine using an AMD EPYC 7543 2.8GHz processor and 512 Gi B of RAM. |
| Software Dependencies | Yes | The same SAT solver as D42 (that is, a modified version of the SAT solver MINISAT 2.2 (E en and S orensson 2004) adapted for D4). |
| Experiment Setup | Yes | The time-out (resp. memory-out) was set to two hours (resp. 16 GB). Due to randomness, every instance was compiled five times, and the results presented in this section are averages. |