本文選題：命題邏輯 + 可滿足性問(wèn)題��； 參考：《西南交通大學(xué)》2016年碩士論文

【摘要】：人工智能領(lǐng)域中,研究命題邏輯公式的可滿足性(SAT)問(wèn)題具有十分重要的作用。隨著科學(xué)、技術(shù)、社會(huì)等領(lǐng)域的發(fā)展,需要解決的SAT問(wèn)題的規(guī)模變得越來(lái)越大,而傳統(tǒng)單一的算法無(wú)法適應(yīng)這些大規(guī)模的SAT問(wèn)題。因此一些針對(duì)大規(guī)模的SAT問(wèn)題的求解器應(yīng)運(yùn)而生,如Chaff、zChaff、Minisa、Lingeling等諸多著名求解器。這些求解器都并非由單一的算法構(gòu)建,而是在傳統(tǒng)的DPLL等算法的基礎(chǔ)上構(gòu)建的一套系統(tǒng),如CDCL求解器,其包含多個(gè)決策過(guò)程,在算法過(guò)程中不斷的改進(jìn)學(xué)習(xí)和調(diào)整,以更為高效的解大規(guī)模的SAT問(wèn)題。這些求解器主要分為如下幾個(gè)部分,分別是變量決策、沖突分析、子句學(xué)習(xí)和回溯機(jī)制。而其中的變量決策過(guò)程在整個(gè)算法構(gòu)架中占有十分重要的地位,一個(gè)好的變量決策策略可以減少?zèng)_突的產(chǎn)生,大量節(jié)省求解時(shí)間,因此研究變量決策過(guò)程的策略具有較為重要的意義。本文主要結(jié)合CDCL求解器構(gòu)架,做了如下幾個(gè)方面的研究工作：1、本文提出一種啟發(fā)式策略,根據(jù)所給子句、文字?jǐn)?shù)量和出現(xiàn)次數(shù),定義文字相關(guān)系數(shù)、子句相關(guān)系數(shù),進(jìn)而對(duì)初始變量決策過(guò)程提供依據(jù)；2、基于定義的相關(guān)系數(shù),給定沖突狀態(tài)定義,根據(jù)沖突狀態(tài)下的總的沖突數(shù)不斷減少的原則,進(jìn)而定義沖突穩(wěn)定狀態(tài),根據(jù)沖突穩(wěn)定狀態(tài)制定回溯回退機(jī)制策略；3、基于以上兩種策略,結(jié)合CDCL求解器形成求解SAT問(wèn)題新算法(Conflict-SAT),并采用SAT競(jìng)賽中的問(wèn)題以及TPTP問(wèn)題庫(kù)中旅行商問(wèn)題進(jìn)行實(shí)例測(cè)試,并對(duì)測(cè)試結(jié)果進(jìn)行分析比較。
[Abstract]:In the field of artificial intelligence, it is very important to study the satisfiability of propositional logic formulas. With the development of science, technology, society and other fields, the scale of SAT problem that needs to be solved becomes larger and larger, but the traditional single algorithm can not adapt to these large-scale SAT problems. Therefore, some solvers for large-scale SAT problems emerge as the times require, such as many famous solvers such as ChaffitzChaff-minisaLingeling and so on. These solvers are not constructed by a single algorithm, but a set of systems based on traditional DPLL algorithms, such as CDCL solvers, which contain multiple decision-making processes and are constantly improved and adjusted in the algorithm process. In order to solve large scale SAT problem more efficiently. These solvers are divided into the following parts: variable decision, conflict analysis, clause learning and backtracking. The variable decision process plays a very important role in the whole algorithm framework. A good variable decision strategy can reduce the conflict and save the solving time. Therefore, it is of great significance to study the strategy of variable decision process. In this paper, combining the CDCL solver architecture, we do the following research work: 1. This paper proposes a heuristic strategy, which defines the text correlation coefficient, clause correlation coefficient and clause correlation coefficient according to the given clause, the number of words and the number of occurrence times. Then it provides the basis for the decision-making process of initial variables, based on the definition of correlation coefficient, given the definition of conflict state, according to the principle that the total number of conflicts in the conflict state is decreasing, and then define the stable state of conflict. Based on the above two strategies, a new algorithm for solving SAT problem, Conflict-SAT, is developed according to the conflict stable state. Based on the above two strategies, the problem in SAT competition and the traveling salesman problem in TPTP problem database are used to test. The test results are analyzed and compared.
【學(xué)位授予單位】：西南交通大學(xué)
【學(xué)位級(jí)別】：碩士
【學(xué)位授予年份】：2016
【分類號(hào)】：TP18

【相似文獻(xiàn)】

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

1 李厚銀;許道云;萬(wàn)武族;;求解SAT問(wèn)題的線性半定規(guī)劃算法[J];計(jì)算機(jī)與數(shù)字工程;2009年11期

2 卜東波;白碩;鄧晶;;3-SAT問(wèn)題相變現(xiàn)象的統(tǒng)計(jì)描述[J];模式識(shí)別與人工智能;1997年04期

3 梁東敏,吳曄,馬紹漢;一個(gè)求解結(jié)構(gòu)SAT問(wèn)題的高效局部搜索算法[J];計(jì)算機(jī)學(xué)報(bào);1998年S1期

4 熊偉;唐璞山;;一種新的SAT問(wèn)題預(yù)處理算法[J];微電子學(xué)與計(jì)算機(jī);2007年10期

5 廉德亮,張煒,朱明程;靜態(tài)SAT問(wèn)題并行處理器的設(shè)計(jì)研究[J];深圳大學(xué)學(xué)報(bào);2002年03期

6 牟嶺;;名牌大學(xué)的第一塊敲門磚:SAT考試[J];全國(guó)新書(shū)目;2010年15期

7 張銀丹;張浩軍;;一個(gè)求解SAT問(wèn)題的新算法[J];電腦知識(shí)與技術(shù);2010年15期

8 徐云 ,陳國(guó)良 ,張國(guó)義;一種求解難SAT問(wèn)題的改進(jìn)DP算法[J];中國(guó)科學(xué)技術(shù)大學(xué)學(xué)報(bào);2002年03期

9 覃杰;鄭映春;Ella;;騏達(dá)1.6GSAT&驚百里[J];音響改裝技術(shù);2006年12期

10 周進(jìn);趙希順;;基于硬件可編程邏輯(FPGA)的SAT算法的綜述[J];電子世界;2012年06期

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

1 熊偉;唐璞山;;一種新的SAT問(wèn)題預(yù)處理算法[A];2007年全國(guó)開(kāi)放式分布與并行計(jì)算機(jī)學(xué)術(shù)會(huì)議論文集(下冊(cè))[C];2007年

2 劉剛;;從美國(guó)SAT考試看我國(guó)高考管理與評(píng)價(jià)制度改革[A];探索與創(chuàng)新——《高校招生》雜志理論研究專輯[C];2009年

3 崔振玲;沙巍;黃曉辰;鄭瑞娟;居金良;胡忠義;;SAT技術(shù)在快速檢測(cè)痰液的結(jié)核分枝桿菌中的應(yīng)用[A];2011年中國(guó)防癆協(xié)會(huì)全國(guó)學(xué)術(shù)會(huì)議論文集[C];2011年

4 項(xiàng)高友;黃志球;;基于SAT的語(yǔ)義Web服務(wù)發(fā)現(xiàn)[A];2008通信理論與技術(shù)新發(fā)展——第十三屆全國(guó)青年通信學(xué)術(shù)會(huì)議論文集（下）[C];2008年

相關(guān)重要報(bào)紙文章 前5條

1 郭松坡;SAT下半年考試為什么比上半年難[N];文匯報(bào);2013年

2 王東;SAT考試熱蘊(yùn)藏出版新賣點(diǎn)[N];中國(guó)圖書(shū)商報(bào);2007年

3 孫文婧;透視內(nèi)地學(xué)生赴港考SAT[N];文匯報(bào);2012年

4 孫蔚;SAT考點(diǎn)落戶中國(guó)內(nèi)地又何妨[N];中國(guó)消費(fèi)者報(bào);2012年

5 本報(bào)專稿 沐陽(yáng);無(wú)名武士——透視日本SAT特種警察突擊隊(duì)[N];世界報(bào);2005年

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

1 許有軍;基于擴(kuò)展規(guī)則的若干SAT問(wèn)題研究[D];吉林大學(xué);2011年

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

1 趙松云;基于子句權(quán)重求解SAT問(wèn)題[D];復(fù)旦大學(xué);2008年

2 劉婉玉;美國(guó)SAT模式研究及其對(duì)我國(guó)基礎(chǔ)教育評(píng)價(jià)的啟示[D];廣西師范大學(xué);2005年

，

本文編號(hào)：1847562