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 Shift Toward Open and Reproducible AI Research," Under Review, 2026. doi: 10.48550/arXiv.2606.16974..
Certifying Top-Down Decision-DNNF Compilers
Authors: Florent Capelli, Jean-Marie Lagniez, Pierre Marquis6244-6253
AAAI 2021 | Venue PDF | LLM Run Details | Input Tokens: 20,240 Total number of tokens sent to the LLM as input for this paper's analysis. | Output Tokens: 4,341 Total number of tokens produced by the LLM (including reasoning/thinking tokens) for this paper's analysis.
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Finally, leveraging a modiļ¬ed version of the compiler D4 for generating certiļ¬able Decision-DNNF circuits and an implementation of the checker, we present the results of an empirical evaluation that has been conducted for assessing how large are the certiļ¬able Decision-DNNF circuits that can be generated in practice, and how much time is needed to compute and to check such circuits. |
| Researcher Affiliation | Academia | Florent Capelli,1 Jean-Marie Lagniez,2 Pierre Marquis2, 3 1 Universit e de Lille & CNRS & Inria & UMR 9189 CRISt AL 2 CRIL, Universit e d Artois & CNRS 3 Institut Universitaire de France |
| Pseudocode | Yes | Algorithm 1: Pseudocode for Decision-DNNF topdown compilers. Speciļ¬c instructions for certiļ¬cation in compilers based on a CDCL SAT-solver are framed. |
| Open Source Code | Yes | The proofs of the propositions reported in the paper and a folder containing the code of CD4, the code of the checker, the benchmarks used in our experiments, and a spreadsheet containing detailed empirical results are available on www.cril.fr/kc/. |
| Open Datasets | Yes | In our experiments, we have considered 703 CNF instances from the SATLIB1 and other repositories (for instance, the benchmarks from the BN family (Bayesian networks) come from http://reasoning.cs.ucla.edu/ace/). They are gathered into 8 data sets, as follows: BN (192), BMC (Bounded Model Checking) (18), Circuit (41), Conļ¬guration (35), Handmade (58), Planning (248), Random (104), Qif (7) (Quantitative Information Flow analysis security). 1www.cs.ubc.ca/ hoos/SATLIB/index-ubc.html |
| Dataset Splits | No | The paper does not provide explicit training, validation, or test dataset splits in terms of percentages or sample counts for model training. The experiments involve compiling and checking individual CNF instances rather than splitting a large dataset for training and evaluation. |
| Hardware Specification | Yes | All the experiments have been conducted on a cluster equipped with quadcore bi-processors Intel XEON E5-5637 v4 (3.5 GHz) and 128 Gi B of memory. The kernel used was Cent OS 7, Linux version 3.10.0-514.16.1.el7.x86 64. |
| Software Dependencies | Yes | The compiler used was gcc version 5.3.1. The DRAT-trim proof checker is available at https://github. com/marijnheule/drat-trim. |
| Experiment Setup | Yes | A time-out of 1h for the generation of certiļ¬able Decision DNNF circuits plus 1h for the veriļ¬cation step has been considered per instance. A memory-out of 7.6 Gi B has been considered per instance. Hyperthreading was disabled, and no cache share between cores was allowed. |