Hybrid DPLL-Style SAT Solver

Part of the Series on Integrated Circuits and Systems book series (ICIR)

The Boolean Satisfiability (SAT) problem has extensive applications in VLSI CAD. Recent advances in SAT solvers based on Conjunctive Normal Form (CNF) representation have resulted in significantly improved performance. In particular, innovative techniques for decision variable selection [38], Boolean constraint propagation (BCP) [36, 38], and backtracking with conflict analysis based learning [37, 38] have led to highperformance CNF-based SAT solvers like Chaff [38]. For circuit application domains such as Automatic Test Pattern Generation (ATPG) [143], equivalence checking [39], and Bounded Model Checking (BMC) [66], the Boolean reasoning problem is typically derived from the circuit structure. This has also led to interest in circuit-based SAT solvers [39, 143-145], which use circuit specific knowledge to guide the search.


Conjunctive Normal Form Hybrid Representation Bound Model Check Circuit Structure Automatic Test Pattern Generation 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer Science+Business Media, LLC 2007

Personalised recommendations