Improving stochastic local search for SAT with a new probability distribution. (English) Zbl 1306.68150
Strichman, Ofer (ed.) et al., Theory and applications of satisfiability testing – SAT 2010. 13th international conference, SAT 2010, Edinburgh, UK, July 11–14, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-14185-0/pbk). Lecture Notes in Computer Science 6175, 10-15 (2010).
Summary: This paper introduces a new SLS-solver for the satisfiability problem. It is based on the solver gNovelty+. In contrast to gNovelty+, when our solver reaches a local minimum, it computes a probability distribution on the variables from an unsatisfied clause. It then flips a variable picked according to this distribution. Compared with other state-of-the-art SLS-solvers this distribution needs neither noise nor a random walk to escape efficiently from cycles. We compared this algorithm which we called Sparrow to the winners of the SAT 2009 competition on a broad range of 3-SAT instances. Our results show that Sparrow is significantly outperforming all of its competitors on the random 3-SAT problem.
For the entire collection see [Zbl 1196.68013].
For the entire collection see [Zbl 1196.68013].
MSC:
| 68T20 | Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) |
