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

【摘要】：人工智能領(lǐng)域中,研究命題邏輯公式的可滿足性(SAT)問題具有十分重要的作用。隨著科學(xué)、技術(shù)、社會等領(lǐng)域的發(fā)展,需要解決的SAT問題的規(guī)模變得越來越大,而傳統(tǒng)單一的算法無法適應(yīng)這些大規(guī)模的SAT問題。因此一些針對大規(guī)模的SAT問題的求解器應(yīng)運(yùn)而生,如Chaff、zChaff、Minisa、Lingeling等諸多著名求解器。這些求解器都并非由單一的算法構(gòu)建,而是在傳統(tǒng)的DPLL等算法的基礎(chǔ)上構(gòu)建的一套系統(tǒng),如CDCL求解器,其包含多個決策過程,在算法過程中不斷的改進(jìn)學(xué)習(xí)和調(diào)整,以更為高效的解大規(guī)模的SAT問題。這些求解器主要分為如下幾個部分,分別是變量決策、沖突分析、子句學(xué)習(xí)和回溯機(jī)制。而其中的變量決策過程在整個算法構(gòu)架中占有十分重要的地位,一個好的變量決策策略可以減少沖突的產(chǎn)生,大量節(jié)省求解時間,因此研究變量決策過程的策略具有較為重要的意義。本文主要結(jié)合CDCL求解器構(gòu)架,做了如下幾個方面的研究工作：1、本文提出一種啟發(fā)式策略,根據(jù)所給子句、文字?jǐn)?shù)量和出現(xiàn)次數(shù),定義文字相關(guān)系數(shù)、子句相關(guān)系數(shù),進(jìn)而對初始變量決策過程提供依據(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問題新算法(Conflict-SAT),并采用SAT競賽中的問題以及TPTP問題庫中旅行商問題進(jìn)行實例測試,并對測試結(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é)位級別】：碩士
【學(xué)位授予年份】：2016
【分類號】：TP18

【相似文獻(xiàn)】

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

2 王東;SAT考試熱蘊(yùn)藏出版新賣點[N];中國圖書商報;2007年

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

4 孫蔚;SAT考點落戶中國內(nèi)地又何妨[N];中國消費者報;2012年

5 本報專稿 沐陽;無名武士——透視日本SAT特種警察突擊隊[N];世界報;2005年

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

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

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

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

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

，

本文編號：1847562