Please use this identifier to cite or link to this item:
Title: Extracting logic circuit structure from conjunctive normal form descriptions
Authors: Fu, Z. 
Malik, S.
Issue Date: 2007
Citation: Fu, Z., Malik, S. (2007). Extracting logic circuit structure from conjunctive normal form descriptions. Proceedings of the IEEE International Conference on VLSI Design : 37-42. ScholarBank@NUS Repository.
Abstract: Boolean Satisfiability is seeing increasing use as a decision procedure in Electronic Design Automation (EDA) and other domains. Most applications encode their domain specific constraints in Conjunctive Normal Form (CNF), which is accepted as input by most efficient contemporary SAT solvers [1-3]. However, such translation may have information loss. For example, when a circuit is encoded into CNF, structural information such as gate orientation, logic paths, signal observability, etc. is lost. However, recent research [4-6] shows that a substantial amount of the lost information can be restored in circuit form. This paper presents an efficient algorithm (CNF2CKT) for extracting circuit information from CNF instances. CNF2CKT is optimal in the sense that it extracts a maximum acyclic combinational circuit from any given CNF using the logic gates pre-specified in a library. The extracted circuit structure is valuable in various ways, particularly when the CNF is not encoded from the circuit, or the circuit description is not readily available. As an example, we show that the extracted circuit structure can be used to derive Circuit Observability Don't Cares [7] for speeding up CNF-SAT [8]. © 2007 IEEE.
Source Title: Proceedings of the IEEE International Conference on VLSI Design
ISBN: 0769527620
ISSN: 10639667
DOI: 10.1109/VLSID.2007.81
Appears in Collections:Staff Publications

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


checked on Sep 26, 2022


checked on Sep 19, 2022

Page view(s)

checked on Sep 22, 2022

Google ScholarTM



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