Splatz SAT Solver

Description

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.

Period	04 Jul 2016
Event title	7th Workshop on Pragmatics of SAT (POS'16)
Event type	Conference
Location	FranceShow on map