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:

1. 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.

2. 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.
3. 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 2006. There are more experimental and recent versions - please ask Sean Weaver for the latest version if you are interested.

  Instructions: download the file above, then

      tar xfz sbsat-2.5b-5.tar.gz
      cd sbsat-2.5b-5
      ./configure
      make
      make check
      make install
  

  See the Makefile for more compilation options. Run

      sbsat --help
  

  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 Science, 2006.

• copyright notice