Engineering a Circuit-Based SAT Solver and Its Applications on Functional Dependency Analysis and Refutation Proof Extraction
Date Issued
2007
Date
2007
Author(s)
Lee, Chih-Chun
DOI
en-US
Abstract
In the first part of the thesis, we have devised a circuit SAT solver with the ability to exploit inherent circuit structure properties for circuit oriented problems based on the concept of justification frontiers. With J-clauses, an extension of J-gates [1], the deduction equipped with justification frontiers can be done on clauses instead of gates while preserving the circuit structure. With DPLL algorithm as the backbone, our solver incorporates the newest techniques for decision, deduction, diagnosis, and proof engines. Large efforts have been paid for tuning the parameters to achieve the best performance for all the benchmark suits. The experimental results shows that our SAT solver is at least competitive with state-of-art ones and superior to them for some benchmark suits. With the great flexibility on the circuit structure, our solver can serve as a solid foundation for the general SAT research in the future.
Functional dependency is concerned with rewriting a Boolean function f as a function h over a set of base functions {g1, …, gn}, i.e. f = h(g1, …, gn). It plays an important role in many aspects of electronics design automation (EDA), ranging from logic synthesis to formal verification. Prior approaches to the exploration of functional dependency are based on binary decision diagrams (BDDs), which may not be easily scalable to large designs. This second part of the thesis proposes a novel reformulation that extensively exploits the capability of modern satisfiability (SAT) solvers. Thereby, functional dependency is detected effectively through incremental SAT solving and the dependency function h, if exists, is obtained through Craig interpolation. The main strengths of the proposed approach include: (1) fast detection of functional dependency with small memory consumption and thus scalable to large designs, (2) a full capacity to handle a large set of base functions and thus discovering dependency whenever exists, and (3) potential application to large-scale logic optimization with different design constraints. Experimental results show the proposed method is far superior to prior work and scales well in dealing with the largest ISCAS89 and ITC99 benchmark circuits with up to 200K gates.
Subjects
滿足性問題
驗證邊界
矛盾證明
函數性依賴
克瑞格內插法
Boolean Satisfiability
Circuit Information
Justification Frontier
Refutation Proof
Functional Dependency
Craig Interpolation
Type
thesis
File(s)![Thumbnail Image]()
Loading...
Name
ntu-96-R94943077-1.pdf
Size
23.31 KB
Format
Adobe PDF
Checksum
(MD5):b8c1df1a5be01aa2db15f5ce7df24a8f