 
Recent work has shown the value of using propositional SAT solvers for
solving many realworld 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 stateoftheart SAT
solvers.
SBSAT differs from conventional propositional SAT solvers by working
directly with nonCNF 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 statebased paradigm provides
for fast implementation of what we call localfunctioncomplete
lookahead, which complements the depthfirst lookahead of zChaff and
variants and the breadthfirst lookahead of Prover, and facilitates a
wider range of complex yet efficient search heuristics which allow
exploitation of domainspecific 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. Stateoftheart 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 BDDbased 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 timeperbranch 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 stateoftheart 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 DavisPutnam 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 DavisPutnam variants, effective heuristics for
choosing search order are easier to invent. SBSAT uses DavisPutnam
to choose variables but also do general resolution when a fruitful
opportunity presents itself.
