[  download | papers ]

Around 2012 local search solvers became much stronger and were even becoming essential to obtain state-of-the-art performance in the crafted track of the SAT competition.

In particular ideas around ProbSAT showed that local search can be competitive on certain hard satisfiable but non-random instances using a simple and beautiful variant of WalkSAT.

As part of reviewing the PhD thesis of Adrian Balint, who introduced ProbSAT, we reimplemented the ProbSAT algorithm in our new local search SAT solver YalSAT, which confirmed its effectiveness. We were quite surprised that a local search solver was able to solve some of the easy structural formulas, we otherwise used for regression testing of for our CDCL solvers, beside of course solving hard uniform random formulas.

We continued to use YalSAT during one local search inprocessing phase in our parallel SAT solver Treengeling, which in turn uses one or two Lingeling threads with local search enabled in a portfolio style manner in parallel to the main cube-and-conquer algorithm. In the SAT competition 2017 it actually turned out that YalSAT won the random track, which however only had very few participants and Dimetheus the winner in the random track in the SAT competition 2016 was missing too.

Download

Newer versions at https://github.com/arminbiere/yalsat.git

[ yalsat-03v.zip ]

Now with clean open source MIT license.

[ yalsat-03u.zip ]

Supports to print the current best solution if a limit is specified (thanks go to Marijn for this suggestion).

[ yalsat-03s.zip ]

Version 03s was submitted to the SAT competition 2017 and includes the parallel portfolio variant PalSAT too.

Papers

Armin Biere. CaDiCaL, Lingeling, Plingeling, Treengeling, YalSAT Entering the SAT Competition 2017. In Proceedings of SAT Competition 2017 - Solver and Benchmark Descriptions, Tomas Tomáš, Marijn Heule, Matti Järvisalo (editors), vol. B-2017-1 of Department of Computer Science Series of Publications B, pages 14-15, University of Helsinki, 2017.
[ paper | bibtex ]

Armin Biere. Yet another Local Search Solver and Lingeling and Friends Entering the SAT Competition 2014. In Proceedings of SAT Competition 2014, Adrian Balint, Anton Belov, Marijn Heule, Matti Järvisalo (editors), vol. B-2014-2 of Department of Computer Science Series of Publications B, pages 39-40, University of Helsinki, 2014.
[ paper | bibtex ]

Adrian Balint, Armin Biere, Andreas Fröhlich, Uwe Schöning. Improving implementation of SLS solvers for SAT and new heuristics for k-SAT with long clauses. In Proc. 17th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'14), Lecture Notes in Computer Science (LNCS) vol. 8561, 302-316, Springer 2014.