高斯消去法在布林可滿足性問題和克雷格內插法的探討

布林可滿足性問題(SAT)是在計算機科學領域中，理論與實際應用的核心問題之一。在計算理論上，SAT問題是第一個證明為NP完備問題。而在實際應用中，許多各種應用計算問題，例如軟硬體驗證、電子設計自動化、人工智慧、電路設計、定理機器證明等，能自然且精簡的編碼成SAT形式並利用當今解SAT問題的求解器快速求解。雖然幾年研究下來，SAT求解器速度大幅改善許多，然而許多研究仍顯示SAT求解器無法處理問題本質上有大量互斥或限制(XOR constraints)。雖然近幾年來如何加速解SAT問題中有大量互斥或限制受到許多關注，但仍有許多挑戰需要被克服。首先，如何得到完備的互斥或限制演繹去偵測邏輯蘊涵(implications)及衝突 (conflicts)。再者，如何有效降低互斥或限制演繹的計算時間。最後，如何直接得到簡潔的克雷格內插法(Craig interpolants)結合互斥或限制和合取範式(CNF)。在本篇論文中，我們發展出新的SAT求解器解決上述的三個挑戰。在我們求解器中，我們發展出單純形法(simplex method)風格的高斯-喬登消去法(Gauss-Jordan Elimination)演繹互斥或限制，並提出新的誘導規則可以直接得到簡潔的克雷格內插法。實驗結果顯示我們的方法可以有效加速求解時間，而且可以直接得到簡潔的克雷格內插法，是其他SAT求解器所不能獲得的。

關鍵字

布林可滿足性問題；克雷格內插法；高斯消去法；互斥或處理；互斥或限制

並列摘要

The Boolean satisfiability problem (SAT) is one of the central problems in computer science of both theoretical and practical interests. SAT is the first discovered NP-complete problem, and many real-world computation problems, such as hardware and software verification, electronic design automation (EDA), artificial intelligence (AI), circuit design, automatic theorem proving, etc., can be naturally encoded as SAT instances and solved efficiently. Although impressive advancements of SAT solving have been achieved, recent research reveals modern solvers' inability to handle formulae in the abundance of parity xor constraints. Although xor-handling in SAT solving has attracted much attention, challenges remain to completely deduce xor-inferred implications and conflicts, to effectively reduce expensive overhead, and to directly generate compact interpolants. This thesis presents a new SAT solver, SimpSat, which integrates SAT solving tightly with Gaussian elimination in the style of Dantzig's simplex method. It yields a powerful tool overcoming these challenges. Experiments show promising performance improvements and efficient derivation of compact interpolants, which are otherwise unobtainable.

並列關鍵字

Boolean satisfiability ； Craig interpolation ； Gaussian elimination ； xor-handling ； xor constraints

參考文獻

[2] A. Biere, M. Heule, H. van Maaren, and T. Walsh (editors). Handbook of Satisfiability, IOS Press, 2009.

[5] A. Cimatti, A. Griggio, and R. Sebastiani. Efficient generation of Craig interpolants in satisfiability modulo theories. ACM Trans. on Computational Logic, 12(1): 7, 2010.

[6] J.-C. Chen. XORSAT: An efficient algorithm for the DIMACS 32-bit parity problem. CoRR abs/cs/0703006, 2007.

[7] J.-C. Chen. Building a hybrid SAT solver via conflict-driven, look-ahead and XOR reasoning techniques. In Proc. Int’l Conf. on Theory and Applications of Satisfiability Testing (SAT), pages 298-311, 2009.

[8] S.A. Cook, The Complexity of Theorem Proving Procedures. In Proc. of 3rd ACM Sympoium on Theory of Computing, page 151-158, 1971.

國際替代計量

高斯消去法在布林可滿足性問題和克雷格內插法的探討

全文下載

主題瀏覽