A Top-Down Compiler for Sentential Decision Diagrams

Authors: Umut Oztok, Adnan Darwiche

IJCAI 2015 | Conference PDF | Archive PDF | Plain Text | LLM Run Details

Reproducibility Variable Result LLM Response
Research Type Experimental We now present an empirical evaluation of the new top-down compiler. In our experiments, we used two sets of benchmarks. First, we used some CNFs from the iscas85, iscas89, and LGSynth89 suites... We compiled those CNFs into SDDs and Decision-SDDs.
Researcher Affiliation Academia Umut Oztok and Adnan Darwiche Computer Science Department University of California, Los Angeles {umut,darwiche}@cs.ucla.edu
Pseudocode Yes Algorithm 1: SAT() Algorithm 2: #SAT(π, S) Algorithm 3: c2s(v, S)
Open Source Code No The paper uses the SDD package [Choi and Darwiche, 2013a] for comparison, which is hosted at http://reasoning.cs.ucla.edu/sdd. However, there is no explicit statement or link provided for the open-source code of the new top-down compiler described in this paper.
Open Datasets Yes First, we used some CNFs from the iscas85, iscas89, and LGSynth89 suites, which correspond to sequential and combinatorial circuits used in the CAD community. We also used some CNFs available at http://www.cril.univ-artois.fr/PMC/pmc.html, which correspond to different applications such as planning and product configuration.
Dataset Splits No The paper does not explicitly provide information on training/validation dataset splits. The research is focused on compiling CNFs into SDDs, not on training a machine learning model with distinct data splits.
Hardware Specification Yes All experiments were performed on a 2.6GHz Intel Xeon E5-2670 CPU under 1 hour of time limit and with access to 50GB RAM.
Software Dependencies No The paper mentions 'the SDD package [Choi and Darwiche, 2013a]' and 'RSat [Pipatsrisawat and Darwiche, 2007]' as tools used or referenced, but it does not provide specific version numbers for these or other software dependencies of their own compiler.
Experiment Setup Yes All experiments were performed on a 2.6GHz Intel Xeon E5-2670 CPU under 1 hour of time limit and with access to 50GB RAM... We first generate a decision vtree for the input CNF... We obtained decision vtrees as in Oztok and Darwiche [2014].