SSAT is an experimental solver and preprocessor for Boolean formula satisfaction problems (SAT). It is a simple piece of software consisting of several command line tools - a SAT solver, an arc-consistency SAT preprocessor, a projection consistency SAT preprocessor and some other testing programs.

I wrote this program to do some experiments with solving SAT problems. Another reason for writing this software is to show that structural properties of SAT problems are not completely utilized in today's state-of-the-art solvers. This is particularly true for difficult unsatisfiable SAT instances (see Fadi Aloul's home page). Even today's state-of-the-art SAT solvers (such as MiniSAT) needs lot of time to answer these relatively small problems.

SSAT is written in C++ with significant use of Standard Template Library (STL).

Change log
Version 0.2.40: additional experimental code and corrections of the sCommon library by Adam Nohejl.

Keywords: SAT solver, SAT preprocessor, difficult SAT instances, consistency, propagation