關(guān)于布爾可滿足性判定的新方法研究
發(fā)布時(shí)間：2021-01-27 06:54
布爾可滿足性（Boolean Satisfiability,SAT）問題是指,給定一組布爾變?cè)猉及由X構(gòu)成的CNF公式,問是否存在一組對(duì)X的賦值,使得公式為真。SAT問題是第一個(gè)被證明為NP完全的問題,在計(jì)算理論中具有重要地位。如果找到能夠在多項(xiàng)式時(shí)間求解SAT問題的完備方法,則P=NP;反之,如果能夠確定所有SAT算法的最壞時(shí)間復(fù)雜度下界為指數(shù)級(jí)別,則P≠NP。此外,SAT問題在電路驗(yàn)證、組合優(yōu)化、自動(dòng)推理等領(lǐng)域有重要的實(shí)踐意義。當(dāng)前,SAT問題的求解算法分為完備算法和不完備算法。完備算法總是能夠找到一個(gè)滿足公式的賦值,或者證明公式的不可滿足性�；贒PLL的搜索算法是目前主流的一類完備算法,這類算法用回溯的方法,對(duì)賦值空間進(jìn)行系統(tǒng)的搜索。在對(duì)DPLL算法的各種改進(jìn)中,CDCL算法利用子句學(xué)習(xí)和非逐字回溯大大減少了回溯次數(shù)。目前已知的完備算法最壞時(shí)間復(fù)雜度為指數(shù)級(jí)別。而不完備算法針對(duì)實(shí)際的SAT問題,提高了求解效率。其中,局部搜索算法廣泛應(yīng)用了概率和貪心的策略,只對(duì)賦值空間的一部分進(jìn)行搜索,提高了搜索效率。基于優(yōu)化的方法將SAT問題轉(zhuǎn)化為優(yōu)化問題,然后用拉格朗日法、牛頓法等方法解決。...
【文章來(lái)源】：中國(guó)科學(xué)院大學(xué)(中國(guó)科學(xué)院重慶綠色智能技術(shù)研究院)重慶市
【文章頁(yè)數(shù)】：79 頁(yè)
【學(xué)位級(jí)別】：碩士
【部分圖文】：
圖３．１?ＤＰＬＬ搜索樹圖示??元傳播化簡(jiǎn)的公式Ｊｅ
圖３．２蘊(yùn)含圖示例??
?關(guān)于布爾可滿足性判定的新方法研究???ｆ?０?Ｊ——?０⑴??，２＝１０＾０??，＝１?￡）??圖３．３?ＣＤＣＬ搜索樹圖示??（在第／ｅｖｅ／層）與其父節(jié)點(diǎn)的邊（在第／ｅｖｄ－１層）對(duì)應(yīng)的賦值，記Ｌｅｖｄ（Ｘｕ）?＝??／ｅｖｄ－１。另一種頂點(diǎn)是矛盾頂點(diǎn)，記為Ａ＾，由其他的頂點(diǎn)推出。蘊(yùn)含圖中，有??向邊的出發(fā)點(diǎn)是賦值（決策賦值或者蘊(yùn)含賦值），終點(diǎn)是蘊(yùn)含賦值或者矛盾。有??向邊用的標(biāo)記，表示代入這條邊出發(fā)點(diǎn)對(duì)應(yīng)的賦值后，Ｍ成為新的單元子句或??者空子句，用單元傳播推出終點(diǎn)對(duì)應(yīng)的蘊(yùn)含賦值或者矛盾。??仍然以〇＾公式７７＝｛０１，〇）２，，．，，叫｝為例，其中，〇；１?＝?｛＾＇１，＆｝，〇）２?＝??｛Ｘ２，Ｘ３｝，的＝卜＆，￣＾４，＾｝’?叫＝｛，Ｘ丨，Ｘ４，Ｘ６｝，噸＝■｛，Ｘ１，，Ｘ５，Ｘ６｝，叫＝??卜Ａ：ｈＸ４，＊ｎＸ６｝，的＝｛－＾，，Ｘ５，，Ｘ６｝，叫＝｛Ｘ３，Ｘ７｝。為了對(duì)比ＤＰＬＬ算法與??ＣＤＣＬ算法的搜索過程，將ＣＤＣＬ算法對(duì)ＪＴ賦值的搜索過程呈現(xiàn)為圖３．３中的搜索??樹。在節(jié)點(diǎn)“１１１１”發(fā)生矛盾之前，搜索流程與ＤＰＬＬ相同，之后的回溯機(jī)制??以及節(jié)點(diǎn)０Ｗ和的含義將在后文中詳述。當(dāng)在節(jié)點(diǎn)“１１１１”發(fā)生矛盾??時(shí)，生成的蘊(yùn)含圖如圖３．２所示。在第０層的邊上賦值不：＝１，在第３層的邊上??賦值Ｘ４：＝ｌ以后，在第４層的頂點(diǎn)上由叱得出Ｘ５＝ｌ。因此，在蘊(yùn)含圖中有兩條??標(biāo)記為叱的有向邊分別從‘％?：＝?１?＼?０”和“＆?：＝?１?＼?３”指向“Ｘ５?＝?１?＼?３”。??矛盾集合用ＣＳ（Ａ／）表示。在求ＣＳ（Ａ〇之前，首先定義集合兒Ｐ（ｇ）。ＡＰＯ）是??一個(gè)賦值的集合，元素為在子句＾中
【參考文獻(xiàn)】：
期刊論文
[1]CDCLSAT求解器的重啟策略分析[J]. 程睿,周彩蘭,徐寧,周強(qiáng). 計(jì)算機(jī)輔助設(shè)計(jì)與圖形學(xué)學(xué)報(bào). 2018(06)
[2]調(diào)查傳播算法收斂的一個(gè)充分條件[J]. 王曉峰,許道云,姜久雷,唐延輝. 中國(guó)科學(xué):信息科學(xué). 2017(12)
[3]基于加強(qiáng)概率控制策略的SAT局部搜索算法[J]. 洪劍珂,張崢華,許貴平. 計(jì)算機(jī)工程與應(yīng)用. 2017(14)
[4]求解SAT問題的算法的研究進(jìn)展[J]. 郭瑩,張長(zhǎng)勝,張斌. 計(jì)算機(jī)科學(xué). 2016(03)
本文編號(hào)：3002641
【文章來(lái)源】：中國(guó)科學(xué)院大學(xué)(中國(guó)科學(xué)院重慶綠色智能技術(shù)研究院)重慶市
【文章頁(yè)數(shù)】：79 頁(yè)
【學(xué)位級(jí)別】：碩士
【部分圖文】：
圖３．１?ＤＰＬＬ搜索樹圖示??元傳播化簡(jiǎn)的公式Ｊｅ
圖３．２蘊(yùn)含圖示例??
?關(guān)于布爾可滿足性判定的新方法研究???ｆ?０?Ｊ——?０⑴??，２＝１０＾０??，＝１?￡）??圖３．３?ＣＤＣＬ搜索樹圖示??（在第／ｅｖｅ／層）與其父節(jié)點(diǎn)的邊（在第／ｅｖｄ－１層）對(duì)應(yīng)的賦值，記Ｌｅｖｄ（Ｘｕ）?＝??／ｅｖｄ－１。另一種頂點(diǎn)是矛盾頂點(diǎn)，記為Ａ＾，由其他的頂點(diǎn)推出。蘊(yùn)含圖中，有??向邊的出發(fā)點(diǎn)是賦值（決策賦值或者蘊(yùn)含賦值），終點(diǎn)是蘊(yùn)含賦值或者矛盾。有??向邊用的標(biāo)記，表示代入這條邊出發(fā)點(diǎn)對(duì)應(yīng)的賦值后，Ｍ成為新的單元子句或??者空子句，用單元傳播推出終點(diǎn)對(duì)應(yīng)的蘊(yùn)含賦值或者矛盾。??仍然以〇＾公式７７＝｛０１，〇）２，，．，，叫｝為例，其中，〇；１?＝?｛＾＇１，＆｝，〇）２?＝??｛Ｘ２，Ｘ３｝，的＝卜＆，￣＾４，＾｝’?叫＝｛，Ｘ丨，Ｘ４，Ｘ６｝，噸＝■｛，Ｘ１，，Ｘ５，Ｘ６｝，叫＝??卜Ａ：ｈＸ４，＊ｎＸ６｝，的＝｛－＾，，Ｘ５，，Ｘ６｝，叫＝｛Ｘ３，Ｘ７｝。為了對(duì)比ＤＰＬＬ算法與??ＣＤＣＬ算法的搜索過程，將ＣＤＣＬ算法對(duì)ＪＴ賦值的搜索過程呈現(xiàn)為圖３．３中的搜索??樹。在節(jié)點(diǎn)“１１１１”發(fā)生矛盾之前，搜索流程與ＤＰＬＬ相同，之后的回溯機(jī)制??以及節(jié)點(diǎn)０Ｗ和的含義將在后文中詳述。當(dāng)在節(jié)點(diǎn)“１１１１”發(fā)生矛盾??時(shí)，生成的蘊(yùn)含圖如圖３．２所示。在第０層的邊上賦值不：＝１，在第３層的邊上??賦值Ｘ４：＝ｌ以后，在第４層的頂點(diǎn)上由叱得出Ｘ５＝ｌ。因此，在蘊(yùn)含圖中有兩條??標(biāo)記為叱的有向邊分別從‘％?：＝?１?＼?０”和“＆?：＝?１?＼?３”指向“Ｘ５?＝?１?＼?３”。??矛盾集合用ＣＳ（Ａ／）表示。在求ＣＳ（Ａ〇之前，首先定義集合兒Ｐ（ｇ）。ＡＰＯ）是??一個(gè)賦值的集合，元素為在子句＾中
【參考文獻(xiàn)】：
期刊論文
[1]CDCLSAT求解器的重啟策略分析[J]. 程睿,周彩蘭,徐寧,周強(qiáng). 計(jì)算機(jī)輔助設(shè)計(jì)與圖形學(xué)學(xué)報(bào). 2018(06)
[2]調(diào)查傳播算法收斂的一個(gè)充分條件[J]. 王曉峰,許道云,姜久雷,唐延輝. 中國(guó)科學(xué):信息科學(xué). 2017(12)
[3]基于加強(qiáng)概率控制策略的SAT局部搜索算法[J]. 洪劍珂,張崢華,許貴平. 計(jì)算機(jī)工程與應(yīng)用. 2017(14)
[4]求解SAT問題的算法的研究進(jìn)展[J]. 郭瑩,張長(zhǎng)勝,張斌. 計(jì)算機(jī)科學(xué). 2016(03)
本文編號(hào)：3002641
本文鏈接：http://sikaile.net/kejilunwen/ruanjiangongchenglunwen/3002641.html
最近更新
教材專著
