SBSAT

SBSAT: a state-based, BDD-based satisfiability solver We present a new approach to SAT solvers, supporting efficient implementation of highly sophisticated search heuristics over a range of propositional inputs, including CNF formulas, but particularly sets of arbitrary boolean constraints, represented as BDDs. The approach preprocesses the BDDs into state machines to allow for fast inferences based upon any single input constraint. It also simplifies the set of constraints, using a tool set similar to standard BDD engines. And it memoizes search information during an extensive preprocessing phase, allowing for a new form of lookahead, called local-function-complete lookahead. This approach has been incorporated, along with existing tools such as lemmas, to build a SAT tool we call SBSAT.par Because of its memoization of constraint-by-constraint lookahead information, besides incorporation of standard lemmas, SBSAT also provides a convenient platform for experimentation with search heuristics. This experimentation is ongoing.par We show the feasibility of SBSAT by comparing it to zChaff on several of the benchmarks. We also show an interesting dependence of some standard benchmarks upon simply the independent/dependent variable distinction.