Engineering an Exact Pseudo-Boolean Model Counter
Authors: Suwei Yang, Kuldeep S. Meel
AAAI 2024 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Our extensive empirical evaluation shows that PBCount can compute counts for 1513 instances while the current state-of-the-art approach could only handle 1013 instances. |
| Researcher Affiliation | Collaboration | 1Grab Taxi Holdings 2Grab-NUS AI Lab 3National University of Singapore 4University of Toronto |
| Pseudocode | Yes | Algorithm 1: compute Count(φ, ρ); Algorithm 2: Preprocess(G); Algorithm 3: Assum Probe(G, xi); Algorithm 4: compile Constraint Bottom Up(T, k, eq); Algorithm 5: compile Constraint Top Down(T, k, eq); Algorithm 6: compile TDRecur(T, k, eq, idx); Algorithm 7: compile Constraint Dynamic(T, k, eq) |
| Open Source Code | Yes | code is available at https://github.com/grab/pbcount |
| Open Datasets | Yes | The sensor placement benchmark setting (1473 instances after removal of 0 counts) is adapted from prior work on identifying code sets (Latour, Sen, and Meel 2023). For the auction benchmark setting (1000 instances), we adapt the combinatorial auction setting (Blumrosen and Nisan 2007) to a counting variant. For the multi-dimension knapsack benchmark setting (Gens and Levner 1980) (1000 instances) |
| Dataset Splits | No | The paper mentions generating benchmarks and instances but does not provide specific details on training, validation, or test dataset splits in the conventional sense (e.g., percentages, counts, or splitting methodology). |
| Hardware Specification | Yes | We performed our evaluations on machines with AMD EPYC 7713 processors. |
| Software Dependencies | No | The paper mentions tools and frameworks like PBLib, PBEncoder, and ADDMC, but does not specify their version numbers or any other software dependencies with version information. |
| Experiment Setup | Yes | Each benchmark instance is provided with 1 core, 16GB memory, and a timeout of 3600 seconds. This includes using the default ADDMC configurations for ADD variable ordering (MCS) and cluster ordering ρ (BOUQUET TREE). |