Considering circuit observability don't cares in CNF satisfiability

Zhaohui Fu, Yinlei Yu, Sharad Malik

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

26 Scopus citations

Abstract

Boolean Satisfiability (SAT) has seen significant use in various tasks in circuit verification in recent years. A key contributor to the efficiency of contemporary SAT solvers is fast deduction using Boolean Constraint Propagation (BCP). This can be efficiently implemented with a Conjunctive Normal Form (CNF) representation of a circuit. However, most circuit verification tasks start from a logic circuit description of the problem instance. Fortunately, there is a simple conversion from a logic circuit to a CNF [12] that enables the use of the CNF representation even for circuit verification tasks. However, this process loses some information regarding the structure of the circuit. One example of such structural information is the Circuit Observability Don't Cares. Several recent papers [6] [7] [8] [9] [11] [13] have addressed the issue of handling circuit unobservability in CNF-based SAT. However, as we will demonstrate, none of these accurately captures the conditions for use of this information in all stages of a CNF-based SAT solver. In this paper, we propose a broader approach to take such Don't Care information into consideration in a CNF-based SAT solver. It does so by adding certain don 't care literals to clauses in the CNF representation. These don't care literals are treated differently at different times during the solution process, much like don't cares in logic synthesis. The major merit of this scheme, unlike other recently proposed techniques, is that the solver can continue to use this don't care information during the learning process, which is an important part of contemporary SAT solvers. We have implemented this approach in the zChaff SAT solver and experiments show that significant performance gain can be obtained through their use.

Original languageEnglish (US)
Title of host publicationProceedings - Design, Automation and Test in Europe, DATE '05
Pages1108-1113
Number of pages6
DOIs
StatePublished - Dec 1 2005
EventDesign, Automation and Test in Europe, DATE '05 - Munich, Germany
Duration: Mar 7 2005Mar 11 2005

Publication series

NameProceedings -Design, Automation and Test in Europe, DATE '05
VolumeII
ISSN (Print)1530-1591

Other

OtherDesign, Automation and Test in Europe, DATE '05
CountryGermany
CityMunich
Period3/7/053/11/05

All Science Journal Classification (ASJC) codes

  • Engineering(all)

Fingerprint Dive into the research topics of 'Considering circuit observability don't cares in CNF satisfiability'. Together they form a unique fingerprint.

  • Cite this

    Fu, Z., Yu, Y., & Malik, S. (2005). Considering circuit observability don't cares in CNF satisfiability. In Proceedings - Design, Automation and Test in Europe, DATE '05 (pp. 1108-1113). [1395741] (Proceedings -Design, Automation and Test in Europe, DATE '05; Vol. II). https://doi.org/10.1109/DATE.2005.102