||Introduction: A State-Based Satisfiability Solver
Recent work has shown the value of using propositional SAT solvers for
solving many real-world Boolean Satisfiability problems including
bounded model checking, equivalence checking, protocol verification,
and others. SBSAT is a research platform for testing ideas that will
improve SAT solver performance on these and other problems. SBSAT
combines BDD manipulation and search methods to support efficient
implementation of complex search heuristics and effective use of early
(preprocessor) learning. SBSAT solves many of the benchmarks tested
competitively substantially faster than other state-of-the-art SAT
SBSAT differs from conventional propositional SAT solvers by working
directly with non-CNF propositional input. Its input format is BDDs.
This allows the use of BDD operations in preprocessing. After
preprocessing, the BDDs are transformed into state machines. Each
state machine represents all possible search states and state
transitions for a single function. Functions represented by these
state machines are generally different than the ones used in the
original input due to the preprocessing step where a good deal of
search lookahead information has been precomputed and memoized in the
states and state transitions. Thus, the state-based paradigm provides
for fast implementation of what we call local-function-complete
lookahead, which complements the depth-first lookahead of zChaff and
variants and the breadth-first lookahead of Prover, and facilitates a
wider range of complex yet efficient search heuristics which allow
exploitation of domain-specific knowledge.
Superior performance can be achieved due the following:
Judicious separation of global information (that is,
information pertinent to the entire formula or subformula)
from local information (that is, information relating to a
piece of the formula or subformula, called a component). Complete
global information provides a solution immediately but is costly to
acquire; whereas primitive local information is cheap to maintain but
usually can be used to derive a solution only with a great deal of
effort (for example, by resolution). Clusters of local information
represent a compromise: although solutions do not follow immediately
from such clusters, much less work is usually needed to derive a
solution from clusters than from an unprocessed input.
Moreover, in many applications, formula components naturally occur in
clusters. State-of-the-art SAT solvers, based on CNF translations,
often do not enjoy the benefit of such knowledge because it is
typically garbled during translation. By working directly with
natural clusters, we stay as much as possible in the original problem
domain and take advantage of the cluster information directly. In
some formal verification problems, BDD tools provide efficient
operators which exploit cluster information. Our approach is designed
to exploit this information in similar fashion. Thus, we do no worse
than BDD-based methods on such problems.
Precomputation of local inferences and heuristic information and
efficient access to this information at branch points in a search for
a solution. The information separation stated above typically reduces
the number of branches in a search. But, the time-per-branch can be
reduced also by precomputing any information that can be used
effectively later. Such information includes both binary and unary
inferences which can be made as well as literal weights (partially)
which may be used in some advanced variable selection rule. Since the
amount of precomputed information increases with cluster size,
Items 1. and 2. cooperate in a unique way.
Dynamic management of global information (lemmas). Inferences which
always apply, called lemmas here, are memoized when they are
discovered. The data base holding these inferences allows reasonably
efficient access to them. They may be used at various points in the
search to prevent fruitless exploration of a search subspace. As is
the case for other state-of-the-art SAT solvers, each global inference
may be viewed as a resolvent of two "clauses" representing a left
branch and a right branch at a choice point. Thus, our search for a
solution can be viewed as a mix between Davis-Putnam style tree
resolution and general resolution. Shorter searches are typically
possible with general resolution, but trying to find the right order
of search is hard. In Davis-Putnam variants, effective heuristics for
choosing search order are easier to invent. SBSAT uses Davis-Putnam
to choose variables but also do general resolution when a fruitful
opportunity presents itself.
- complete distribution
Easily compiles under unix operating systems using the gnu C++
compiler. Can compile in Windows with Cygwin. This version dates to
2010. There are more experimental and recent versions - please
ask Sean Weaver for the
latest version if you are interested.
Instructions: make sure you have bison, flex, and help2man installed.
Then download the file above and do the following:
tar xfz sbsat-2.7b.tar.gz
See the Makefile for more compilation options. Run
to see most runtime options.
Mac users can try macports
- user manual
Not yet complete but can get you started.
- description of sbsat
An article that was published in the Journal of Universal Computer
- Finally, do 'git clone git://github.com/nerdling/SBSAT.git' if you want the latest.
- copyright notice