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 25 articles )

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

1 2 next

  1. Alam, Jawaherul Md.; Bekos, Michael A.; Dujmović, Vida; Gronemann, Martin; Kaufmann, Michael; Pupyrev, Sergey: On dispersable book embeddings (2021)
  2. Fleury, Mathias; Biere, Armin: Efficient all-UIP learned clause minimization (2021)
  3. Froleyks, Nils; Heule, Marijn; Iser, Markus; Järvisalo, Matti; Suda, Martin: SAT competition 2020 (2021)
  4. Giráldez-Cru, Jesús; Levy, Jordi: Popularity-similarity random SAT formulas (2021)
  5. Heule, Marijn J. H.; Kauers, Manuel; Seidl, Martina: New ways to multiply (3 \times3)-matrices (2021)
  6. Manthey, Norbert: The \textscMergeSatsolver (2021)
  7. Nawrocki, Wojciech; Liu, Zhenjun; Fröhlich, Andreas; Heule, Marijn J. H.; Biere, Armin: XOR local search for Boolean Brent equations (2021)
  8. Schreiber, Dominik; Sanders, Peter: Scalable SAT solving in the cloud (2021)
  9. Junttila, Tommi; Karppa, Matti; Kaski, Petteri; Kohonen, Jukka: An adaptive prefix-assignment technique for symmetry reduction (2020)
  10. Kaufmann, Daniela; Biere, Armin; Kauers, Manuel: Incremental column-wise verification of arithmetic circuits using computer algebra (2020)
  11. Kochemazov, Stepan: Improving implementation of SAT competitions 2017--2019 winners (2020)
  12. Li, Chu-Min; Xiao, Fan; Luo, Mao; Manyà, Felip; Lü, Zhipeng; Li, Yu: Clause vivification by unit propagation in CDCL SAT solvers (2020)
  13. Otpuschennikov, Ilya V.; Semenov, Alexander A.: Using merging variables-based local search to solve special variants of MaxSAT problem (2020)
  14. Pashkovich, Kanstantsin; Poirrier, Laurent: Three-dimensional stable matching with cyclic preferences (2020)
  15. 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)
  16. Vallade, Vincent; Le Frioux, Ludovic; Baarir, Souheib; Sopena, Julien; Ganesh, Vijay; Kordon, Fabrice: Community and LBD-based clause sharing policy for parallel SAT solving (2020)
  17. Wenjie Zhang, Zeyu Sun, Qihao Zhu, Ge Li, Shaowei Cai, Yingfei Xiong, Lu Zhang: NLocalSAT: Boosting Local Search with Solution Prediction (2020) arXiv
  18. Yolcu, Emre; Wu, Xinyu; Heule, Marijn J. H.: Mycielski graphs and PR proofs (2020)
  19. Beleĭ, Evgeniya Gennad’evna; Semënov, Aleksandr Anatol’evich: On propositional coding techniques for the distinguishability of objects in finite sets (2019)
  20. Kauers, Manuel; Seidl, Martina; Zeilberger, Doron: On the maximal minimal cube lengths in distinct DNF tautologies (2019)

1 2 next