LSAT - The light SAT-solver

LSAT

Documentation

Copyright

Description

LSAT is a leight weight SAT-solver tailored for diagnosing systems, based on propositional models, e.g., digital circuits. Unlike many other SAT-solvers it can compute all possible truth assignments for any formula in DIMACS CNF - given it can determine at least one solution at all. It is based on a non-destructive DPLL variant using mutually linked lists, and is able to minimalise the result set with respect to a predetermined set of "components"/variables.

Download

Source code: lsat-0.0.2.tar.gz (1.13 MBytes)

Documentation

Installation:

In order to install and run LSAT you will need a C and a C++ compiler, such as GCC. Inside the LSAT distribution you may run configure, make, and make install (as root), if you're on a Unix-ish system. For a list of available program options start LSAT with the '--help' parameter. Further information is available in LSAT's README file, while example DIMACS-files may be found in the examples/ directory.

The 20 Seconds Introduction to DIMACS CNF:

The common DIMACS CNF format looks somewhat like this:

  p a c
  1 2 3 0
  4 -5 0
  ...

where a is the number of occurring atoms, and c the number of occurring clauses. Atoms are linearly numbered from 1 to a, whereas each clause closes with a trailing 0 that is not interpreted by the SAT-solver. A number of DIMACS sample files is also available from the DIMACS ftp server.

LSAT also accepts a slightly different CNF format: 1. the trailing 0 can be omitted from each clause, 2. an a directive can be used in order to define which variables constitute "components" which - according to a system description - may be anormal.

  p 5 10
  a 5 3
  1 2 3
  4 -5
  ...

This example defines variables 5 and 3 as "components" which may be arnomal. Potentially abnormal atoms are also the minimalisation criterion for LSAT. For further details, see also:

• Andreas Bauer. Simplifying diagnosis using LSAT: a propositional approach to reasoning from first principles. In Proceedings of the 2005 International Conference on Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems (CP-AI-OR), volume 3524 of Lecture Notes in Computer Science, Prague, Czech Republic, pages 49-63, June 2005. Springer-Verlag.

Copyright

Copyright © 2004 - 2005 Andreas Bauer <baueran@in.tum.de>

LSAT is released under the terms of the GNU General Public License. For more information, see the README and COPYING documents provided with the LSAT program. Have fun!