University of Limerick Institutional Repository

New and improved models for SAT-based bi-decomposition

DSpace Repository

Show simple item record

dc.contributor.author Chen, Huan
dc.contributor.author Marques-Silva, Joao
dc.date.accessioned 2012-12-20T14:20:33Z
dc.date.available 2012-12-20T14:20:33Z
dc.date.issued 2012
dc.identifier.uri http://hdl.handle.net/10344/2762
dc.description peer-reviewed en_US
dc.description.abstract Boolean function bi-decomposition is pervasive in logic synthesis. Bi-decomposition entails the decomposition of a Boolean function into two other simpler functions connected by a simple two-input gate. Existing solutions are based either on Binary Decision Diagrams (BDDs) or Boolean Satisfiability (SAT). Furthermore, the partition of the input set of variables is either assumed, or an automatic derivation is required. Most recent work on bi-decomposition proposed the use of Minimally Unsatisfiable Subformulas (MUSes) or Quantified Boolean Formulas (QBF) for computing, respectively, variable partitions of either approximate or optimum quality. This paper develops new grouporiented MUS-based models for addressing both the performance and the quality of bi-decompositions. The paper shows that approximate MUS search can be guided by the quality of well-known metrics. In addition, the paper improves on recent high-performance approximate models and versatile exact models, to address the practical requirements of bi-decomposition in logic synthesis. Experimental results obtained on representative benchmarks demonstrate significant improvement in performance as well as in the quality of decompositions. en_US
dc.language.iso eng en_US
dc.publisher Association for Computing Machinery en_US
dc.relation.ispartofseries GLSVLSI '12 Proceedings of the great lakes symposium on VLSI;pp. 141-146
dc.relation.uri http://dx.doi.org/10.1145/2206781.2206817
dc.rights "© ACM, 2012. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in GLSVLSI '12 Proceedings of the great lakes symposium on VLSI, pp. 141-146, http://dx.doi.org/10.1145/2206781.2206817 en_US
dc.subject bi-decomposition en_US
dc.subject logic synthesis en_US
dc.subject satisfiability en_US
dc.title New and improved models for SAT-based bi-decomposition en_US
dc.type info:eu-repo/semantics/conferenceObject en_US
dc.type.supercollection all_ul_research en_US
dc.type.supercollection ul_published_reviewed en_US
dc.contributor.sponsor SFI en_US
dc.relation.projectid BEACON 09/IN.1/I2618 en_US
dc.rights.accessrights info:eu-repo/semantics/openAccess en_US


Files in this item

This item appears in the following Collection(s)

Show simple item record

Search ULIR


Browse

My Account

Statistics