請用此 Handle URI 來引用此文件：
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/74077完整後設資料紀錄
| DC 欄位 | 值 | 語言 |
|---|---|---|
| dc.contributor.advisor | 黃鐘揚(Chung-Yang Huang) | |
| dc.contributor.author | Jia-Shiuan Chen | en |
| dc.contributor.author | 陳家暄 | zh_TW |
| dc.date.accessioned | 2021-06-17T08:19:03Z | - |
| dc.date.available | 2019-08-18 | |
| dc.date.copyright | 2019-08-18 | |
| dc.date.issued | 2019 | |
| dc.date.submitted | 2019-08-14 | |
| dc.identifier.citation | [1] S. A. Cook, “The complexity of theorem-proving procedures,” in Proceedings of the third annual ACM symposium on Theory of computing, pp. 151–158, ACM, 1971.
[2] M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, and S. Malik, “Chaff: Engineering an efficient sat solver,” in Proceedings of the 38th annual Design Automation Conference, pp. 530–535, ACM, 2001. [3] N. Eén and N. Sörensson, “An extensible sat-solver,” in International conference on theory and applications of satisfiability testing, pp. 502–518, Springer, 2003. [4] A. Biere, “CaDiCaL, Lingeling, Plingeling, Treengeling, YalSAT Entering the SAT Competition 2017,” in Proc. of SAT Competition 2017 – Solver and Benchmark Descriptions (T. Balyo, M. Heule, and M. Järvisalo, eds.), vol. B-2017-1 of Department of Computer Science Series of Publications B, pp. 14–15, University of Helsinki, 2017. [5] J. H. Liang, H. G. V. K., P. Poupart, K. Czarnecki, and V. Ganesh, “An empirical study of branching heuristics through the lens of global learning rate,” in Theory and Applications of Satisfiability Testing - SAT 2017 - 20th International Conference, Melbourne, VIC, Australia, August 28 - September 1, 2017, Proceedings, pp. 119–135, 2017. [6] B. Selman, D. G. Mitchell, and H. J. Levesque, “Generating hard satisfiability problems,” Artificial intelligence, vol. 81, no. 1-2, pp. 17–29, 1996. [7] E. Nudelman, K. Leyton-Brown, H. H. Hoos, A. Devkar, and Y. Shoham, “Understanding random sat: Beyond the clauses-to-variables ratio,” in International Conference on Principles and Practice of Constraint Programming, pp. 438–452, Springer, 2004. [8] F. Hutter, Y. Hamadi, H. H. Hoos, and K. Leyton-Brown, “Performance prediction and automated tuning of randomized and parametric algorithms,” in International Conference on Principles and Practice of Constraint Programming, pp. 213–228, Springer, 2006. [9] F. Hutter, L. Xu, H. H. Hoos, and K. Leyton-Brown, “Algorithm runtime prediction: Methods & evaluation,” Artificial Intelligence, vol. 206, pp. 79–111, 2014. [10] M. Davis, G. Logemann, and D. Loveland, “A machine program for theoremproving,” Communications of the ACM, vol. 5, no. 7, pp. 394–397, 1962. [11] J. P. Marques-Silva and K. A. Sakallah, “Grasp: A search algorithm for propositional satisfiability,” IEEE Transactions on Computers, vol. 48, no. 5, pp. 506–521, 1999. [12] N. Srivastava, G. Hinton, A. Krizhevsky, I. Sutskever, and R. Salakhutdinov, “Dropout: a simple way to prevent neural networks from overfitting,” The journal of machine learning research, vol. 15, no. 1, pp. 1929–1958, 2014. [13] DIMACS CNF file format. http://www.satcompetition.org/2009/format-benchmarks2009.html. [14] MiniSAT webpage. http://minisat.se/MiniSat.html. [15] SAT Competitions Benchmarks. http://www.satcompetition.org. | |
| dc.identifier.uri | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/74077 | - |
| dc.description.abstract | 布林可滿足性問題(SAT)是NP-complete問題中最被廣泛研究的問題之一。作為一個基本的運算及驗證單元，布林可滿足性問題解法器在電子設計自動化的領域中被頻繁且廣泛的使用。以現行的演算法來說，即使是相同規模的輸入資料，所需要的運算時間還是會有很大的不同。
在這篇論文中，我們提出了一套方法用來預測解法器所需要的運算時間。我們的預測是透過分析輸入的資料以及解法器在運算過程中的運算資料，再透過機器學習的方法經由類神經網路的模型作出預測。除了運算時間，我們也可以針對輸入資料預測出最適合該測資的解法器參數。所有的預測都可以在解法器的運行期間同時進行。 實驗數據顯示，我們的方法在各種布林可滿足性問題中的可以做出準確的預測。不僅如此，我們的預測模型還具備可擴充性，預測單一種類的輸入資料時，給與更針對性的分析資訊可以有效提昇預測的準確率。 | zh_TW |
| dc.description.abstract | Boolean satisfiability problem (SAT) is one of the most well-studied NP-Complete problems. SAT solvers are the fundamental engines that heavily used in many Electronic Design Automation (EDA) applications. As the characteristic of the NP-complete problem, SAT instances with similar sizes can still result in very different solving time.
In this thesis, we propose a machine learning approach which is based on neural network models to estimate the runtime of the given input. The predictions are made based on the analysis of the input CNF instance and the runtime data recorded from solvers. Our model can also provide recommended parameters for the solver to solve the given problem. All the analysis and predictions can be processed during the run time of the solving process. Experiments show that our model can make accurate predictions on general SAT instances. Moreover, it is also a base model which can be improved by using the domain knowledge when the inputs are restricted to a single type of SAT instances. The prediction accuracy will raise as the problem-specific features are taken into consideration. | en |
| dc.description.provenance | Made available in DSpace on 2021-06-17T08:19:03Z (GMT). No. of bitstreams: 1 ntu-108-R06921061-1.pdf: 2185769 bytes, checksum: 2ea49cc6a9fdf5b5dc42d24c8aa4a773 (MD5) Previous issue date: 2019 | en |
| dc.description.tableofcontents | 口試委員會審定書 i
誌謝 ii Acknowledgements iii 摘要 iv Abstract v 1 Introduction 1 1.1 Boolean Satisfiability Problem (SAT) 3 1.2 Machine Learning (ML) 3 1.3 Motivation 4 1.4 Related Work 5 1.5 Organizations of the Thesis 5 2 Preliminaries 6 2.1 Conjunctive Normal Form (CNF) 7 2.2 Algorithms for SAT problem 8 2.2.1 Davis-Putnam-Logemann-Loveland (DPLL) Algorithm 8 2.2.2 Conflict-Driven Clause Learning (CDCL) Algorithm 9 2.2.3 Other techniques 10 2.3 Random SAT Problem 11 2.4 Deep Learning (DL) 12 2.4.1 Gradient descent 12 2.4.2 Neural Network 13 3 Feature Selection 16 3.1 Basic Information 16 3.1.1 Variables and Clauses 16 3.1.2 Phase Ratio of Literals 18 3.2 Clause Length 20 3.3 Variable Distribution and Focal Clauses 23 3.4 Repetition Rate of Learnt Clauses 25 3.5 Efficiency Analysis of Decision Stack Restarting 28 3.5.1 Clause Length 29 3.5.2 Conflict Level 30 3.5.3 Similarity of clauses 31 3.6 Neighbor Counts of Variables 32 4 Model Construction 34 4.1 Data Preprocessing 34 4.2 NN Architectures 37 4.2.1 Output Form of Models 37 4.2.2 DNN 38 4.2.3 SNN 38 4.2.4 Other NNs 40 4.3 Machine Learning Techniques 43 4.3.1 Weights of Classes 43 4.3.2 Ensemble learning 43 4.4 Evaluation Metrics 44 5 Experimental Result 45 5.1 Time prediction 46 5.1.1 Performance of each Model 46 5.1.2 Abort dataset 48 5.1.3 Random 3-SAT dataset 48 5.1.4 Combining datasets 49 5.1.5 Dynamic features from different time period 50 5.1.6 Training on different features 50 5.2 Prediction on parameter tuning 52 5.2.1 Restart frequency 52 5.2.2 Reduce DB threshold 52 5.2.3 Case Study : SAT Competition 2018 53 6 Conclusion and Future work 54 6.1 Conclusion 54 6.2 Future work 55 Bibliography 56 | |
| dc.language.iso | en | |
| dc.subject | 布林可滿足性問題 | zh_TW |
| dc.subject | 機器學習 | zh_TW |
| dc.subject | 效率預測 | zh_TW |
| dc.subject | 執行時期分析 | zh_TW |
| dc.subject | 動態特徵 | zh_TW |
| dc.subject | Boolean Satisfiability Problem | en |
| dc.subject | Performance Prediction | en |
| dc.subject | Ma-chine Learning | en |
| dc.subject | Runtime analysis | en |
| dc.subject | Dynamic features | en |
| dc.title | 利用機器學習分析運算數據以預測布林可滿足性問題之演算效率 | zh_TW |
| dc.title | Predict the Performance of SAT Algorithm by Analyzing the Runtime Data with Machine Learning Techniques | en |
| dc.type | Thesis | |
| dc.date.schoolyear | 107-2 | |
| dc.description.degree | 碩士 | |
| dc.contributor.oralexamcommittee | 許智仁(Chih-Jen (Jacky),王柏堯 | |
| dc.subject.keyword | 布林可滿足性問題,機器學習,效率預測,執行時期分析,動態特徵, | zh_TW |
| dc.subject.keyword | Boolean Satisfiability Problem,Performance Prediction,Ma-chine Learning,Runtime analysis,Dynamic features, | en |
| dc.relation.page | 57 | |
| dc.identifier.doi | 10.6342/NTU201903472 | |
| dc.rights.note | 有償授權 | |
| dc.date.accepted | 2019-08-14 | |
| dc.contributor.author-college | 電機資訊學院 | zh_TW |
| dc.contributor.author-dept | 電機工程學研究所 | zh_TW |
| 顯示於系所單位： | 電機工程學系 | |
文件中的檔案：
| 檔案 | 大小 | 格式 | |
|---|---|---|---|
| ntu-108-1.pdf 未授權公開取用 | 2.13 MB | Adobe PDF |
系統中的文件，除了特別指名其著作權條款之外，均受到著作權保護，並且保留所有的權利。