Paper Info
Title
Considering Circuit Observability Don't Cares in CNF Satisfiability
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.
Year
DOI
Venue
2005
10.1109/DATE.2005.102
DATE
Keywords
Field
DocType
contemporary sat solvers,zchaff sat solver,cnf-based sat,logic circuit description,circuit verification task,cnf representation,circuit observability,circuit verification,circuit unobservability,cnf-based sat solver,logic circuit,cnf satisfiability,data structures,computability,computer science,observability,boolean constraint propagation,sat solver,electronic design automation,logic design,logic synthesis,boolean satisfiability,combinatorial optimization,network synthesis,conjunctive normal form,logic circuits,satisfiability
Logic synthesis,#SAT,Logic gate,Computer science,Boolean satisfiability problem,Computability,Theoretical computer science,Conjunctive normal form,Solver,Unit propagation
Conference
ISSN
ISBN
Citations 
1530-1591
0-7695-2288-2
19
PageRank 
References 
Authors
0.94
9
3
Name
Order
Citations
PageRank
Zhaohui Fu128314.28
Yinlei Yu2955.96
Sharad Malik37766691.24