https://scholars.lib.ntu.edu.tw/handle/123456789/632106
標題: | A Circuit-Based SAT Solver for Logic Synthesis | 作者: | Zhang H.-T JIE-HONG JIANG Mishchenko A. |
公開日期: | 2021 | 卷: | 2021-November | 來源出版物: | IEEE/ACM International Conference on Computer-Aided Design, Digest of Technical Papers, ICCAD | 摘要: | In recent years SAT solving has been widely used to implement various circuit transformations in logic synthesis. However, off-the-shelf CNF-based SAT solvers often have suboptimal performance on these challenging optimization problems. This paper describes an application-specific circuit-based SAT solver for logic synthesis. The solver is based on Glucose, a state-of-the-art CNF-based solver and adds a number of novel features, which make it run faster on multiple incremental SAT problems arising in redundancy removal and logic restructuring among others. In particular, the circuit structure of the problem instance is leveraged in a new way to guide variable decisions and to converge to a solution faster for both satisfiable and unsatisfiable instances. Experimental results indicate that the proposed solver leads to a 2-4x speedup, compared to the original Glucose. ©2021 IEEE |
URI: | https://www.scopus.com/inward/record.uri?eid=2-s2.0-85124145654&doi=10.1109%2fICCAD51958.2021.9643505&partnerID=40&md5=84f302f5bbb02a563ca44e29201ffde9 https://scholars.lib.ntu.edu.tw/handle/123456789/632106 |
ISSN: | 10923152 | DOI: | 10.1109/ICCAD51958.2021.9643505 | SDG/關鍵字: | Codes (symbols); Computer circuits; Glucose; Model checking; Timing circuits; Application specific; Circuit transformation; Logic restructuring; Optimization problems; Redundancy removal; SAT problems; SAT solvers; SAT-solving; State of the art; Sub-optimal performance; Logic Synthesis |
顯示於: | 電機工程學系 |
在 IR 系統中的文件,除了特別指名其著作權條款之外,均受到著作權保護,並且保留所有的權利。