Online Bayesian Moment Matching based SAT Solver Heuristics
Authors: Haonan Duan, Saeed Nejati, George Trimponias, Pascal Poupart, Vijay Ganesh
ICML 2020 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We perform extensive experiments to evaluate the efficacy of our BMM-based heuristic against 4 other initialization methods (random, survey propagation, Jeroslow-Wang, and default) in state-of-the-art solvers, Maple COMSPS and Maple LCMDist Chronot BT over the SAT competition 2018 application benchmark, as well as the best-known solvers in the cryptographic category, namely, Crypto Mini SAT, Glucose, and Maple SAT. |
| Researcher Affiliation | Collaboration | 1University of Waterloo 2Vector Institute 3Huawei Noah s Ark Lab. |
| Pseudocode | No | The paper describes the Bayesian Moment Matching (BMM) algorithm conceptually and through mathematical equations and figures, but it does not include a formally labeled pseudocode block or algorithm box. |
| Open Source Code | Yes | The source code of our implementations is available at https://github.com/saeednj/BMMSAT. |
| Open Datasets | Yes | We used the main track of the SAT competition 2018, which contains 400 instances coming from a variety of real-world application domains, like verification, graph problems, scheduling and combinatorics (Heule et al., 2019). |
| Dataset Splits | No | The paper discusses solving SAT instances and benchmarks them against other methods. It refers to sets of instances (e.g., 50 cryptographic instances, 400 SAT competition instances) but does not provide any explicit training/validation/test splits for these instances, nor does it describe cross-validation or stratified splitting. The instances themselves are the problems being solved, not data for a traditional ML training/validation process. |
| Hardware Specification | Yes | All jobs were run on Intel Xeon E52667 CPUs at 3.20GHz and 8GB of RAM. |
| Software Dependencies | Yes | The solvers we used were Maple SAT (Liang et al., 2016), Glucose-4 (Audemard & Simon, 2018) and Crypto Mini SAT-5 (Soos, 2018). |
| Experiment Setup | Yes | We use 10 epochs for application instances (each clause is seen ten times) and empirically observed that it results in a good initial point while being efficient. |