運用虛擬布林最佳化工具解決可滿足性問題

可滿足性(SAT)問題為一著名問題，並被廣泛運用於電腦輔助積體電路設計領域；近幾年來，可滿足性解法器的重大進步幫助我們能夠更有效率地解決許多問題實例。本篇論文提出一種新的想法，將可滿足性問題轉換為虛擬布林(PB)最佳化問題，藉而運用虛擬布林工具解決。我們取代在連結正規式(CNF)裡部分子句中的部分變數，以這些分割變數減弱子句間連結性之限制；再利用被取代的變數必須與原變數同值之一致性，將子句間代表同一變數的變數值差異總和最小化視為目標，進行最佳化工作。為了要選取適當的分割變數，我們運用兩種方法實行子句的分割：一種以hMETIS軟體為工具，產生最小切割之二元分割；另一種則是根據變數及變數文字的出現次數，對各子句評估。實驗結果顯示，我們的方法對於部分實例表現出不錯的效果。

關鍵字

可滿足性問題；虛擬布林最佳化；連結正規式子句分割

並列摘要

Boolean satisfiability (SAT) problem is a well-known problem with many applications in the field of VLSI Computer-Aided Design. In recent years, dramatic improvements in SAT solver help us to solve instances more efficiently. In this thesis, we propose a novel idea to translate SAT problem into Pseudo-Boolean (PB) optimization problem and then solve by PB engine. Our approach produces a cut for the instance by breaking part of clause connectivity from some variables. We utilize the requirement of synchronizing same variables with identical assignment during the process, making sum of the difference in value between a cutting variable in different clauses as the optimization goal to be minimized. To pick appropriate variables, we apply two algorithms based on clause partitioning - one views CNF as hypergraph and uses hMETIS for min-cut bi-partitioning; another evaluates the clauses depending on literal and variable activity. The experimental results show that the PB optimization modeling technique performs well for a few instances.

並列關鍵字

SAT ； Pseudo-Boolean optimization problem ； Clause partitioning

參考文獻

[1] S. Cook, “The Complexity of Theorem Proving Procedures,” in Proc. ACM Symp. on the Theory of Computing, pp. 151-158, 1971.

[2] M. Davis, G. Logemann, D. Loveland, “A Machine Program for Theorem Proving,” in Communications of the ACM, pp. 394-497, 1962.

[3] J. P. Marques-Silva, K. A. Sakallah, “GRASP: A new search algorithm for satisfiability,” in International Conference on Computer-Aided Design, pp. 220–227, 1996.

[4] M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, S. Malik, “Chaff: Engineering an efficient SAT solver,” in Proc. DAC, pp. 530–535, 2001.

[6] G. Tseitin, “On the complexity of derivation in propositional calculus,” Studies in Constructive Mathematics and Mathematical Logic, 1968.

國際替代計量

運用虛擬布林最佳化工具解決可滿足性問題

全文下載

主題瀏覽