發(fā)布時間：2018-04-28 03:58

  本文選題：SAT問題 + CDCL算法�。� 參考：《西南交通大學(xué)》2017年碩士論文

【摘要】：SAT問題是判斷命題邏輯公式可滿足性,也是NP完全問題之首,在計算機科學(xué)和人工智能等領(lǐng)域有重要的理論和應(yīng)用價值,成為了這些領(lǐng)域的一個熱點研究問題。長期以來,人們對SAT問題的求解進行了深入研究,提出了很多求解SAT問題的算法,其中最流行的要數(shù)CDCL算法�；贑DCL算法,有許多的求解器被開發(fā)出來,如Chaff、zChaff、Minisat、Glucose、Lingeling等著名求解器。這些求解器都是通過對CDCL算法的變量決策、沖突分析、子句學(xué)習(xí)、回溯回退等主要部分進行不斷地替換和調(diào)整而來。本文著重研究了 CDCL算法的決策過程,也對變量決策過程進行改進。在決策過程中考慮了子句長短不一的問題,采用優(yōu)先滿足短子句的思想,利用單子句的蘊含原理和滿足較多的短子句方法,盡可能早的產(chǎn)生沖突或減少沖突的產(chǎn)生,提高算法求解SAT問題的效率�；贑DCL算法結(jié)構(gòu)框架,對算法做了相應(yīng)部分的替換,主要的研究工作如下:1.基于優(yōu)先滿足短子句的思想,依據(jù)子句固有的結(jié)構(gòu)信息,滿足較多的子句,盡可能減少一些沖突的產(chǎn)生,提高算法求解SAT問題的效率,首先以在子句集中出現(xiàn)頻率較多且大多出現(xiàn)在短子句中的變量作為選擇前提,結(jié)合子句的長度,給出變量在子句中的平均長度的概念及一些相關(guān)的性質(zhì);然后將變量在子句中的平均長度,與變量出現(xiàn)的次數(shù)相聯(lián)系,設(shè)計變量權(quán)重的計算函數(shù);最后提出一種初始變量決策策略。2.依據(jù)子句長度在決策過程中的影響,以短子句為出發(fā)點,為了能夠發(fā)現(xiàn)較多的單子句,采用單子句的蘊含原理,盡可能早地發(fā)現(xiàn)沖突或避免一些沖突的產(chǎn)生,提高算法求解SAT問題的時間效率,首先以生成單子句為目的,結(jié)合子句的長度,構(gòu)造子句權(quán)重的計算函數(shù);然后提出一種新的分支變量選擇策略。3.基于初始變量選擇策略和分支變量選擇策略形成兩種新算法,在CDCL算法結(jié)構(gòu)框架上分別做了一些相應(yīng)部分的改進,集成VW-SAT求解器和CW-SAT求解器,并進一步通過2015年SAT競賽中的競賽例和SAT問題庫測試?yán)?驗證了算法的有效性。
[Abstract]:SAT problem is not only the satisfiability of judging propositional logic formula, but also the head of NP complete problem. It has important theoretical and application value in computer science and artificial intelligence, and has become a hot research problem in these fields. For a long time, people have deeply studied the solution of SAT problem, and put forward many algorithms to solve SAT problem, among which the most popular one is CDCL algorithm. Based on the CDCL algorithm, many solvers have been developed, such as the famous solvers such as ChaffitzChaffa Minisatt Glucose Lingeling and so on. These solvers are used to replace and adjust the main parts of CDCL algorithm, such as variable decision, conflict analysis, clause learning, backtracking and so on. In this paper, the decision process of CDCL algorithm is studied, and the variable decision process is improved. In the decision-making process, the problem of different length of clause is considered, the idea of priority satisfying short clause is adopted, the principle of implication of single child sentence and the method of satisfying more short clauses are used to produce conflict or reduce conflict as early as possible. The efficiency of the algorithm for solving SAT problem is improved. Based on the CDCL algorithm framework, the corresponding part of the algorithm is replaced. The main research work is as follows: 1. Based on the idea of first satisfying the short clause and according to the inherent structure information of the clause, it can satisfy more clauses, reduce some conflicts as far as possible, and improve the efficiency of the algorithm to solve the SAT problem. Firstly, the concept of the average length of the variable in the clause and some related properties are given by taking the variable which appears frequently in the set of clauses and mostly in the short clause as the premise of selection, combined with the length of the clause. Then the average length of the variable in the clause is related to the number of times the variable appears, and the calculation function of the variable weight is designed. Finally, an initial variable decision strategy .2. is proposed. According to the influence of clause length in the decision-making process, taking the short clause as the starting point, in order to find more single sub-sentences and adopt the implication principle of single clause, we can find conflicts or avoid some conflicts as early as possible. In order to improve the time efficiency of the algorithm for solving the SAT problem, a new branch variable selection strategy, .3., is proposed, which combines the length of the clause with the length of the clause, and constructs the function of calculating the weight of the clause. Based on the initial variable selection strategy and the branch variable selection strategy, two new algorithms are formed, and some corresponding improvements are made on the framework of the CDCL algorithm, which integrates the VW-SAT solver and the CW-SAT solver. Furthermore, the effectiveness of the algorithm is verified by the competition examples in the 2015 SAT competition and the test examples of the SAT problem library.
【學(xué)位授予單位】：西南交通大學(xué)
【學(xué)位級別】：碩士
【學(xué)位授予年份】：2017
【分類號】：O141

【相似文獻】

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

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

2 宮凌;;外教英語教學(xué)與學(xué)生SAT備考的關(guān)聯(lián)性分析[J];科技信息;2013年09期

3 張奎,陳大岳;可滿足性(SAT)問題的概率研究[J];數(shù)學(xué)進展;2001年03期

4 ;[J];;年期

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

1 熊偉;唐璞山;;一種新的SAT問題預(yù)處理算法[A];2007年全國開放式分布與并行計算機學(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考試熱蘊藏出版新賣點[N];中國圖書商報;2007年

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

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

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

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

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

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

1 吳小瑞;基于子句權(quán)重求解SAT問題算法的研究[D];西南交通大學(xué);2017年

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

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

，

本文編號：1813667