Splatz

This is the SAT solver Splatz. It is a reimplementation of some of the ideas used in Lingeling, but based on more recent insights from our SAT’15 and POS’15 papers. The list of inprocessing techniques is way smaller and thus on many benchmarks Lingeling is superior. This solver accepts more clauses and variables than Lingeling though, is better documented and tries to be more easier to extend. In contrast to Lingeling it is implemented in C++ and not C, and does not have an API yet. All data structures are statically allocated.


References in zbMATH (referenced in 12 articles )

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

  1. Junttila, Tommi; Karppa, Matti; Kaski, Petteri; Kohonen, Jukka: An adaptive prefix-assignment technique for symmetry reduction (2020)
  2. Kaufmann, Daniela; Biere, Armin; Kauers, Manuel: Incremental column-wise verification of arithmetic circuits using computer algebra (2020)
  3. Li, Chu-Min; Xiao, Fan; Luo, Mao; Manyà, Felip; Lü, Zhipeng; Li, Yu: Clause vivification by unit propagation in CDCL SAT solvers (2020)
  4. 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)
  5. Wenjie Zhang, Zeyu Sun, Qihao Zhu, Ge Li, Shaowei Cai, Yingfei Xiong, Lu Zhang: NLocalSAT: Boosting Local Search with Solution Prediction (2020) arXiv
  6. Beleĭ, Evgeniya Gennad’evna; Semënov, Aleksandr Anatol’evich: On propositional coding techniques for the distinguishability of objects in finite sets (2019)
  7. Tonello, Elisa; Farcot, Etienne; Chaouiya, Claudine: Local negative circuits and cyclic attractors in Boolean networks with at most five components (2019)
  8. Baud-Berthier, Guillaume; Giráldez-Cru, Jesús; Simon, Laurent: On the community structure of bounded model checking SAT problems (2017)
  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. Junttila, Tommi; Karppa, Matti; Kaski, Petteri; Kohonen, Jukka: An adaptive prefix-assignment technique for symmetry reduction (2017)
  11. Nejati, Saeed; Newsham, Zack; Scott, Joseph; Liang, Jia Hui; Gebotys, Catherine; Poupart, Pascal; Ganesh, Vijay: A propagation rate based splitting heuristic for divide-and-conquer solvers (2017)
  12. Niemetz, Aina; Preiner, Mathias; Biere, Armin: Propagation based local search for bit-precise reasoning (2017)