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.

Issue  "./configure.sh && make" to compile the binary 'splatz'.

For license and copying information see LICENSE.

Armin Biere