Please use this identifier to cite or link to this item: https://doi.org/10.1109/DATE.2005.102
Title: Considering circuit observability don't cares in CNF satisfiability
Authors: Fu, Z. 
Yu, Y.
Malik, S.
Issue Date: 2005
Source: Fu, Z.,Yu, Y.,Malik, S. (2005). Considering circuit observability don't cares in CNF satisfiability. Proceedings -Design, Automation and Test in Europe, DATE '05 II : 1108-1113. ScholarBank@NUS Repository. https://doi.org/10.1109/DATE.2005.102
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.
Source Title: Proceedings -Design, Automation and Test in Europe, DATE '05
URI: http://scholarbank.nus.edu.sg/handle/10635/40256
ISBN: 0769522882
ISSN: 15301591
DOI: 10.1109/DATE.2005.102
Appears in Collections:Staff Publications

Show full item record
Files in This Item:
There are no files associated with this item.

SCOPUSTM   
Citations

25
checked on Dec 13, 2017

Page view(s)

52
checked on Dec 16, 2017

Google ScholarTM

Check

Altmetric


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.