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.