YalSAT

YalSAT Yet Another Local Search Solver. 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


References in zbMATH (referenced in 10 articles )

Showing results 1 to 10 of 10.
Sorted by year (citations)

  1. Junttila, Tommi; Karppa, Matti; Kaski, Petteri; Kohonen, Jukka: An adaptive prefix-assignment technique for symmetry reduction (2020)
  2. Li, Chu-Min; Xiao, Fan; Luo, Mao; Manyà, Felip; Lü, Zhipeng; Li, Yu: Clause vivification by unit propagation in CDCL SAT solvers (2020)
  3. Semenov, Alexander; Otpuschennikov, Ilya; Gribanova, Irina; Zaikin, Oleg; Kochemazov, Stepan: Translation of algorithmic descriptions of discrete functions to SAT with applications to cryptanalysis problems (2020)
  4. Beleĭ, Evgeniya Gennad’evna; Semënov, Aleksandr Anatol’evich: On propositional coding techniques for the distinguishability of objects in finite sets (2019)
  5. Kauers, Manuel; Seidl, Martina; Zeilberger, Doron: On the maximal minimal cube lengths in distinct DNF tautologies (2019)
  6. Kiesl, Benjamin; Heule, Marijn J. H.; Biere, Armin: Truth assignments as conditional autarkies (2019)
  7. Semenov, Alexander A.: Merging variables: one technique of search in pseudo-Boolean optimization (2019)
  8. Tonello, Elisa; Farcot, Etienne; Chaouiya, Claudine: Local negative circuits and cyclic attractors in Boolean networks with at most five components (2019)
  9. Hyttinen, Antti; Plis, Sergey; Järvisalo, Matti; Eberhardt, Frederick; Danks, David: A constraint optimization approach to causal discovery from subsampled time series data (2017)
  10. Niemetz, Aina; Preiner, Mathias; Biere, Armin: Propagation based local search for bit-precise reasoning (2017)