Fast Converging Anytime Model Counting
Authors: Yong Lai, Kuldeep S. Meel, Roland H.C. Yap
AAAI 2023 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Our empirical analysis demonstrates that Partial KC achieves significant scalability and accuracy over prior state-of-the-art approximate counters, including satss and STS. Interestingly, the empirical results show that Partial KC reaches convergence for many instances and therefore provides exact model counting performance comparable to state-of-the-art exact counters. 6 Experiments We evaluated Partial KC on a comprehensive set of benchmarks: |
| Researcher Affiliation | Academia | 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 1: Partial KC(φ, t) ... Algorithm 2: MICROKC(φ) ... Algorithm 3: PROJECTEDKC(φ, P) |
| Open Source Code | Yes | We implemented Partial KC in the toolbox KCBox.1 ... 1KCBox is available at: https://github.com/meelgroup/KCBox |
| Open Datasets | Yes | We evaluated Partial KC on a comprehensive set of benchmarks: (i) 1114 benchmarks from a wide range of application areas...; and (ii) 100 public instances adopted in the Model Counting Competition 2022. We remark that the 1114 instances have been employed in the past to evaluate model counting and knowledge compilation techniques (Lagniez and Marquis 2017; Lai, Liu, and Yin 2017; Fremont, Rabe, and Seshia 2017; Soos and Meel 2019; Lai, Meel, and Yap 2021, 2022). |
| Dataset Splits | No | The paper mentions using benchmarks for evaluation but does not specify any training/test/validation dataset splits, such as percentages or specific sample counts for each split. |
| Hardware Specification | Yes | The experiments were run on a cluster (HPC cluster with job queue) where each node has 2x E5-2690v3 CPUs with 24 cores and 96GB of RAM. |
| Software Dependencies | No | The paper mentions various software tools such as 'KCBox', 'D4', 'sharp SAT-td', 'Exact MC', 'satss', 'STS', 'Approx MC', and 'B+E' but does not specify their version numbers. |
| Experiment Setup | Yes | Each instance was run on a single core with a timeout of 5000 seconds and 8GB memory. We used the pre-processing tool B+E (Lagniez, Lonca, and Marquis 2016) for all the instances... Approx MC was run with ε = 4 and δ = 0.2. |