This is the second public release of Limmat a satisfiability solver.  It
reads a propositional formula in Dimacs format and checks it for
satisfiability.  Limmat is inspired by Chaff and Grasp.  In addition it
provides a fast conflict detection mechanism in boolean constraint
propagation and compared to Chaff fast access to both watched literals in a
clause.  It is implemented in C with handcrafted data structures and
includes a solid test frame work.

First you should read the information contained in the LICENSE file, for the
rights on using this software.  Then see INSTALL for information on how to
compile Limmat and USAGE for using it.


Armin Biere, Zurich, July 4, 2002.