Function-Complete Lookahead in Support of Efficient SAT Search Heuristics

摘要: Recent work has shown the value of using propositional SAT solvers, as opposed to pure BDD for solving many real-world Boolean Satisfiability prob- lems including Bounded Model Checking problems (BMC). We propose a solver paradigm which combines use BDDs and search methods support efficient implementation complex heuristics effective early (preprocessor) learning. implement these ideas in software called SBSAT. show that SBSAT solves benchmarks tested competitively or substantially faster than state-of-the-art solvers. differs from standard solvers by working directly with non- CNF input; its input format is BDDs. This allows some BDD-style pro- cessing be used preprocessing tool. After preprocessing, are trans- formed into state machines (different ones original model checking problem) good deal lookahead information precomputed memoized. provides fast new form lookahead, local-function-complete (contrasting depth-first zChaff (Moskewicz et al. 01) breadth-first Prover (Stalmarck 94)). choice heuristics, allowing users exploit domain-specific experience. describe this paper. conjunction tool bmc Carnegie Mellon translate bounded problem classical logic then solve output. approach now traditional translating output clauses CNF-based solver, such