Between SAT and UNSAT: the fundamental difference in CDCL SAT. The way CDCL SAT solvers find a satisfying assignment is very different from the way they prove unsatisfiability. We propose an explanation to the difference by identifying direct connections to the workings of some of the most important elements in CDCL solvers: the effects of restarts and VSIDS, and the roles of learned clauses. We give a wide range of concrete evidence that highlights the varying effects and roles of these elements. As a result, this paper also sheds a new light on the internal workings of CDCL. Based on our reasoning on the difference in solver behaviors, we present several ideas for optimizing SAT solvers for either SAT or UNSAT instances. We then show that we can achieve improvements on both SAT and UNSAT at the same time by judiciously exploiting the difference. We have implemented a hybrid idea mixing two different restart strategies on top of our new solver COMiniSatPS and observed substantial performance improvement.
Keywords for this software
References in zbMATH (referenced in 10 articles )
Showing results 1 to 10 of 10.
- Barak-Pelleg, D.; Berend, D.; Saunders, J. C.: A model of random industrial SAT (2022)
- Bjørner, Nikolaj; Levatich, Maxwell; Lopes, Nuno P.; Rybalchenko, Andrey; Vuppalapati, Chandrasekar: Supercharging plant configurations using Z3 (2021)
- Cai, Shaowei; Zhang, Xindi: Deep cooperation of CDCL and local search for SAT (2021)
- Kochemazov, Stepan; Ignatiev, Alexey; Marques-Silva, Joao: Assessing progress in SAT solvers through the Lens of incremental SAT (2021)
- Manthey, Norbert: The \textscMergeSatsolver (2021)
- Li, Chu-Min; Xiao, Fan; Luo, Mao; Manyà, Felip; Lü, Zhipeng; Li, Yu: Clause vivification by unit propagation in CDCL SAT solvers (2020)
- Karpiński, Michał; Piotrów, Marek: Encoding cardinality constraints using multiway merge selection networks (2019)
- Liang, Jia Hui; Oh, Chanseok; Mathew, Minu; Thomas, Ciza; Li, Chunxiao; Ganesh, Vijay: Machine learning-based restart policy for CDCL SAT solvers (2018)
- Balyo, Tomáš; Biere, Armin; Iser, Markus; Sinz, Carsten: SAT race 2015 (2016)
- Oh, Chanseok: Between SAT and UNSAT: the fundamental difference in CDCL SAT (2015)