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 [1].
Better Decision Heuristics in CDCL through Local Search and Target Phases
Authors: Shaowei Cai, Xindi Zhang, Mathias Fleury, Armin Biere
JAIR 2022 | Venue PDF | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Experiments on benchmarks from the main tracks of the last three SAT Competitions from 2019 to 2021 and an additional benchmark set from spectrum allocation show that the techniques bring significant improvements, particularly and not surprisingly, on satisfiable real-world application instances. The experimental results clearly show that these techniques enable solving a remarkable number of additional instances in the main track benchmarks of the last three SAT Competitions from 2019 to 2021... |
| Researcher Affiliation | Academia | Shaowei Cai EMAIL Xindi Zhang EMAIL State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences Beijing, China School of Computer Science and Technology, University of Chinese Academy of Sciences Beijing, China Mathias Fleury EMAIL Armin Biere EMAIL Albert-Ludwigs-University Freiburg, Freiburg, Germany Johannes-Kepler-University Linz, Linz, Austria |
| Pseudocode | Yes | Algorithm 1: Typical CDCL algorithm: CDCL(F, α); Algorithm 2: Relaxed CDCL Algorithm with Local-search Rephasing; Algorithm 3: Algorithm to identify and adapt an autarky from a model; Algorithm 4: Implementation of the algorithm to identify an autarky from a model |
| Open Source Code | Yes | The source codes2 and detailed experiment results3 are available online. 2. http://lcs.ios.ac.cn/~caisw/Code/JAIR-SATcodes.zip |
| Open Datasets | Yes | Additionally, we evaluate the solvers on an important application benchmark suite consisting of 10 000 instances1 from the spectrum repacking in the context of bandwidth auction which resulted in about 7 billion dollar revenue (Newman et al., 2018). 1. https://www.cs.ubc.ca/labs/beta/www-projects/SATFC/cacm_cnfs.tar.gz |
| Dataset Splits | No | The paper mentions using "main track benchmarks of the SAT Competitions" and "an additional benchmark set from spectrum allocation" consisting of "10 000 instances". However, it does not specify how these datasets were partitioned into training, validation, or test sets for their experiments. |
| Hardware Specification | Yes | We conducted all experiments on a cluster of computers with Intel Xeon Platinum 8153 @2.00 GHz CPUs and 1 024 GB RAM under the operating system Cent OS 7.7.1908. |
| Software Dependencies | Yes | We conducted all experiments on a cluster of computers with Intel Xeon Platinum 8153 @2.00 GHz CPUs and 1 024 GB RAM under the operating system Cent OS 7.7.1908. |
| Experiment Setup | Yes | For each instance, each solver run with a cutofftime of 5 000 s. p is a parameter and is set to 0.4 according to preliminary experiments on a random sample of instances from recent SAT Competitions. q is set to 0.9 for the same reason. we disallow local search for a certain number of k restarts, where k is set to 500 for Glucose, and 400 for Maple. The limit is set to 5 107 and fixed during search. |