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.
Keywords for this software
References in zbMATH (referenced in 9 articles )
Showing results 1 to 9 of 9.
- Junttila, Tommi; Karppa, Matti; Kaski, Petteri; Kohonen, Jukka: An adaptive prefix-assignment technique for symmetry reduction (2020)
- Li, Chu-Min; Xiao, Fan; Luo, Mao; Manyà, Felip; Lü, Zhipeng; Li, Yu: Clause vivification by unit propagation in CDCL SAT solvers (2020)
- Beleĭ, Evgeniya Gennad’evna; Semënov, Aleksandr Anatol’evich: On propositional coding techniques for the distinguishability of objects in finite sets (2019)
- Tonello, Elisa; Farcot, Etienne; Chaouiya, Claudine: Local negative circuits and cyclic attractors in Boolean networks with at most five components (2019)
- Baud-Berthier, Guillaume; Giráldez-Cru, Jesús; Simon, Laurent: On the community structure of bounded model checking SAT problems (2017)
- Hyttinen, Antti; Plis, Sergey; Järvisalo, Matti; Eberhardt, Frederick; Danks, David: A constraint optimization approach to causal discovery from subsampled time series data (2017)
- Junttila, Tommi; Karppa, Matti; Kaski, Petteri; Kohonen, Jukka: An adaptive prefix-assignment technique for symmetry reduction (2017)
- 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)
- Niemetz, Aina; Preiner, Mathias; Biere, Armin: Propagation based local search for bit-precise reasoning (2017)