https://scholars.lib.ntu.edu.tw/handle/123456789/499726
標題: | Interpolant generation without constructing resolution graph. | 作者: | Hsu, Chih-Jen Huang, Shao-Lun Wu, Chi-An CHUNG-YANG HUANG |
公開日期: | 2009 | 起(迄)頁: | 9-12 | 來源出版物: | 2009 International Conference on Computer-Aided Design, ICCAD 2009, San Jose, CA, USA, November 2-5, 2009 | 摘要: | In this paper, we proposed a novel interpolant generation algorithm without constructing the resolution graph of the unsatisfiability proof. Our algorithm generates the interpolant by building sub-interpolants from conflict analyses and then merges them based on the last decision conflict. The experimental results show that our algorithm has the advantages over the prior interpolant generation techniques in both memory usage and interpolation circuit size. Copyright 2009 ACM. |
URI: | https://scholars.lib.ntu.edu.tw/handle/123456789/499726 https://www.scopus.com/inward/record.uri?eid=2-s2.0-76349118305&doi=10.1145%2f1687399.1687402&partnerID=40&md5=d6bb8c5adf3268868663693c1555955b |
DOI: | 10.1145/1687399.1687402 | SDG/關鍵字: | Computer aided design; Circuit size; Conflict analysis; Decision conflicts; Generation algorithm; Generation techniques; Interpolants; Memory usage; Resolution graphs; Interpolation |
顯示於: | 電機工程學系 |
在 IR 系統中的文件,除了特別指名其著作權條款之外,均受到著作權保護,並且保留所有的權利。