Notice: The reproducibility variables underlying each score are classified using an automated LLM-based pipeline, validated against a manually labeled dataset. LLM-based classification introduces uncertainty and potential bias; scores should be interpreted as estimates. Full accuracy metrics and methodology are described in Coakley et alK. L. Coakley, T. Snelleman, H. Hoos, and O. E. Gundersen, "The embrace of open science: An analysis of a decade of AI research and 56 800 conference papers," Under Review, 2026..
Guiding CDCL SAT Search via Random Exploration amid Conflict Depression
Authors: Md Solimul Chowdhury, Martin Müller, Jia You1428-1435
AAAI 2020 | Venue PDF | 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. EMAIL |
| 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. |