Please use this identifier to cite or link to this item:
|Title:||Considering circuit observability don't cares in CNF satisfiability|
|Authors:||Fu, Z. |
|Citation:||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  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       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|
|Appears in Collections:||Staff Publications|
Show full item record
Files in This Item:
There are no files associated with this item.
checked on Feb 20, 2019
checked on Nov 17, 2018
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.