On the Role of Canonicity in Knowledge Compilation
Authors: Guy Van den Broeck, Adnan Darwiche
AAAI 2015 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | On the practical side, we reveal an empirical finding that seems quite surprising: bottom-up compilation with compressed SDDs is much more feasible practically than with uncompressed ones, even though the latter supports a polytime Apply function while the former does not. ... Table 3 shows the corresponding sizes and compilation times. ... Figure 3 shows the distribution of these ratios for the two methods (note the log scale). ... The number of function calls is 67,809 for compressed SDDs, vs. 1,626,591 for uncompressed ones. The average ratio is 0.027 for compressed, vs. 0.101 for uncompressed. |
| Researcher Affiliation | Academia | Guy Van den Broeck and Adnan Darwiche Computer Science Department University of California, Los Angeles {guyvdb,darwiche}@cs.ucla.edu |
| Pseudocode | Yes | Algorithm 1 Apply(α, β, ) |
| Open Source Code | Yes | We used the SDD package provided by the Automated Reasoning Group at UCLA4 in our experiments. 4Available at http://reasoning.cs.ucla.edu/sdd/ |
| Open Datasets | No | The paper mentions 'LGSynth89 benchmarks' and 'ISCAS89 benchmarks' but does not provide specific access information such as a link, DOI, repository, or formal citation for these datasets. |
| Dataset Splits | No | The paper analyzes compilation of benchmark CNFs but does not specify any training, validation, or test dataset splits. The experiments focus on the compilation process itself rather than training a model with data splits. |
| Hardware Specification | No | The paper states 'due to running out of 4GB of memory' but does not provide any specific hardware details such as GPU/CPU models, processors, or specific computer specifications used for running the experiments. |
| Software Dependencies | No | The paper mentions using 'the SDD package provided by the Automated Reasoning Group at UCLA' but does not specify a version number for this or any other software dependency. |
| Experiment Setup | Yes | In our first experiment, we compiled CNFs from the LGSynth89 benchmarks into the following (all trimmed): Compressed SDDs respecting an arbitrary vtree. Dynamic vtree search is used to minimize the size of the SDD during compilation, starting from a balanced vtree. Compressed SDDs respecting a fixed balanced vtree. Uncompressed SDDs respecting a fixed balanced vtree. |