- 學位論文
利用機器學習分析運算數據以預測布林可滿足性問題之演算效率
Predict the Performance of SAT Algorithm by Analyzing the Runtime Data with Machine Learning Techniques
摘要
布林可滿足性問題(SAT)是NP-complete問題中最被廣泛研究的問題之一。作為一個基本的運算及驗證單元，布林可滿足性問題解法器在電子設計自動化的領域中被頻繁且廣泛的使用。以現行的演算法來說，即使是相同規模的輸入資料，所需要的運算時間還是會有很大的不同。 在這篇論文中，我們提出了一套方法用來預測解法器所需要的運算時間。我們的預測是透過分析輸入的資料以及解法器在運算過程中的運算資料，再透過機器學習的方法經由類神經網路的模型作出預測。除了運算時間，我們也可以針對輸入資料預測出最適合該測資的解法器參數。所有的預測都可以在解法器的運行期間同時進行。 實驗數據顯示，我們的方法在各種布林可滿足性問題中的可以做出準確的預測。不僅如此，我們的預測模型還具備可擴充性，預測單一種類的輸入資料時，給與更針對性的分析資訊可以有效提昇預測的準確率。
並列摘要
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.