A local search SAT solver using an effective switching strategy and an efficient unit propagation Advances in local-search SAT solvers have traditionally been presented in the context of local search solvers only. The most recent and rather comprehensive comparisons between UnitWalk and several versions of WalkSAT demonstrate that neither solver dominates on all benchmarks. QingTing2 (a `dragonfly’ in Mandarin) is a SAT solver script that relies on a novel switching strategy to invoke one of the two local search solvers: WalkSAT or QingTing1. The local search solver QingTing1 implements the UnitWalk algorithm with a new unit-propagation technique. The experimental methodology we use not only demonstrates the effectiveness of the switching strategy and the efficiency of the new unit-propagation implementation -- it also supports, on the very same instances, statistically significant performance evaluation between local search and other state-of-the-art DPLL-based SAT solvers. The resulting comparisons show a surprising pattern of solver dominance, completely unanticipated when we began this work.
Keywords for this software
References in zbMATH (referenced in 7 articles )
Showing results 1 to 7 of 7.
- Menai, Mohamed El Bachir; Al-Yahya, Tasniem Nasser: A taxonomy of exact methods for partial Max-SAT (2013)
- Gableske, Oliver; Heule, Marijn J.H.: EagleUP: Solving random 3-SAT using SLS with unit propagation (2011) ioport
- Wei, Wanxia; Li, Chu Min; Zhang, Harry: A switching criterion for intensification and diversification in local search for SAT (2008)
- Kautz, Henry; Selman, Bart: The state of SAT (2007)
- Brglez, Franc; Li, Xiao Yu; Stallmann, Matthias F.: On SAT instance classes and a method for reliable performance experiments with SAT solvers (2005)
- Li, Xiao Yu; Stallmann, Matthias F.; Brglez, Franc: A local search SAT solver using an effective switching strategy and an efficient unit propagation (2004)
- Kautz, Henry; Selman, Bart: Ten challenges \itredux: recent progress in propositional reasoning and search (2003)