Certifying Top-Down Decision-DNNF Compilers
Authors: Florent Capelli, Jean-Marie Lagniez, Pierre Marquis6244-6253
AAAI 2021 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Finally, leveraging a modified version of the compiler D4 for generating certifiable 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 certifiable 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. Specific instructions for certification 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), Configuration (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 certifiable Decision DNNF circuits plus 1h for the verification 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. |