頁籤選單縮合
| 題 名 | A Study of Gaussian Elimination on Boolean Satisfiability and Craig Interpolation=高斯消去法在布林可滿足性問題和克雷格內插法的探討 |
|---|---|
| 作 者 | 韓承駪; 江介宏; | 書刊名 | 中華民國資訊學會通訊 |
| 卷 期 | 16:1 2013.03[民102.03] |
| 頁 次 | 頁115-129 |
| 分類號 | 471.6 |
| 關鍵詞 | 高斯消去法; 布林可滿足性問題; 克雷格內插法; SAT; |
| 語 文 | 英文(English) |
| 中文摘要 | 布林可滿足性問題(SAT)是在計算機科學領域中,理論與實際應用的核心問題之一。在計算理論上,SAT 問題是第一個證明為NP 完備問題。而在實際應用中,許多計算問題,例如軟硬體驗證、電子設計自動化、人工智慧、電路設計、定理機器證明等,能自然且精簡的編碼成合取範式(Conjunctive Normal Form, CNF)並利用SAT求解器快速求解。雖然SAT求解技術已非常成熟並廣泛應用於處理業界規模的問題,當今SAT求解器仍無法有效處理問題本質上有大量的奇偶限制式(parity or XOR constraint)。雖然近幾年來如何加速求解隱含大量奇偶限制式的CNF受到許多關注,但仍有以下問題需要被克服:首先,如何在奇偶限制式系統中完備且有效率的偵測邏輯蘊涵(implication)及衝突(conflicts)。再者,如何在奇偶式與合取範式混合的限制式求得簡潔的克雷格內插子(Craig interpolant)。本論文發展新的SAT 求解器解決上述挑戰。我們提出單純形法(simplex method)風格的高斯-喬登消去法(Gauss-Jordan Elimination)來有效處理奇偶限制式,並提出新的推導規則獲得簡潔的克雷格內插子。實驗結果顯示我們的方法可以有效加速求解時間,並可直接得到簡潔的克雷格內插子,是其他SAT 求解器所不能獲得的。 |
本系統中英文摘要資訊取自各篇刊載內容。