Limmat

News

Version 1.1 is a 64-bit port to Linux on Alpha. A configure script was added and the broken time out option was fixed. The default time out is one hour. The latest version 1.3 adds the possibility to change the rescoring factor at runtime. A detailed listing of new features can be found in the NEWS file that comes with the sources.

Download

[ limmat-1.3.tar.gz ]

Above you find the sources of the SAT solver Limmat. The SAT problem is the classical NP complete problem of searching for a satisfying assignment of a propositional formula in conjunctive normal form (CNF).

License

Limmat uses a BSD style license. In essence, you can use and modify the sources as you like provided that you acknowledge the origin of the software. More details can be found in the LICENSE file that comes with the sources.

Background

In recent years there has been an tremendous increase in reasoning power enabling SAT solvers to handle very large formulae and solving large real world problems. You may want to note, that Limmat won the SAT2002 competition in the category all solvers on satisfiable industrial benchmarks, which in essence is the category, where realistic examples are checked, with the emphasis on finding bugs.

General information on the SAT problem can be found at www.cs.ubc.ca/~hoos/SATLIB.