Preprocessing for Propositional Model Counting
Authors: Jean-Marie Lagniez, Pierre Marquis
AAAI 2014 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We performed intensive experiments, using a huge number of benchmarks coming from a large number of families. Two approaches to model counting have been considered downstream: direct model counting using Cachet and compilation-based model counting, based on the C2D compiler. The experimental results we have obtained show that our preprocessor is both efficient and robust. |
| Researcher Affiliation | Academia | Jean-Marie Lagniez and Pierre Marquis CRIL-CNRS and Universit e d Artois, Lens, France {lagniez, marquis}@cril.fr |
| Pseudocode | Yes | Algorithm 1: vivification Simpl; Algorithm 2: occurrence Simpl; Algorithm 3: backbone Simpl; Algorithm 4: equiv Simpl; Algorithm 5: ANDgate Simpl; Algorithm 6: XORgate Simpl; Algorithm 7: pmc. |
| Open Source Code | Yes | Our preprocessor pmc and some detailed empirical results, including the benchmarks considered in our experiments, are available at www.cril.fr/PMC/pmc.html. |
| Open Datasets | Yes | We made quite intensive experiments on a number of CNF instances Σ from different domains, available in the SAT LIBrary (www.cs.ubc.ca/ hoos/SATLIB/indexubc.html). |
| Dataset Splits | No | The paper evaluates preprocessing techniques on benchmarks but does not specify dataset splits (e.g., train, validation, test percentages or sample counts) as commonly done for training and validating machine learning models. |
| Hardware Specification | Yes | Our experiments have been conducted on a Quad-core Intel XEON X5550 with 32GB of memory. |
| Software Dependencies | No | The paper mentions using "Cachet" and the "C2D compiler" but does not provide specific version numbers for these or any other software components, which is necessary for reproducible software details. |
| Experiment Setup | Yes | In our experiments, we have considered two combinations of the elementary preprocessings described in the previous section: eq corresponds to the parameter assignment of pmc where opt V = opt B = opt O = 1 and opt G = 0... #eq corresponds to the parameter assignment of pmc where opt V = opt B = opt O = 1 and opt G = 1... In our experiments num Tries was set to 10... (i.e., max A in our experiments max A = 10)... only XOR clauses χi of size max X are targeted; in our experiments max X = 5... A time-out of 3600 seconds per instance Σ has been considered for Cachet and the same time-out has been given to C2D for achieving the compilation of Σ and computing the number of models of the resulting d-DNNF formula. |