Hybrid DPLL-Style SAT Solver
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 , 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 . For circuit application domains such as Automatic Test Pattern Generation (ATPG) , equivalence checking , and Bounded Model Checking (BMC) , 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.
KeywordsConjunctive Normal Form Hybrid Representation Bound Model Check Circuit Structure Automatic Test Pattern Generation
Unable to display preview. Download preview PDF.