Function-Complete Lookahead in Support of Efficient SAT Search Heuristics

Простая страница элемента
dc.creatorFranco,John
dc.creatorKouril,Michal
dc.creatorSchlipf,John
dc.creatorWeaver,Sean
dc.creatorDransfield,Michael
dc.creatorVanfleet,W.
dc.date2004
dc.date.accessioned2024-02-06T12:53:16Z
dc.date.available2024-02-06T12:53:16Z
dc.descriptionRecent 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].
dc.formattext/html
dc.identifierhttps://doi.org/10.3217/jucs-010-12-1655
dc.identifierhttps://lib.jucs.org/article/28327/
dc.identifier.urihttps://openrepository.mephi.ru/handle/123456789/8666
dc.languageen
dc.publisherJournal of Universal Computer Science
dc.relationinfo:eu-repo/semantics/altIdentifier/eissn/0948-6968
dc.relationinfo:eu-repo/semantics/altIdentifier/pissn/0948-695X
dc.rightsinfo:eu-repo/semantics/openAccess
dc.rightsJ.UCS License
dc.sourceJUCS - Journal of Universal Computer Science 10(12): 1655-1692
dc.subjectBinary Decision Diagrams
dc.subjectBounded Model Checking
dc.subjectDAG
dc.subjectSatisfiability
dc.subjectState Machines
dc.subjectSatisfiability Decision Heuristics
dc.titleFunction-Complete Lookahead in Support of Efficient SAT Search Heuristics
dc.typeResearch Article
Файлы
Коллекции