GANAK: A Scalable Probabilistic Exact Model Counter
Authors: Shubham Sharma, Subhajit Roy, Mate Soos, Kuldeep S. Meel
IJCAI 2019 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We evaluate the runtime performance of GANAK on 2031 publicly available benchmarks arising from a wide range of applications of model counting such as probabilistic reasoning, plan recognition, DQMR networks, ISCAS89 combinatorial circuits, quantified information flow, logistics, and the like as have been previously employed in studies on model counting [Brglez et al., 1989; Sang et al., 2005b; Chakraborty et al., 2016; Lagniez and Marquis, 2017]. |
| Researcher Affiliation | Academia | Shubham Sharma1 , Subhajit Roy1 , Mate Soos2 and Kuldeep S. Meel2 1Department of Computer Science and Engineering, Indian Institute of Technology Kanpur, India 2School of Computing, National University of Singapore |
| Pseudocode | Yes | Algorithm 1 GANAK(F, δ)" and "Algorithm 2 Counter(F, δ)" are present in Section 4.1. |
| Open Source Code | Yes | The open source tool along with benchmarks is available at https://github.com/meelgroup/ganak |
| Open Datasets | Yes | We evaluate the runtime performance of GANAK on 2031 publicly available benchmarks arising from a wide range of applications of model counting such as probabilistic reasoning, plan recognition, DQMR networks, ISCAS89 combinatorial circuits, quantified information flow, logistics, and the like as have been previously employed in studies on model counting [Brglez et al., 1989; Sang et al., 2005b; Chakraborty et al., 2016; Lagniez and Marquis, 2017]. |
| Dataset Splits | No | The paper evaluates solvers on a set of benchmarks but does not describe any train/validation/test dataset splits. |
| Hardware Specification | Yes | All our experiments were conducted on a high-performance computer cluster, with each node consists of E5-2690 v3 CPU with 24 cores and 96GB of RAM. |
| Software Dependencies | No | The paper mentions "C++" and "CLHash" as implementation details and refers to other tools like "sharp SAT" and "Approx MC3" but does not provide specific version numbers for any software dependencies. |
| Experiment Setup | Yes | For our experiments, we set δ = 0.05 (for GANAK), a maximum component cache size of 2GB (for sharp SAT and GANAK) and a timeout of 5000 seconds (for all the tools). All other parameters are set to their default values. |