Notice: The reproducibility variables underlying each score are classified using an automated LLM-based pipeline, validated against a manually labeled dataset. LLM-based classification introduces uncertainty and potential bias; scores should be interpreted as estimates. Full accuracy metrics and methodology are described in Coakley et alK. L. Coakley, T. Snelleman, H. Hoos, and O. E. Gundersen, "The embrace of open science: An analysis of a decade of AI research and 56 800 conference papers," Under Review, 2026..
A Compiler for Weak Decomposable Negation Normal Form
Authors: Petr Illner, Petr Kučera
AAAI 2024 | Venue PDF | 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 EMAIL, EMAIL |
| 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. |