English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Recent work has shown the value of using propositional SAT solvers, as opposed to pure BDD solvers, for solving many real-world Boolean Satisfiability prob- lems 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 (preprocessor) 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 pro- cessing to be used as a preprocessing tool. After preprocessing, the BDDs are trans- formed 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 lookahead, called local-function-complete lookahead (contrasting with the depth-first lookahead of zChaff (Moskewicz et al. 01) and the breadth-first lookahead of Prover (Stalmarck 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

Function-Complete Lookahead in Support of Efficient SAT Search Heuristics