可滿足性問題(即SAT問題)是當(dāng)代理論計(jì)算機(jī)科學(xué)的重要研究方向之一,也是第一個被證明的NP完全問題,SAT問題的求解有助于解決其他NP問題。其快速求解算法不僅具有重要的理論意義,也具有重要的實(shí)際價值。SAT問題廣泛應(yīng)用于社會生產(chǎn)和人類生活中的各個領(lǐng)域,如人工智能、自動推理、軟件自動驗(yàn)證等。因此,設(shè)計(jì)并實(shí)現(xiàn)求解SAT問題的高效算法具有重要研究意義。目前,求解SAT問題的算法主要分為完備算法和不完備算法兩類。不完備算法主要是基于隨機(jī)搜索策略的局部搜索算法。完備算法主要基于1962年由Martin Davis,Hilary Putnam,George Logemann和Donald W.Loveland提出的DPLL算法,現(xiàn)在大多數(shù)完備算法都是基于DPLL算法發(fā)展而來,包括現(xiàn)在主流的CDCL算法。隨著社會科學(xué)的進(jìn)步,許多基于CDCL算法的求解器應(yīng)運(yùn)而生,用于解決日益復(fù)雜的大規(guī)模SAT問題,如z Chaff、Mini SAT、Glucose、Lingeling、PicoSAT等。本文基于CDCL算法結(jié)構(gòu),做了如下幾個方面的研究工作:1.根據(jù)變量決策層和沖突次數(shù),引入了分支決策階段變量得分的增量函數(shù),用于動態(tài)衡量不同搜索階段下變量的得分,在此基礎(chǔ)上,提出了基于變量決策層的分支策略(DLBH),為分支決策提供依據(jù),引導(dǎo)求解器搜索過程;2.根據(jù)學(xué)習(xí)子句中不同變量的決策層,引入了子句深度,用于評估求解過程中所產(chǎn)生學(xué)習(xí)子句的質(zhì)量,以刪除低質(zhì)量學(xué)習(xí)子句而保證高效率求解為目的,提出了基于子句深度的學(xué)習(xí)子句刪除策略(DBCD);3.分別將所提出的DLBH策略和DBCD策略形成相應(yīng)算法,嵌入到著名求解器Glucose3.0中,得到新的求解器glucose3.0+dlbh和glucose3.0+dbcd;將DLBH策略和DBCD策略對應(yīng)的算法同時嵌入到著名求解器Glucose3.0中,得到新的求解器glucose3.0+dlbh+dbcd。選擇2015年和2017年SAT國際競賽中的問題進(jìn)行測試,從測試結(jié)果在成功求解個數(shù)、平均決策次數(shù)、平均沖突次數(shù)、平均重啟次數(shù)、平均用時等多項(xiàng)指標(biāo)進(jìn)行對比分析,顯現(xiàn)出了新的求解器的有效性及優(yōu)勢。
【學(xué)位單位】：西南交通大學(xué)
【學(xué)位級別】：碩士
【學(xué)位年份】：2018
【中圖分類】：TP301.6
【部分圖文】：

圖中的每一個點(diǎn)代表一個測試?yán)挥谟蚁路降狞c(diǎn)代表求解器的性能高于位于左上方的點(diǎn)。從圖5.1 可以看出，求解器 glucose3.0+dlbh、glucose3.0+dbcd 及 glucose3.0+dlbh+dbcd 在性

【參考文獻(xiàn)】

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

1 郭瑩;張長勝;張斌;;一種求解SAT問題的人工蜂群算法[J];東北大學(xué)學(xué)報(bào)(自然科學(xué)版);2014年01期

2 劉歆;顏萍;;用布爾可滿足性驗(yàn)證邏輯電路的等價性[J];湖北工業(yè)大學(xué)學(xué)報(bào);2007年02期

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

1 丁志宇;應(yīng)用線性代數(shù)求解可滿足性問題的研究與實(shí)現(xiàn)[D];中山大學(xué);2014年

本文編號：2812429