Paper Info
Title
Exploiting Circuit Reconvergence through Static Learning in CNF SAT Solvers
Abstract
Most contemporary SAT solvers use a conjunctive-normal-form (CNF) representation for logic functions due to the availability of efficient algorithms for this form, such as deduction through unit propagation and conflict driven learning using clause resolution. The use of CNF generally entails transformation to this form from other representations such as logic circuits (Tseitin, 1970). However, this transformation results in loss of information such as direction of signal flow and observability of signals at circuit outputs (Een, 2003)(Fu, 2005). This has prompted the development of various circuit-based solvers (Ganai et al., 2002), hybrid CNF+circuit-based solvers (Fu, 2005), as well as augmented CNF solvers (Een, 2003). Having the circuit available provides for additional capabilities at a cost, and thus requires careful analysis to determine the viability of each approach. This paper highlights one specific capability provided by a circuit: the ability to consider reconvergent paths in unit propagation. Unit propagation is the workhorse of contemporary SAT solvers, thus any improvement to this has significant practical potential. We first demonstrate that the Tseitin circuit-to-CNF transformation limits backward unit propagation and how additional implications can be derived when unit propagation across multiple paths is considered. Next, we show how these implications can be exploited by statically learning clauses during circuit pre-processing. The results of the practical implementation of these algorithms show that the static learning can provide significant speed-up on several classes of benchmark circuits. Finally, we discuss how this work compares with other circuit-based approaches, especially those arising from the automatic-test-pattern-generation (ATPG) community (e.g. recursive learning) and circuit and non- circuit based pre-processors.
Year
DOI
Venue
2008
10.1109/VLSI.2008.90
VLSI Design
Keywords
Field
DocType
various circuit-based solvers,conjunctive-normal-form representation,exploiting circuit reconvergence,static learning,non-circuit based pre-processors,cnf sat solvers,mark circuit,atpg,backward unit propagation,augmented cnf solvers,circuit-based solvers,contemporary sat solvers,circuit reconvergence,reconvergent paths,automatic test pattern generation,computability,unit propagation,logic design,cnf gen,circuit pre-processing,hybrid cnf,automatic-test-pattern-generation,electronic design automation,logic circuit,circuit preprocessing,sat solver,conjunctive normal form
Logic synthesis,Automatic test pattern generation,Observability,Logic gate,Computer science,Electronic engineering,Computability,Electronic design automation,Unit propagation,Electronic circuit
Conference
ISSN
ISBN
Citations 
1063-9667
0-7695-3083-4
0
PageRank 
References 
Authors
0.34
17
3
Name
Order
Citations
PageRank
Yinlei Yu1955.96
Cameron Brien200.68
Sharad Malik37766691.24