Sat Solvers.
Fahiem Bacchus, University of Toronto
The following software is available:
-
-
-
Before you download please be aware of the following legal restriction on the
use of the software.
Legal Matters
The software available at this site is
copyright (c) 1994-2002 Fahiem Bacchus. All rights are
reserved. Use of this software is permitted for non-commercial
research purposes, and it may be copied only for that use. All copies
must include this copyright message. This software and any
documentation and/or information supplied with it is distributed on an
as is basis. Fahiem Bacchus and the University of Toronto make no
warranties, express or implied, including but not limited to implied
warranties of merchantability and fitness for a particular purpose,
regarding the documentation, functions or performance of such
software, documentation and/or information.
If you would like to use any of this software for commercial purposes, please
contact
the author.
1. 2clseq-A DPLL Solver Using Extensive Binary Clause
Reasoning
2clseq is a DPLL SAT solver that utilizes extensive reasoning with
the binary clause subtheory at every node of the search tree. Since
this reasoning is performed dynamically many more opportunities arise
as we descend the search tree. In particular, as literals are valued
and clauses reduced many new binary clauses are produced.
2clseq displays very impressive performance. It is competitive with
the state of the art SAT solvers (state of the art in
2002). Interesting, with very few exceptions these other solvers
utilize only unit propagation at each node of the search tree,
avoiding any more complex forms of reasoning. In fact, prior to 2clseq
there has never been any convincing evidence that more reasoning at
each node could payoff in terms of improved performance.
The following two papers describe the approach.
-
Enhancing Davis Putnam with Extended
Binary Clause Reasoning,
F. Bacchus, National Conference on Artificial
Intelligence (AAAI-2002) to appear, 2002.
This paper presents the basic ideas that are the foundation of the
2clseq system.
-
Exploring the Computational Tradeoff
of more Reasoning and Less Searching,
F. Bacchus, Fifth International Symposium on Theory and
Applications of Satisfiability Testing, pages 7-16, 2002.
This paper presents some additional empirical data, and discusses
the issue of how much search can be saved by doing more reasoning.
Some more information about the software:
2clseq is written in C++ (using C++ as an improved version of C rather
than the object oriented nightmare that it can easily mutate to). It
should compile on almost any machine (including under Windows using
Visual C++).
This is version 2.0, it is the version that was entered in the
SAT2002 SAT
solvers competition. Check the competition web site for information
about how well 2clseq performed.
Version 2.0 features
- Binary Clause resolution, detection of hyper-resolvants, and
equality reduction (as described in my AAAI2002 paper linked
above).
- Intelligent backtracking via detection of conflicts.
- 2nd order relevance bounded clause learning which facilitates
a low overhead implementation.
- Five Heuristics:
- "-h 0" Lexographic variable ordering.
- "-h 1" MOMs, variable with largest number of active 2 clauses
break ties by number of active 3-clauses.
- "-h 2" Like 1, but chooses among tied variables randomly
(random tie breaking works well).
- "-h 3" Estimates the number of new 2-clauses that would
be produced, and picks variable that would generate
the largest number of new 2-clauses.
(Best for random problems.)
- "-h 4" The heursitic used in the competition. Like 2 but
does small amount of lookahead to see if it can detect
a few more new binary clauses.
- "-h 5" Like 3 except uses a TABU list to ensure that the same
variable is not always instantiated at the same level.
As far as I can tell from my experiments, use "-h 4" for non-random
problems and "-h 3" for random problems.
- A pacifier. As a rough estimate of how much progress the search
is making, the pacifier rate can be set with "-pcr K". Then every K
nodes of the search tree the highest level it backtracked to and the
deepest level the search reached during last K nodes is printed. (If the search
is spending most of its time at a very deep level of the search tree
odds are it won't finish anytime soon.)
- Statistics Log file. The file "timetable.dat" contains one line
for every problem run. The line is a comma separated list of the
following numbers:
- input file name
- [0,1,-1]: 0=UNSAT, 1=SAT -1=UNKNOWN
- total CPU seconds used
- CPU seconds used to do initial processing
- number of nodes searched (calls to DPLL)
- number of terminal nodes visited (leaves)
- fraction of times a hyper-resolvant was found amoung the times
one was searched for.
- number of hyper-resolvants found
- number of times a hyper-resovant was searched for
- number of pure literals reduced
- number of literal equalities found
- number of clause subsumptions found (in initial processing).
2. Hypre Preprocessor Software
The Hyper binary resolution + equality reduction inference used
inside of 2clseq has been implemented in a preprocessor. The
preprocessor often does a rather remarkable job of simplifying
formulas, working best on structured formulas. The following paper describes the
approach (which is quite different from the approach used in 2clseq)
Some more information about the software.
- hypre the preprocessor itself. By default when run with an
input file "foo.cnf" produces the output file "foo_out.cnf". Each run adds
a data line to "preprocessor.dat". The fields of this file are:
input file name, solution status (with 0 = UNSAT, 1 = SAT, -1 =
UNRESOLVED by the preprocessor), original number of variables. The output file "foo_out.cnf"
contains a mapping of the original variables. The mapping specifies what
happened to each of the original variables (whether or not they became true or
false, disappeared from the theory, or were made equal to some other variable).
The mapping is specified as a set of comment lines at the top of the DIMACS
formatted "foo_out.cnf". With the mapping one can map solutions of the
perprocessed formula to solutions of the original formula. Some software
along these lines is provided as the next two items.
- modelcheck takes a file containing a v-line (a solution in the
format used by the SAT competition: a line starting with a 'v' followed by a
list of the true literals terminated by 0) and a .cnf file and determines whether or not the solution specified by the
v-line satisfies the .cnf theory.
- vline takes as input a file containing a v-line, and a
file output by the preprocessor (a *_out.cnf file) and generates a
file containing a new v-line. The new v-line should be a solution to
the original *.cnf file. This is accomplished by using the map placed
in the *_out.cnf file by the preprocessor. By
- running the preprocessor on an original cnf file foo.cnf one
obtains foo_out.cnf, a simplified cnf file.
- solving foo_out.cnf and placing the v-line solution (dependent on
the solver one might need to edit its output) in an
output file foo.vline
- running v-line on foo.vline to get vline.out
- running modelcheck on vline.out and foo.cnf
one can check that the solution to the preprocessed file correctly
maps to a solution to the original cnf theory.
3. NoClause DPLL solver that solves non-clausal
theories.
The following paper describes the approach:
This suite is due to
M. Velev. It demonstrates the ISCAS format NoClause can take as
input. NoClause can also solve any of the other ISCAS format suites
from Velev's benchmark site.
To my home page.