Guiding CDCL SAT Search via Random Exploration amid Conflict Depression
Authors: Md Solimul Chowdhury, Martin Müller, Jia You1428-1435
AAAI 2020 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | An extensive empirical evaluation with four state-of-the-art CDCL SAT solvers demonstrates good-to-strong performance gains with the exp SAT approach. |
| Researcher Affiliation | Academia | Md Solimul Chowdhury, Martin M uller, Jia-Huai You Department of Computing Science, University of Alberta Edmonton, Alberta, Canada. {mdsolimu, mmueller, jyou}@ualberta.ca |
| Pseudocode | Yes | Algorithm 1: Exploration Based CDCL Solver : exp SAT; Algorithm 2: Decide the Branching Variable |
| Open Source Code | Yes | Source code of the exp SAT solvers and 52 SATCoin instances are available at: https://figshare.com/articles/exp SAT Solvers Instances/10324172. |
| Open Datasets | Yes | Test Set 1 contains 750 instances from the main track of SAT-2017 (350) and 2018 (400) and is run with a time limit of 5000 seconds per instance. Test Set 2 consists of 52 hard instances from SATCoin (Bit Coin Mining) cryptographic benchmark, which are generated with the instance generator from (Manthey and Heusser 2018). |
| Dataset Splits | No | The paper describes test sets used for evaluation of SAT solvers but does not specify training, validation, or test splits in the context of training a machine learning model, as the research focuses on SAT solver extensions. |
| Hardware Specification | Yes | All experiments presented in this paper were run on a workstation with 64GB RAM and a processor clock speed of 2.4 GHz. |
| Software Dependencies | Yes | We adopted four baseline solvers: g LCM4, Mpl COMSPS5 (winner of SAT-2016), Mpl CM4 (second runner up of SAT-2018) and Mpl CBT4 (winner of SAT-2018). glucose 4.2.1, which implements the Learned Clause Minimization (LCM) (Luo et al. 2017) technique on top of glucose 4.1. |
| Experiment Setup | Yes | To set the values of the exploration parameters, we performed a small scale grid search with e GLCM: we took one instance at random out of each benchmark from SAT-2018, which gave a subset of 23 instances. We run e GLCM on this subset for small parameters ranges, l W and n W in [4,5,6] and pexp in [0.01,0.02,0.03]. From this grid search, we chose our default parameter setting (m W, m S, pexp)=(5, 5, 0.02). We set the value of the exponential decay parameter ω to 0.9 based on intuition. These are the values used in the experiments. The values of the other parameters for adaptive version are given in Table 7: Weights (w1, w2, w3) (40, 10, 3), Range for n W [ln W , un W ] [1, 20], Range for l W [ll W , ul W ] [1, 10], Range for pexp [lpexp, upexp] [0.02, 0.6], Step size for parameters (sn W , sl W , spexp) (1, 1, 0.01), Exponential Decay Factor ω 0.9. |