SAT問(wèn)題是計(jì)算機(jī)科學(xué)理論和人工智能中的著名問(wèn)題。NP完全問(wèn)題（NP-complete,NPC）排在千禧年七大難數(shù)學(xué)問(wèn)題之首,許多NP完全問(wèn)題都可以在多項(xiàng)式時(shí)間內(nèi)轉(zhuǎn)換為SAT問(wèn)題進(jìn)行求解。SAT問(wèn)題廣泛應(yīng)用于數(shù)學(xué)定理證明、計(jì)算機(jī)軟件與理論、工程技術(shù)、軟件驗(yàn)證以及邏輯電路等價(jià)性驗(yàn)證等多個(gè)領(lǐng)域。因而SAT問(wèn)題一直是國(guó)內(nèi)外學(xué)者關(guān)注的熱點(diǎn)問(wèn)題,設(shè)計(jì)并實(shí)現(xiàn)求解SAT問(wèn)題的高效算法具有重要的鉆研意義和應(yīng)用遠(yuǎn)景。DPLL求解器開創(chuàng)了求解SAT問(wèn)題的先河,但其算法自身的回溯機(jī)制對(duì)大規(guī)模問(wèn)題的求解有一定程度的制約性。為了提升DPLL算法的求解效率,國(guó)內(nèi)外學(xué)者們進(jìn)行了大量的研究,添加了一些關(guān)鍵技術(shù)。例如啟發(fā)式分支策略、基于沖突分析和子句學(xué)習(xí)、非時(shí)序回溯、學(xué)習(xí)子句的刪除和周期性重啟等,形成了當(dāng)前最流行的CDCL（Conflict-Driven-Clause-Learning,CDCL）求解器。基于CDCL算法結(jié)構(gòu),本文做了以下研究工作:一、借鑒VSIDS策略及其延伸策略的思想,研究變量的決策層和變量參與沖突的沖突次數(shù)對(duì)分支決策階段的影響,在此基礎(chǔ)上提出一種改進(jìn)的啟發(fā)式分支策略——基于變量決策層的啟發(fā)式變量選... 

【文章來(lái)源】：西南交通大學(xué)四川省211工程院校教育部直屬院校

【文章頁(yè)數(shù)】：59 頁(yè)

【學(xué)位級(jí)別】：碩士

【部分圖文】：

不同刪除比例的求解性能對(duì)比

圖 5-1 不同求解器對(duì) 2017 年測(cè)試?yán)那蠼庑阅軐?duì)比.2.2 2018 年 SAT 競(jìng)賽結(jié)果表 5-3 列出了四個(gè)求解器對(duì) 2018 年 SAT 國(guó)際競(jìng)賽問(wèn)題中 Main Track 組中 400 個(gè)

不同求解器對(duì)2018年測(cè)試?yán)那蠼庑阅軐?duì)比

【參考文獻(xiàn)】：
期刊論文
[1]基于演繹長(zhǎng)度的學(xué)習(xí)子句刪除策略[J]. 常文靜,徐揚(yáng),吳貫鋒.  計(jì)算機(jī)工程與應(yīng)用. 2018(16)
[2]一種求解SAT問(wèn)題的人工蜂群算法[J]. 郭瑩,張長(zhǎng)勝,張斌.  東北大學(xué)學(xué)報(bào)(自然科學(xué)版). 2014(01)
[3]著色歸結(jié)、PI著色碰撞及其完備性[J]. 陸汝占,林凱,孫永強(qiáng).  計(jì)算機(jī)學(xué)報(bào). 1987(12)

博士論文
[1]基于矛盾體分離的命題邏輯動(dòng)態(tài)自動(dòng)演繹推理求解系統(tǒng)研究[D]. 陳青山.西南交通大學(xué) 2018

碩士論文
[1]基于CDCL結(jié)構(gòu)的SAT問(wèn)題優(yōu)化策略的研究[D]. 杜忠和.西南交通大學(xué) 2018
[2]布爾可滿足關(guān)鍵問(wèn)題研究[D]. 王藝源.吉林大學(xué) 2014
[3]基于DPLL的SAT算法的研究及應(yīng)用[D]. 陳穩(wěn).電子科技大學(xué) 2011



本文編號(hào)：3616929