請用此 Handle URI 來引用此文件:
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/29775
完整後設資料紀錄
DC 欄位 | 值 | 語言 |
---|---|---|
dc.contributor.advisor | 黃鐘揚(Chu) | |
dc.contributor.author | Chih-Chun Lee | en |
dc.contributor.author | 李智群 | zh_TW |
dc.date.accessioned | 2021-06-13T01:18:21Z | - |
dc.date.available | 2007-10-22 | |
dc.date.copyright | 2007-07-20 | |
dc.date.issued | 2007 | |
dc.date.submitted | 2007-07-18 | |
dc.identifier.citation | [1] C.-A. Wu, T.-H. Lin, C.-C. Lee, C.-Y. Huang. “QuteSAT: A Robust Circuit-based SAT Solver for Complex Circuit Structure”. In Design Automation and Test in Europe (DATE) Conference, pp.1313-1319, 2007.
[2] C.-C. Lee, J.-H. R. Jiang, C.-Y. Huang, and A. Mishchenko. 'Scalable Exploration of Functional Dependency by Interpolation and Incremental SAT Solving'. In Proc. International Workshop of Logic Synthesis (IWLS), 2007 [3] S. A. Cook. “The Complexity of Theorem Proving Procedures”. In Proc. Third Annual ACM Symposium on the Theory of Computing, pp. 151-158, 1971 [4] S. H. Gerez. “Algorithms for VLSI Design Automation”. John Wiley & Sons, 1999. [5] E. M. Clarke, O. Grumberg, D. A. Peled. “Model Checking”. MIT Press, 1999. [6] S. Russell and P. Norvig. “Artificial Intelligence: A Modern Approach 2nd Edition”. Prentice Hall, 2003. [7] J. Gallier. “Logic for Computer Science: Foundations of Automatic Theorem Proving”. Wiley, 1986. [8] M. Davis, G.Longemann, D. Loveland. “A Machine Program for Theorem Proving”. In Communications of ACM (CACM), pp. 394-397, 1962. [9] G. Tseitin. “On the complexity of derivation in propositional calculus”. In Studies in Constr. Math. and Math. Logic, 1968. [10] M. Abramovici, M. Breuer, and A. Friedman. “Digital Systems Testing and Testable Design”, Chapters 3,5, and 6, W.H.Freeman, 1990. [11] F. Lu, L.-C. Wang, K.-T. Cheng, and C.-Y. Huang. 'A Circuit SAT Solver with Signal correlation Guided Learning'. In Design Automation and Test in Europe, pp. 892-897, 2003. [12] S.-Y. Huang, K.-T. Cheng, K.-C. Chen, C.-Y. R. Huang, and F. Brewer. “AQUILA: An Equivalence Checking System for Large Sequential Designs”. In IEEE Transactions on Computers, pp. 443-464, 2000. [13] L. Zhang and S. Malik. “Validating SAT Solvers Using an Independent Resolution-Based Checker: Practical Implementations and Other Applications”. In Design Automation and Test in Europe, pp. 880-885, 2003. [14] J. Huang. “MUP: A Minimal Unsatisfiability Prover”. In ASP-DAC, pp. 432-437, 2005. [15] K. L. McMillan. Interpolation and SAT-based model checking. In Proc. CAV, pp. 1-13, 2003. [16] J.-H. R. Jiang and R. K. Brayton. Functional dependency for verification reduction. In Proc. CAV, pp. 268-280, 2004. [17] E. Sentovich, H. Toma, and G. Berry. Latch optimization in circuits generated from high-level descriptions. In Proc. ICCAD, pp. 428-435, 1996. [18] B. Lin and A. R. Newton. Exact redundant state registers removal based on binary decision diagrams. In Proc. Int'l Conf. Very Large Scale Integration, pp. 277-286, 1991. [19] V. Kravets and P. Kudva. Implicit enumeration of structural changes in circuit optimization. In Proc. DAC, pp. 438-441, 2004. [20] A. J. Hu and D. L. Dill. Reducing BDD size by exploiting functional dependencies. In Proc. DAC, pp. 266-271, 1993. [21] C. Berthet, O. Coudert, and J.-C. Madre. New ideas on symbolic manipulations of finite state machines. In Proc. ICCD, pp. 224-227, 1990. [22] C. A. J. van Eijk and J. A. G. Jess. Exploiting functional dependencies in finite state machine verification. In Proc. European Design & Test Conf., pp. 9-14, 1996. [23] E. Gregoire, R. Ostrowski, B. Mazure, and L. Sais. Automatic extraction of functional dependencies. In Proc. SAT, 2004. [24] R. E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Trans. Computers, pp. 677--691, August 1986. [25] M. Moskewicz, C. Madigan, L. Zhang, and S. Malik. Chaff: Engineering an efficient SAT solver. In Proc. DAC, pp. 530-535, 2001. [26] N. Een and N. Sorensson. An extensible SAT-solver. In Proc. SAT, pp. 502-518, 2003. [27] A. Mishchenko and R. Brayton. SAT-based complete don't-care computation for network optimization. In Proc. DATE, pp. 418-423, 2005. [28] A. Mishchenko, J. Zhang, S. Sinha, J. Burch, R.K. Brayton, and M. Chrzanowska-Jeske. Using simulation and satisfiability to compute flexibilities in Boolean networks. IEEE Trans. on CAD, vol. 25, no. 5, pp. 742-755, 2006. [29] W. Craig. Linear reasoning: A new form of the Herbrand-Gentzen theorem. J. Symbolic Logic, 22(3):250-268, 1957. [30] J. Huang, A. Darwiche. “A Structure Based Variable Ordering Heuristic for SAT”. In Proceedings of IJCAI, 2003. [31] V. Durairaj, P. Kalla. “Variable Ordering for Efficient SAT Search by Analyzing Constraint-Variable Dependencies”. In SAT, 2005. [32] F. A. Aloul, I. L. Markov, K. A. Sakallah. “FORCE: A Fast and Easy-to-implement Variable Ordering Heuristic”. In Great Lakes Symposium on VLSI, pp 116-119, 2003. [33] E. Goldberg and Y. Novikov. “BerkMin: A Fast and Robust SAT Solver”. In Proceedings of Design Automation and Test in Europe Conference, pp. 142-149, 2002. [34] L. Ryan. “Efficient Algorithms for Clause-Learning SAT Solvers”. Mater Thesis, Simon Fraser University, 2004. [35] R. Gershman and O. Strichman. “A Decision Heuristic Based on an Abstraction/ Refinement Model”. In IBM Verification Conference, 2005. [36] J. P. Marques-Silva, K. A. Sakalla. “GRASP: A New Search Algorithm for Satisfiability”. In Proceedings of International Conference on Computer-Aided Design, pp. 220-227, 1996. [37] O. Coudert. “On Solving Covering Problems”. In Proc. of Design Automation Conference, pp. 197-202, 1996. [38] H. Zhang. “SATO: An Efficient Propositional Prover”. In Proceedings of International Conference on Automated Deduction, pp. 272-275, 1997. [39] I. Lynce and J. P. Marques-Silva. “Efficient Data Structures for Backtrack Search SAT Solvers”. In Annual of Mathematics and Artificial Intelligence 47(1), pp. 137-152, 2005. [40] F. Bacchus and J. Winter. “Effective Preprocessing with Hyper-Resolution and Equality Reduction”. In Theory and Applications of Satisfiability Testing, volume 2919 of LNCS, pp. 341-355, 2003. [41] R. Gershman and O. Strichman. “Cost-Effective Hyper-Resolution for Pre- processing CNF Formulas”. In Theory and Applications of Satisfiability Testing, 2005. [42] R. J. Bayardo, R. C. Schrag. “Using CSP Look-Back Techniques to Solve Real-World SAT Instances”. In Proceedings of the 14th National Conference on Artificial Intelligence, pp. 203-208, 1997. [43] J. Huang. “The Effect of Restarts on the Efficiency of Clause Learning”. In Proceedings of 12th International Joint Conference on Artificial Intelligence, pp. 2318-2323, 2007. [44] M. Luby, A. Sinclair, and D. Zuckerman. “Optimal Speedup of Las Vegas Algorithms”. In Information Processing Letters 47, pp. 173-180, 1993. [45] A. Mishchenko. “ABC: A System for Sequential Synthesis and Verification”. http://www.eecs.berkeley.edu/~alanmi/abc [46] R. K. Brayton, et al. “VIS: A System for Verification and Synthesis”. In Proc. CAV, pp. 428-432, 1996. [47] Y. Novikov and R. Brinkmann. “Foundations of Hierarchical SAT Solving”. In Proceedings of International Workshop on Boolean Problems, 2004. [48] R. Jhala and K. L. McMillan. “Interpolant-Based Transition Relation Approximation”. In Proc. CAV, pp. 39-51, 2005. [49] SAT-Race 2006. http://fmv.jku.at/sat-race-2006/ [50] M. Velve’s SAT benchmarks. http://www.miroslav-velev.com/sat_benchmarks.html [51] N. Een and N. Sorensson. Minisat-p_v1.14. http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/Main.html [52] Niklas Een, Armin Biere. “Effective Preprocessing in SAT through Variable and Clause Elimination”. In Theory and Applications of Satisfiability Testing, 2005. | |
dc.identifier.uri | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/29775 | - |
dc.description.abstract | 在本論文的第一部分,基於驗證邊界(Justification Frontiers),我們設計了擁有利用問題內含電路結構能力的電路可滿足性解法器。裝備驗證邊界技巧的演繹技術可以不需在電路上實作而以在句型上(Clauses)實作取代,同時還能夠保持完整的電路結構。以DPLL演算法為骨幹,我們的可滿足性解法器成功的包含了決定、演繹、診斷以及證明儲存引擎中最新的方法。我們也在解法器參數上下了很大的功夫去調整以達到整體的最佳效能。實驗結果顯示,我們的解法器至少可能夠目前世界上最佳的解法器披敵,甚至在某些例子上還遠勝於它們。在電路結構上的靈活性使得我們的可滿足性解法器能為未來研究廣義可解法性問題開拓道路。
函數性依賴(Functional Dependency)與於如何改寫布林函數f成為一個依賴於一組基底函數{g1, …, gn}的函數h使得f = h(g1, …, gn)的問題有緊密的關連性。函數性依賴在電子設計自動化領域中扮演了重要的角色,從邏輯合成到正規驗證都有其應用之處。先前探索函數性依賴的方法乃基於二元決策樹(BDDs)的使用,然而二元決策樹在處理大型電路設計的能力上卻不足夠。本論文的第二部分提出了一個嶄新的方法,此方法大量運用了現代可滿足性解法器(SAT Solvers)的優秀能力。經由此法以及微量可滿足性解法,函數性依賴的偵測問題能夠很有效率的被解決。若問題中的依賴性函數存在,我們接下來可使用克瑞格內插法(Craig Interpolation)進一步的得到此函數。我們所建議方法的優點如下:(1)僅需使用少量的記憶體即可有效率的解決函數性依賴的偵測問題,因而可以解決大型電路設計的問題;(2)對於處理大量基底函數擁有完整的能力,因而只要依賴性函數存在,我們必能得到它;(3)對於多種面向限制的大型邏輯優化問題擁有潛在性的應用。實驗結果顯示我們所提出的方法效能遠勝過先前的方法,而且對於最多可到二十萬邏輯閘的大型ITC以及ISCAS電路的處理能力表現上也相當的好。 | zh_TW |
dc.description.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. | en |
dc.description.provenance | Made available in DSpace on 2021-06-13T01:18:21Z (GMT). No. of bitstreams: 1 ntu-96-R94943077-1.pdf: 7608335 bytes, checksum: 2526e6913e539829b15720981334a241 (MD5) Previous issue date: 2007 | en |
dc.description.tableofcontents | 誌謝 壹
摘要 貳 Abstract i Table of Contents iii List of Tables vi List of Figures vii Chapter 1 Introduction 1 1.1 Circuit SAT Solver 1 1.1.1 Overview 1 1.1.2 Our Contributions 3 1.2 Functional Dependency 4 1.2.1 Overview 4 1.2.2 Our Contributions 5 1.3 Thesis Organization 6 Chapter 2 Preliminaries 7 2.1 Propositional Satisfiability 7 2.2 Refutation Proof 8 2.3 Interpolant 10 2.4 Functional Dependency 12 Chapter 3 Engineering a Circuit SAT Solver 14 3.1 DPLL-Styled Framework 14 3.2 Decision Engine 16 3.2.1 Variable State Independent Decaying Sum (VSIDS) 16 3.2.2 BerkMin 17 3.2.3 Variable-Move-To-Front (VMTF) 18 3.2.4 Clause-Move-To-Front (CMTF) 19 3.2.5 Justification Froniters 20 3.2.6 Putting Altogether 23 3.3 Deduction Engine 23 3.3.1 Head/Tail Structure 25 3.3.2 Two Literal Watching Scheme 25 3.3.3 Boundary Sentinels 26 3.3.4 Binary and Ternary Clauses 26 3.3.5 Putting Altogether 27 3.4 Diagnosis Engine 27 3.4.1 Conflict Analysis 29 3.4.2 Conflict Minimization 32 3.4.3 Restart Policy 33 3.4.4 Putting Altogether 34 3.5 Proof Recording Engine 35 3.5.1 On-Line Recording 36 3.6 Experimental Results 37 Chapter 4 Exploration of Functional Dependency 42 4.1 Derivation of Functional Dependency by BDD 42 4.2 Detection of Functional Dependency by SAT Solving 44 4.3 Recover Dependency Functions through Interpolants 46 4.4 Incremental SAT Solving 48 4.5 Enumeration of Functional Dependency 50 4.6 Experimental Results 52 Chapter 5 Conclusion and Future works 58 References 60 | |
dc.language.iso | en | |
dc.title | 在電路上實現可滿足性解法器以及其在函數相依性分析與矛盾抽取證明上之應用 | zh_TW |
dc.title | Engineering a Circuit-Based SAT Solver and Its Applications on Functional Dependency Analysis and Refutation Proof Extraction | en |
dc.type | Thesis | |
dc.date.schoolyear | 95-2 | |
dc.description.degree | 碩士 | |
dc.contributor.oralexamcommittee | 江介宏,王柏堯 | |
dc.subject.keyword | 滿足性問題,電路資訊,驗證邊界,矛盾證明,函數性依賴,克瑞格內插法, | zh_TW |
dc.subject.keyword | Boolean Satisfiability,Circuit Information,Justification Frontier,Refutation Proof,Functional Dependency,Craig Interpolation, | en |
dc.relation.page | 64 | |
dc.rights.note | 有償授權 | |
dc.date.accepted | 2007-07-19 | |
dc.contributor.author-college | 電機資訊學院 | zh_TW |
dc.contributor.author-dept | 電子工程學研究所 | zh_TW |
顯示於系所單位: | 電子工程學研究所 |
文件中的檔案:
檔案 | 大小 | 格式 | |
---|---|---|---|
ntu-96-1.pdf 目前未授權公開取用 | 7.43 MB | Adobe PDF |
系統中的文件,除了特別指名其著作權條款之外,均受到著作權保護,並且保留所有的權利。