請用此 Handle URI 來引用此文件:
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/47983
標題: | 運用圖形同構於滿足性解法器之加速 Application of Graph Automorphism on Improving SAT Solver Performance |
作者: | Chun-Xun Lin 林春薰 |
指導教授: | 郭斯彥(Sy-Yen Kuo) |
關鍵字: | 布林可滿足性問題,圖形同構,滿足性解法器, Boolean satisfiability problem,graph automorphism,SAT solver, |
出版年 : | 2011 |
學位: | 碩士 |
摘要: | NP-complete 問題在各個層面應用極為廣泛,然而截至目前為止,
仍無法證明存在著多項式時間的演算法能在短時間內找出 NP-complete問題的最佳解。而在 NP-complete 問題中,布林可滿足性問題是第一個被證實是NP-complete,也是最被廣為研究的一類問題,布林可滿足性問題在現實應用於人工智慧、計算理論、正規驗證以及電子設計自動化相關領域中。 對於布林可滿足性問題,現有方法則以滿足性解法器為主,雖然滿足性解法器對於某些問題可以在有限時間內找出解答,但在複雜度上,仍為指數時間,也因此還有很多的難題尚無法求解。 在本論文中,實做了一套流程,透過先將布林問題轉化成圖形,利 用圖形同構演算法將各個變數之間的對稱性找出,因為對稱性質可以 刪除掉多餘的解空間,再將變數對稱轉換成布林表示式提供給滿足性 解法器加速其搜尋。由實驗結果可看出雖然圖形同構演算法必須花費 額外時間運算對稱,但對稱性大幅減短了解法器求解的時間,也使得 整體表現有著顯著提升。 NP-complete problems are often seen in different areas, but there is no proof showing NP equals P up to present and thus no polynomial time algorithms exist to give an optimal solution for NP-complete problems. Among all NP-complete problems, Boolean satisfiability is the first proven NP-complete problem and received widely study and found applications in artificial intelligence, computational theory, formal verification and electronic design automation(EDA) related areas.For Boolean satisfiability problem, SAT solver is the mainstream method, although many problems can be solved by SAT solver in reasonable time, but in terms of complexity, SAT solver still is of exponential time, so there are still lots of intractable problems. In this dissertation,a flow is implemented by transforming the Boolean satisfiability problem into a graph, and then using the graph automorphism algorithm to search for symmetries between variables. The symmetries found can prune the solution space, and finally a Boolean representation of symmetries is provided to SAT solver to accelerate its speed. The experimental results show that searching for symmetries requires additional time though,but the symmetries reduce the execution time of SAT solver substantially and therefore improve the whole performance. |
URI: | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/47983 |
全文授權: | 有償授權 |
顯示於系所單位: | 電子工程學研究所 |
文件中的檔案:
檔案 | 大小 | 格式 | |
---|---|---|---|
ntu-100-1.pdf 目前未授權公開取用 | 2.13 MB | Adobe PDF |
系統中的文件,除了特別指名其著作權條款之外,均受到著作權保護,並且保留所有的權利。