The Power of Literal Equivalence in Model Counting
Authors: Yong Lai, Kuldeep S. Meel, Roland H. C. Yap3851-3859
AAAI 2021 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We perform an extensive experimental evaluation over a comprehensive set of benchmarks and conduct performance comparison of Exact MC vis-a-vis the state of the art counters, c2d, Dsharp, mini C2D, D4, ADDMC, and Ganak. Our empirical evaluation demonstrates Exact MC can solve 885 instances while the prior state of the art solved only 843 instances, representing a significant improvement of 42 instances. |
| Researcher Affiliation | Academia | Yong Lai,1, 2 Kuldeep S. Meel,2 Roland H. C. Yap2 1 Key Laboratory of Symbolic Computation and Knowledge Engineering of Ministry of Education, Jilin University, China 2 School of Computing, National University of Singapore |
| Pseudocode | Yes | Algorithm 2: Exact MC(ϕ, X) |
| Open Source Code | Yes | Exact MC and Pre Lite are available at https://github.com/ meelgroup/KCBox |
| Open Datasets | Yes | We implemented a prototype of Exact MC in C++ 3 and evaluated it on a comprehensive set of 1114 benchmarks 4 from a wide range of application areas... 4The benchmarks are from the following sites: https://www.cril.univ-artois.fr/KC/benchmarks.html https://github.com/meelgroup/sampling-benchmarks https://github.com/dfremont/counting-benchmarks https://www.cs.ubc.ca/hoos/SATLIB/benchm.html |
| Dataset Splits | No | The paper evaluates its model counter on a set of benchmarks but does not provide specific train, validation, or test dataset splits. |
| Hardware Specification | Yes | The experiments were run on a cluster5 where each node has 2x E5-2690v3 CPUs with 24 cores and 96GB of RAM. |
| Software Dependencies | No | The paper mentions implementation in "C++" and the use of the "B+E" pre-processing tool, but it does not specify version numbers for these software components or any other libraries. |
| Experiment Setup | Yes | Each instance was run on a single core with a timeout of 3600 seconds and 4GB memory. easy bound is defined by min(128, #Non Unit Vars/2). If the formula ϕ is classified as easy, then SHOULDKERNELIZE returns false. Else, we consider the search path from the last kernelization (if no kernelization, then the root) to the current node. If the number of unit clauses on the path is greater than 48 and also greater than twice the number of decisions on the path, SHOULDKERNELIZE returns true. |