請用此 Handle URI 來引用此文件:
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/40149
標題: | 運用虛擬布林最佳化工具解決可滿足性問題 Solving SAT Problem by Pseudo-Boolean Optimization Engine |
作者: | Chi-Cheng Hu 胡啟政 |
指導教授: | 黃鐘揚(Chung-Yang Huang) |
關鍵字: | 可滿足性問題,虛擬布林最佳化,連結正規式子句分割, SAT,Pseudo-Boolean optimization problem,Clause partitioning, |
出版年 : | 2008 |
學位: | 碩士 |
摘要: | 可滿足性(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. |
URI: | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/40149 |
全文授權: | 有償授權 |
顯示於系所單位: | 電子工程學研究所 |
文件中的檔案:
檔案 | 大小 | 格式 | |
---|---|---|---|
ntu-97-1.pdf 目前未授權公開取用 | 709.27 kB | Adobe PDF |
系統中的文件,除了特別指名其著作權條款之外,均受到著作權保護,並且保留所有的權利。