Exploiting circuit reconvergence through static learning in CNF SAT solvers

Yinlei Yu, Cameron Brien, Sharad Malik

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Scopus citations

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 [23]. However, this transformation results in loss of information such as direction of signal flow and observability of signals at circuit outputs [12][13]. This has prompted the development of various circuit-based solvers [2][14][17][22], hybrid CNF+circuit-based solvers[13], as well as augmented CNF solvers [12]. 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 back-ward 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 bench-mark 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.

Original languageEnglish (US)
Title of host publicationProceedings - 21st International Conference on VLSI Design, VLSI DESIGN 2008
Pages461-468
Number of pages8
DOIs
StatePublished - Jul 25 2008
Event21st International Conference on VLSI Design, VLSI DESIGN 2008 - Hyderabad, India
Duration: Jan 4 2008Jan 8 2008

Publication series

NameProceedings of the IEEE International Frequency Control Symposium and Exposition

Other

Other21st International Conference on VLSI Design, VLSI DESIGN 2008
CountryIndia
CityHyderabad
Period1/4/081/8/08

All Science Journal Classification (ASJC) codes

  • Engineering(all)

Fingerprint Dive into the research topics of 'Exploiting circuit reconvergence through static learning in CNF SAT solvers'. Together they form a unique fingerprint.

Cite this