Please use this identifier to cite or link to this item: https://doi.org/10.1109/DATE.2005.102
DC FieldValue
dc.titleConsidering circuit observability don't cares in CNF satisfiability
dc.contributor.authorFu, Z.
dc.contributor.authorYu, Y.
dc.contributor.authorMalik, S.
dc.date.accessioned2013-07-04T08:00:09Z
dc.date.available2013-07-04T08:00:09Z
dc.date.issued2005
dc.identifier.citationFu, 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. <a href="https://doi.org/10.1109/DATE.2005.102" target="_blank">https://doi.org/10.1109/DATE.2005.102</a>
dc.identifier.isbn0769522882
dc.identifier.issn15301591
dc.identifier.urihttp://scholarbank.nus.edu.sg/handle/10635/40256
dc.description.abstractBoolean 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.
dc.description.urihttp://libproxy1.nus.edu.sg/login?url=http://dx.doi.org/10.1109/DATE.2005.102
dc.sourceScopus
dc.typeConference Paper
dc.contributor.departmentCOMPUTER SCIENCE
dc.description.doi10.1109/DATE.2005.102
dc.description.sourcetitleProceedings -Design, Automation and Test in Europe, DATE '05
dc.description.volumeII
dc.description.page1108-1113
dc.identifier.isiutNOT_IN_WOS
Appears in Collections:Staff Publications

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

SCOPUSTM   
Citations

27
checked on Dec 8, 2022

Page view(s)

162
checked on Dec 8, 2022

Google ScholarTM

Check

Altmetric


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