This is the wepage for the propositional satisfiabillity solver Umsat. The
main feature of the current version of Umsat is that it can handle a number
of constraint types other than clauses in CNF. Several of these constraints
require exponentially large encodings in CNF and would thus slow down a
pure CNF solver despite providing useful information for the solver. In
addition Umsat also implements an interface to tcl which allows tcl to
create and call solver objects in Umsat.
Umsat is based on the Minisat solver developed
at Chalmers. The current version of Umsat uses the solver core from Minisat
unchaged and implements a number of new constraint types, a different sett
of command line options and an interface to tcl.
Currenly we are working further extensions of the solver, and a better documentation
for users outside our research group. These inculde a few more natural
constraint types and the addition of new reasoning mechanisms
to allow the solver to rapildy handle several problem types known to have
exponential lower bounds in general resolution.
A student is also working on creating a system making it possible to utilise
multiple computers in order to solve large scale problem which are out of
reach for single machine SAT-solvers.
The source code of
Version 0.1 as a gzipped tar-archive. Questions regarding the code should be
directed to
Daniel Andrén
The manual in
postscript format.
Umsat has been developed by
Daniel Andrén
Lars Hellström
Klas Markström