CCAnr
CCAnr: a configuration checking based local search solver for non-random satisfiability. This paper presents a stochastic local search (SLS) solver for SAT named CCAnr, which is based on the configuration checking strategy and has good performance on non-random SATinstances. CCAnr switches between twomodes: it flips a variable according to the CCA (configuration checking with aspiration) heuristic if any; otherwise, it flips a variable in a random unsatisfied clause (which we refer to as the focused local search mode). The main novelty of CCAnr lies on the greedy heuristic in the focused local search mode, which contributes significantly to its good performance on structured instances. Previous two-mode SLS algorithms usually utilize diversifying heuristics such as age or randomized strategies to pick a variable from the unsatisfied clause. Our experiments on combinatorial and application benchmarks from SAT Competition 2014 show that CCAnr has better performance than other state-of-the-art SLS solvers on structured instances, and its performance can be further improved by using a preprocessor CP3. Our results suggest that a greedy heuristic in the focused local search mode might be helpful to improve SLS solvers for solving structured SAT instances.
Keywords for this software
References in zbMATH (referenced in 4 articles , 1 standard article )
Showing results 1 to 4 of 4.
Sorted by year (- Yamashita, Hiroshi; Aihara, Kazuyuki; Suzuki, Hideyuki: Accelerating numerical simulation of continuous-time Boolean satisfiability solver using discrete gradient (2021)
- Wenjie Zhang, Zeyu Sun, Qihao Zhu, Ge Li, Shaowei Cai, Yingfei Xiong, Lu Zhang: NLocalSAT: Boosting Local Search with Solution Prediction (2020) arXiv
- Cai, Shaowei; Luo, Chuan; Lin, Jinkun; Su, Kaile: New local search methods for partial MaxSAT (2016)
- Cai, Shaowei; Luo, Chuan; Su, Kaile: CCAnr: a configuration checking based local search solver for non-random satisfiability (2015)