An Improved Decision-DNNF Compiler
Authors: Jean-Marie Lagniez, Pierre Marquis
IJCAI 2017 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | In order to assess D4 and to compare it with C2D and Dsharp, we performed experiments on many benchmarks, coming from several families. The results obtained clearly show the benefits offered by D4. |
| Researcher Affiliation | Academia | Jean-Marie Lagniez and Pierre Marquis CRIL, U. Artois & CNRS, F-62300 Lens, France, e-mail: {lagniez, marquis}@cril.univ-artois.fr |
| Pseudocode | Yes | The pseudo-code of D4. Algorithm ?? provides the pseudocode of the compiler D4. The compilation of a given CNF formula Σ is achieved by calling D4(Σ, ). |
| Open Source Code | Yes | The runtime code of D4, the benchmarks used, and some additional empirical results are available on line from https: //www.cril.univ-artois.fr/KC/. |
| Open Datasets | Yes | We have considered 703 CNF instances from the SAT LIBrary www.cs.ubc.ca/ hoos/SATLIB/index-ubc. html, gathered into 8 data sets, as follows: BN (Bayesian networks) (192), BMC (Bounded Model Checking) (18), Circuit (41), Configuration (35), Handmade (58), Planning (248), Random (104), Qif (7) (Quantitative Information Flow analysis security). |
| Dataset Splits | No | No specific training/test/validation splits are mentioned. The experiments are conducted on 703 CNF instances from the SAT LIBrary. |
| Hardware Specification | Yes | The experiments have been conducted on Intel Xeon E5-2643 (3.30 GHz) processors with 32 Gi B RAM on Linux Cent OS. |
| Software Dependencies | Yes | We used our own solver solve, which is based on the state-of-the-art SAT solver Mini SAT 2.2 [E en and S orensson, 2003]. |
| Experiment Setup | Yes | A time-out of 1h and a memory-out of 7.6 Gi B has been considered for each instance. |