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

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

【摘要】：SAT問題是判斷命題邏輯公式可滿足性,也是NP完全問題之首,在計算機科學和人工智能等領域有重要的理論和應用價值,成為了這些領域的一個熱點研究問題。長期以來,人們對SAT問題的求解進行了深入研究,提出了很多求解SAT問題的算法,其中最流行的要數(shù)CDCL算法�；贑DCL算法,有許多的求解器被開發(fā)出來,如Chaff、zChaff、Minisat、Glucose、Lingeling等著名求解器。這些求解器都是通過對CDCL算法的變量決策、沖突分析、子句學習、回溯回退等主要部分進行不斷地替換和調整而來。本文著重研究了 CDCL算法的決策過程,也對變量決策過程進行改進。在決策過程中考慮了子句長短不一的問題,采用優(yōu)先滿足短子句的思想,利用單子句的蘊含原理和滿足較多的短子句方法,盡可能早的產生沖突或減少沖突的產生,提高算法求解SAT問題的效率�；贑DCL算法結構框架,對算法做了相應部分的替換,主要的研究工作如下:1.基于優(yōu)先滿足短子句的思想,依據(jù)子句固有的結構信息,滿足較多的子句,盡可能減少一些沖突的產生,提高算法求解SAT問題的效率,首先以在子句集中出現(xiàn)頻率較多且大多出現(xiàn)在短子句中的變量作為選擇前提,結合子句的長度,給出變量在子句中的平均長度的概念及一些相關的性質;然后將變量在子句中的平均長度,與變量出現(xiàn)的次數(shù)相聯(lián)系,設計變量權重的計算函數(shù);最后提出一種初始變量決策策略。2.依據(jù)子句長度在決策過程中的影響,以短子句為出發(fā)點,為了能夠發(fā)現(xiàn)較多的單子句,采用單子句的蘊含原理,盡可能早地發(fā)現(xiàn)沖突或避免一些沖突的產生,提高算法求解SAT問題的時間效率,首先以生成單子句為目的,結合子句的長度,構造子句權重的計算函數(shù);然后提出一種新的分支變量選擇策略。3.基于初始變量選擇策略和分支變量選擇策略形成兩種新算法,在CDCL算法結構框架上分別做了一些相應部分的改進,集成VW-SAT求解器和CW-SAT求解器,并進一步通過2015年SAT競賽中的競賽例和SAT問題庫測試例,驗證了算法的有效性。
[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.
【學位授予單位】：西南交通大學
【學位級別】：碩士
【學位授予年份】：2017
【分類號】：O141

【相似文獻】

相關期刊論文 前4條

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

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

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

4 ;[J];;年期

相關會議論文 前4條

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

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

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

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

相關重要報紙文章 前5條

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

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

3 孫文婧;透視內地學生赴港考SAT[N];文匯報;2012年

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

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

相關博士學位論文 前1條

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

相關碩士學位論文 前3條

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

2 趙松云;基于子句權重求解SAT問題[D];復旦大學;2008年

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

，

本文編號：1813667