本文關(guān)鍵詞： SAT問題 分支變量 啟發(fā)式算法 變量活性 獎(jiǎng)勵(lì)函數(shù)　出處：《西南交通大學(xué)》2017年碩士論文　論文類型：學(xué)位論文

【摘要】：命題邏輯公式的可滿足性問題(即SAT問題)是人工智能和計(jì)算機(jī)科學(xué)領(lǐng)域的核心問題之一。1971年Stephen.Cook從算法時(shí)間復(fù)雜度的角度證明了 SAT問題是NP完全問題,而NP完全問題在七大數(shù)學(xué)難題中排在首位,可見SAT問題是一類非常困難的問題。由于SAT問題在約束可滿足問題、數(shù)理邏輯、自動(dòng)推理、軟件及硬件驗(yàn)證等領(lǐng)域具有廣泛的應(yīng)用,因此研究SAT問題的求解具有重要的理論價(jià)值和應(yīng)用前景。目前求解SAT問題的算法大致可歸為兩類:一類是完備的求解算法;一類是不完備的求解算法�；贒PLL算法的CDCL(Conflict Derive Clause Learning)算法是目前比較流行的完備算法,由該算法設(shè)計(jì)的求解器(CDCLSAT求解器)的求解過程主要分為三大階段,分別是分支變量選擇階段、布爾約束傳播階段和沖突分析及回溯階段。其中,變量選擇階段的分支變量啟發(fā)式算法可歸結(jié)為兩類:第一類是沒有與沖突分析過程相結(jié)合的啟發(fā)式算法,比如JW算法(Jeroslow-Wang)、DLIS(Dynamic Larger Independent Sum)算法等;第二類是與沖突分析過程相結(jié)合的啟發(fā)式算法,比如VSIDS(Variable State Independent Decaying Sum)算法、CHB(Conflict History-based Branching Heuristic)算法、LRB(Learning Rate Branching)算法等。由于第一類分支變量啟發(fā)式算法計(jì)算代價(jià)大,第二類分支變量啟發(fā)式算法未能很好地利用子句固有的信息以及未體現(xiàn)出學(xué)習(xí)子句中變量的不同。故為了盡可能減少這些算法的不足以及選出更好的分支變量,本文以經(jīng)典的VSIDS算法為基本框架設(shè)計(jì)了基于獎(jiǎng)勵(lì)的分支變量啟發(fā)式算法,并用該算法代替MiniSat求解器中的分支變量啟發(fā)式算法,得到新的求解器一Modified-MiniSat 求解器。本文就新算法的提出主要做了以下四方面的工作:1.對(duì)于一般的SAT問題,短子句較長(zhǎng)子句更難被滿足,依據(jù)子句的長(zhǎng)度賦予每個(gè)子句權(quán)重,進(jìn)而給出變量在子句以及子句集中的權(quán)重的定義。并用變量在子句集中的權(quán)重刻畫變量的活性,從而盡可能準(zhǔn)確地反映變量在子句集中的活躍度。2.設(shè)計(jì)了與決策層有關(guān)的獎(jiǎng)勵(lì)函數(shù)。在問題求解過程中,當(dāng)學(xué)習(xí)子句添加到子句集時(shí),根據(jù)學(xué)習(xí)子句中變量所在決策層的不同,獎(jiǎng)勵(lì)變量,以便增大學(xué)習(xí)子句中的變量活性。3.基于上述兩方面的工作,給出了基于獎(jiǎng)勵(lì)的分支變量啟發(fā)式算法,并用該算法代替MiniSat求解器中的分支變量啟發(fā)式算法,設(shè)計(jì)了相應(yīng)的求解器-Modified-MiniSat求解器。4.選擇2013 SAT競(jìng)賽以及2016年SAT競(jìng)賽例作為測(cè)試?yán)?對(duì)Modified-MiniSat求解器和MiniSat求解器做對(duì)比測(cè)試,通過分析實(shí)驗(yàn)結(jié)果得知Modified-MiniSat求解器有一定的優(yōu)勢(shì),從而說明了改進(jìn)后的分支變量啟發(fā)式算法的有效性。
[Abstract]:The satisfiability problem of propositional logic formula (SAT problem) is one of the core problems in the field of artificial intelligence and computer science. In 1971, Stephen.Cook proved that the SAT problem is NP-complete problem from the angle of algorithm time complexity. The NP-complete problem ranks first among the seven mathematical problems. It can be seen that the SAT problem is a kind of very difficult problem. Because the SAT problem has a wide range of applications in the fields of constrained satisfiability problem, mathematical logic, automatic reasoning, software and hardware verification, etc. Therefore, it has important theoretical value and application prospect to study the solution of SAT problem. At present, the algorithms for solving SAT problem can be classified into two categories: one is complete algorithm; One is incomplete algorithm. The CDCL(Conflict Derive Clause learning algorithm based on DPLL algorithm is a popular complete algorithm. The solver designed by this algorithm is divided into three stages. They are branch variable selection, Boolean constraint propagation and conflict analysis and backtracking. In the stage of variable selection, the branch variable heuristic algorithm can be divided into two categories: the first is a heuristic algorithm that does not combine with the conflict analysis process, such as the JW algorithm Jeros low-Wangli dynamic Larger Independent Sumet, etc. The second is the heuristic algorithm combined with the conflict analysis process, such as VSIDS(Variable State Independent Decaying summing (VSIDS(Variable State Independent Decaying summing) algorithm and so on. The second kind of heuristic algorithm of branch variable can not make good use of the inherent information of clause and the difference of variable in learning clause, so in order to minimize the deficiency of these algorithms and select better branch variable, In this paper, the classical VSIDS algorithm is used as the basic framework to design a heuristic algorithm for branching variables based on rewards, and the algorithm is used to replace the branch variable heuristic algorithm in the MiniSat solver. A new solver, Modified-MiniSat solver, is obtained. In this paper, the following four aspects of the proposed algorithm are mainly done: 1. For a general SAT problem, the short clause is more difficult to satisfy than the long clause, and each clause is given weight according to the length of the clause. Then the definition of the weight of variable in clause and clause set is given, and the activity of variable in clause set is characterized by the weight of variable in clause set. The reward function related to the decision level is designed. In the process of solving the problem, when the learning clause is added to the clause set, the variable in the learning clause is different from the decision layer in the learning clause. Reward variables in order to increase the activity of variables in the learning clause. 3. Based on the above two aspects of work, a heuristic algorithm of branch variables based on reward is presented, and the heuristic algorithm of branch variables in MiniSat solver is replaced by the heuristic algorithm. The corresponding solver -Modified-MiniSat solver .4.Selects the 2013 SAT contest and the 2016 SAT contest as test examples, and makes a comparative test of Modified-MiniSat solver and MiniSat solver. Through the analysis of the experimental results, it is found that Modified-MiniSat solver has some advantages. Thus, the effectiveness of the improved heuristic algorithm for branch variables is demonstrated.
【學(xué)位授予單位】：西南交通大學(xué)
【學(xué)位級(jí)別】：碩士
【學(xué)位授予年份】：2017
【分類號(hào)】：O141

【相似文獻(xiàn)】

相關(guān)期刊論文 前10條

1 李詩(shī)珍;;配送中心訂單分批揀貨模型及種籽啟發(fā)式算法[J];起重運(yùn)輸機(jī)械;2009年01期

2 王慶貞;趙雁;鐘斌;王玉龍;;車輛優(yōu)化調(diào)度算法研究初探[J];黑龍江科技信息;2010年03期

3 王樂善;_5良震;;求圖的總體最佳2—?jiǎng)澐值挠行l(fā)式算法[J];安徽大學(xué)學(xué)報(bào)(自然科學(xué)版);1983年02期

4 徐亦文;運(yùn)輸路徑問題的一個(gè)新啟發(fā)式算法[J];上海機(jī)械學(xué)院學(xué)報(bào);1987年02期

5 郭耀煌,范莉莉;貨運(yùn)汽車調(diào)度的一種啟發(fā)式算法[J];系統(tǒng)工程;1989年01期

6 陳駐民;羊英;;混流企業(yè)中基于瓶頸的啟發(fā)式算法的應(yīng)用[J];武漢理工大學(xué)學(xué)報(bào)(信息與管理工程版);2010年02期

7 鄭攀;胡思繼;張晨;;機(jī)門指派模型建立與啟發(fā)式算法設(shè)計(jì)[J];系統(tǒng)工程學(xué)報(bào);2011年01期

8 馬磊;任成磊;韓定定;;模塊度優(yōu)化啟發(fā)式算法應(yīng)用[J];現(xiàn)代電子技術(shù);2012年19期

9 黃干平,劉娟;解“時(shí)間表問題”的啟發(fā)式算法[J];武漢大學(xué)學(xué)報(bào)(自然科學(xué)版);1996年01期

10 趙赫,杜端甫;TSP的鄰域搜索算法的分析和改進(jìn)[J];中國(guó)管理科學(xué);1997年01期

相關(guān)會(huì)議論文 前10條

1 羅守成;唐國(guó)春;;二維集裝箱問題的一個(gè)啟發(fā)式算法[A];2001年全國(guó)數(shù)學(xué)規(guī)劃及運(yùn)籌研討會(huì)論文集[C];2001年

2 劉青松;孔云峰;黨蘭學(xué);王震;;元啟發(fā)式算法在校車路徑規(guī)劃中的應(yīng)用[A];第七屆全國(guó)地理學(xué)研究生學(xué)術(shù)年會(huì)論文摘要集[C];2012年

3 劉嘉敏;馬廣煜;黃有群;;基于組合的三維集裝箱裝入啟發(fā)式算法的研究[A];全國(guó)第13屆計(jì)算機(jī)輔助設(shè)計(jì)與圖形學(xué)（CAD/CG）學(xué)術(shù)會(huì)議論文集[C];2004年

4 何正文;徐渝;;多模式項(xiàng)目支付進(jìn)度問題的優(yōu)化模型及啟發(fā)式算法[A];中國(guó)運(yùn)籌學(xué)會(huì)第七屆學(xué)術(shù)交流會(huì)論文集（上卷）[C];2004年

5 趙文丹;汪定偉;郭小萍;王貴成;;網(wǎng)絡(luò)廣告資源優(yōu)化問題研究[A];第二十九屆中國(guó)控制會(huì)議論文集[C];2010年

6 楊士準(zhǔn);謝政;陳摯;熊李軍;;k約束QoS問題的啟發(fā)式算法[A];中國(guó)通信學(xué)會(huì)第六屆學(xué)術(shù)年會(huì)論文集（下）[C];2009年

7 劉金朋;魏長(zhǎng)江;;啟發(fā)式算法求最短路徑的一種高效率實(shí)現(xiàn)方法[A];2007北京地區(qū)高校研究生學(xué)術(shù)交流會(huì)通信與信息技術(shù)會(huì)議論文集（上冊(cè)）[C];2008年

8 范敏;鄒平;朱興東;;一種啟發(fā)式離散化算法及其Delphi實(shí)現(xiàn)[A];第二屆中國(guó)智能計(jì)算大會(huì)論文集[C];2008年

9 王文瀚;杜斌;朱俊;賈樹晉;;集成MILP與啟發(fā)式的混合算法求解板坯設(shè)計(jì)問題[A];中國(guó)計(jì)量協(xié)會(huì)冶金分會(huì)2012年會(huì)暨能源計(jì)量與節(jié)能降耗經(jīng)驗(yàn)交流會(huì)論文集[C];2012年

10 馮德鴻;唐加福;郭琦;李輝;;訂貨批量問題改進(jìn)的相關(guān)策略啟發(fā)式算法與仿真分析[A];2007系統(tǒng)仿真技術(shù)及其應(yīng)用學(xué)術(shù)會(huì)議論文集[C];2007年

相關(guān)博士學(xué)位論文 前9條

1 李福清;交通規(guī)劃中專用道設(shè)置問題建模和求解研究[D];廣東工業(yè)大學(xué);2016年

2 賴向京;原子團(tuán)簇結(jié)構(gòu)預(yù)測(cè)的現(xiàn)實(shí)途徑—高性能啟發(fā)式算法[D];華中科技大學(xué);2012年

3 黎展滔;具有成組約束的柔性流水車間作業(yè)計(jì)劃制定的啟發(fā)式算法[D];廣東工業(yè)大學(xué);2012年

4 曹斌;生物啟發(fā)式智能計(jì)算及其應(yīng)用的研究[D];吉林大學(xué);2012年

5 董興業(yè);啟發(fā)式算法及其在同順序流水作業(yè)問題中的應(yīng)用[D];北京交通大學(xué);2008年

6 古繼興;KOD多播技術(shù)與Steiner樹啟發(fā)式算法[D];上海交通大學(xué);2007年

7 胡大偉;設(shè)施定位和車輛路線問題模型及其啟發(fā)式算法研究[D];長(zhǎng)安大學(xué);2008年

8 楊玉珍;基于元啟發(fā)式算法的帶生產(chǎn)約束作業(yè)車間調(diào)度問題若干研究[D];華東理工大學(xué);2014年

9 任志磊;組合優(yōu)化問題的特化與泛化算法設(shè)計(jì)[D];大連理工大學(xué);2013年

相關(guān)碩士學(xué)位論文 前10條

1 朱璽睿;氯氧鎂板材生產(chǎn)線優(yōu)化研究[D];東北林業(yè)大學(xué);2015年

2 尹青山;綠色微數(shù)據(jù)中心與NGPON融合網(wǎng)絡(luò)部署規(guī)劃研究[D];大連海事大學(xué);2015年

3 石闖;基于啟發(fā)式算法的Ad Hoc網(wǎng)絡(luò)QoS路由協(xié)議的研究與仿真[D];東北大學(xué);2013年

4 劉暢;基于混合啟發(fā)式算法的單線公交車輛調(diào)度問題研究[D];北京交通大學(xué);2016年

5 張毅;啟發(fā)式算法的自調(diào)參數(shù)方法研究[D];西安工程大學(xué);2016年

6 周書橙;護(hù)士排班的啟發(fā)式算法研究與排班管理系統(tǒng)的設(shè)計(jì)實(shí)現(xiàn)[D];北京交通大學(xué);2016年

7 任平飛;基于啟發(fā)式算法的云計(jì)算負(fù)載均衡問題研究[D];哈爾濱工業(yè)大學(xué);2016年

8 戈麗娜（Galina Deeva）;配送過程中提貨送貨問題的靜態(tài)動(dòng)態(tài)方法的應(yīng)用效果研究[D];哈爾濱工業(yè)大學(xué);2016年

9 劉賽賽;基于增強(qiáng)學(xué)習(xí)的啟發(fā)式和元啟發(fā)式搜索的參數(shù)調(diào)優(yōu)策略[D];電子科技大學(xué);2016年

10 李鵬;定制衣柜零件分揀方式及效能分析[D];南京林業(yè)大學(xué);2016年

，

本文編號(hào)：1502336