Function-Complete Lookahead in Support of Efficient SAT Search Heuristics

John Franco (University of Cincinnati, USA)

Michal Kouril (University of Cincinnati, USA)

John Schlipf (University of Cincinnati, USA)

Sean Weaver (University of Cincinnati, USA)

Michael Dransfield (National Security Agency, USA)

W. Mark Vanfleet (National Security Agency, USA)

Abstract: Recent work has shown the value of using propositional SAT solvers, as opposed to pure BDD solvers, for solving many real-world Boolean Satisfiability problems including Bounded Model Checking problems (BMC). We propose a SAT solver paradigm which combines the use of BDDs and search methods to support efficient implementation of complex search heuristics and effective use of early (preeprocessor) learning. We implement many of these ideas in software called SBSAT. We show that SBSAT solves many of the benchmarks tested competitively or substantially faster than state-of-the-art SAT solvers.

SBSAT differs from standard propositional SAT solvers by working directly with non-CNF propositional input, its input format is BDDs. This allows some BDD-style processing to be used as a preprocessing tool. After preprocessing, the BDDs are transformed into state machines (different state machines than the ones used in the original model checking problem) and a good deal of lookahead information is precomputed and memoized. This provides for fast implementation of a new form of look ahead, called local-function-complete lookahead (contrasting with the depth-first lookahead of zChaff [Moskewicz et al. 01] and the breadth-first lookahead of Prover [Stålmarck 94]). SBSAT provides a choice of search heuristics, allowing users to exploit domain-specific experience. We describe SBSAT in this paper.

We use SBSAT in conjunction with the tool bmc from Carnegie Mellon to translate a bounded model checking problem to classical propositional logic and then use SBSAT to solve the bmc output. We show this approach is faster than the now traditional approach of translating the bmc output to CNF clauses and using a CNF-based SAT solver, such as zChaff. The work continues that of [Franco et al. 01] and [Franco et al. 04].

Keywords: Binary Decision Diagrams, Bounded Model Checking, DAG, Satisfiability, Satisfiability Decision Heuristics, State Machines

Categories: B.6.1, F.4.1