Towards Projected and Incremental Pseudo-Boolean Model Counting
Authors: Suwei Yang, Kuldeep S. Meel
AAAI 2025 | Venue PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | In our evaluations, PBCount2 completed at least 1.40 the number of benchmarks of competing methods for projected model counting and at least 1.18 of competing methods in incremental model counting. In this section, we detail the extensive evaluations conducted to investigate the performance of PBCount2 s new features, namely projected PB model counting and incremental PB model counting. |
| Researcher Affiliation | Collaboration | Suwei Yang1,2,4, Kuldeep S. Meel3,5 1Grabtaxi Holdings 2Grab-NUS AI Lab 3Georgia Institute of Technology 4National University of Singapore 5University of Toronto |
| Pseudocode | Yes | Algorithm 1: PBCount2 model counting with LOW-MD heuristic; Algorithm 2: Cache retrieval of PBCount2 |
| Open Source Code | No | The paper does not explicitly provide a link to the source code or state that the code is publicly released. The provided arXiv link is for the paper itself. |
| Open Datasets | No | In our experiments, we derived synthetic benchmarks from prior work (Yang and Meel 2024), which has 3 benchmark sets auction, multi-dimension knapsack, and sensor placement. The paper references prior work for the benchmarks but does not provide concrete access information (e.g., specific link, DOI, or repository) to the exact datasets used in this study. |
| Dataset Splits | No | The paper discusses benchmark configurations as '3-step' and '5-step' for incremental counting, referring to sequential modifications. It does not provide any specific information regarding training, validation, or test dataset splits in terms of percentages, sample counts, or predefined splits for the benchmarks used. |
| Hardware Specification | Yes | In the experiments, we ran each benchmark instance using 1 core of an AMD EPYC 7713 processor, 16GB memory, and a timeout of 3600 seconds. |
| Software Dependencies | Yes | We implemented PBCount2 in C++, using CUDD library (Somenzi 2015) with double precision and the same ADD variable ordering (MCS) as PBCount and ADDMC (Dudek, Phan, and Vardi 2020a; Yang and Meel 2024). Somenzi 2015 is cited for 'CUDD: CU decision diagram package release 3.0.0'. |
| Experiment Setup | Yes | In the experiments, we ran each benchmark instance using 1 core of an AMD EPYC 7713 processor, 16GB memory, and a timeout of 3600 seconds. |