Symmetric Component Caching for Model Counting on Combinatorial Instances
Authors: Timothy van Bremen, Vincent Derkinderen, Shubham Sharma, Subhajit Roy, Kuldeep S. Meel3922-3930
AAAI 2021 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Our extensive experiments on hard combinatorial instances demonstrate that the resulting counter, SYMGANAK, leads to improvements over GANAK both in terms of PAR-2 score and the number of instances solved. We first prove the soundness of our approach, and then integrate it into the stateof-the-art model counter GANAK. |
| Researcher Affiliation | Collaboration | 1KU Leuven 2Nutanix Software India Pvt. Ltd. 3Indian Institute of Technology Kanpur 4National University of Singapore |
| Pseudocode | Yes | Algorithm 1: #DPLL algorithm with component caching. Algorithm 2: Encoding symmetric components |
| Open Source Code | Yes | The code has been released as a branch of the mainline GANAK implementation2. ... 2https://github.com/meelgroup/ganak |
| Open Datasets | Yes | We evaluated SYMGANAK on 212 instances from a wide range of combinatorial benchmark classes: Battleships, nqueens, grid Bayesian networks, k-colouring of grid graphs, quasigroup (Latin square) completion, FPGA switch-boxes, and logic synthesis, among several others. ... counting variants of many combinatorial problems, such as n-queens, quasigroup (Latin square) completion, and graph k-colouring, enjoy straightforward reductions to #SAT (Wang et al. 2020; Lauria et al. 2017; Gomes and Shmoys 2002). |
| Dataset Splits | No | The paper evaluates solvers on a set of benchmarks and does not describe traditional training/validation/test splits of a dataset in the context of model training. |
| Hardware Specification | Yes | We performed our experiments on a high-performance computer cluster, with each node having an Intel Xeon E52690 v3 CPU with 24 cores and 96GB of RAM. |
| Software Dependencies | No | The paper mentions using 'NAUTY (Mc Kay and Piperno 2014)' for graph canonization, but it does not provide a specific version number for NAUTY or other software used, which is required for reproducibility. |
| Experiment Setup | Yes | For GANAK and SYMGANAK, we set the default value of δ = 0.05, a maximum component cache size of 2GB, and a timeout of 5000 seconds. For SYMGANAK, we empirically determined 10 and 250 to be good lower and upper bound values for hybrid thresholding (see Section 4.2). SYMGANAK (similar to GANAK) uses the independent support (IS) (Ivrii et al. 2016) of the formula to accelerate the search; due to cost considerations, IS is used only if fewer than 500 conflicts are detected after 500 000 decisions. All other parameters were set to their default values as in GANAK. |