郭瑩

摘要摘要：布爾可滿足性（簡稱SAT）問題是研究最廣泛的NP-完全（簡稱NPC）問題之一。編碼、預處理和求解算法是SAT問題求解的3個關鍵技術，近年來涌現了大量成果。SAT問題廣泛應用在生產和生活中， SAT求解技術的健壯性和綜合性能迫切需要進一步提升。從SAT問題分類、SAT問題應用領域、研究現狀及面臨的挑戰(zhàn)等方面對相關研究成果進行梳理。

關鍵詞關鍵詞：SAT問題；NP完全問題；編碼；預處理；求解算法

DOIDOI：10.11907/rjdk.162699

中圖分類號：TP301

文獻標識碼：A文章編號文章編號：16727800（2017）005020403

0引言

布爾可滿足性問題（Boolean Satisfiability Problem，簡稱SAT問題）是一個著名的判定問題[1]，不僅在數理邏輯和計算理論等方面有著舉足輕重的研究地位，而且在實際生產領域具有很高的應用價值。本文從SAT問題求解的研究背景、意義和基本概念出發(fā)，在分析國內外研究現狀基礎上，介紹了SAT問題3大求解關鍵技術：編碼、預處理和求解算法；對SAT問題求解面臨的挑戰(zhàn)進行了論述。

1SAT問題

SAT問題的基本形式指給定一個命題變量集合X和一個X上的合取范式φ（X），判斷是否存在一個真值賦值t（X），使得φ（X）為真。如果能找到，則稱φ（X）是可滿足的（satisfiable），否則稱φ（X）是不可滿足的（unsatisfiable）。SAT問題的模型發(fā)現形式指當φ（X）可滿足時，給出使公式φ（X）可滿足的一組賦值。

本文參照SAT國際競賽組別[2]，按照問題產生來源將SAT問題實例劃分為應用類（Application）、組合類（Hard combination）和隨機類（Random）。

2SAT問題應用領域

SAT問題是世界上第一個被證明的NPC問題[3]。SAT問題在計算機科學、復雜性理論、密碼系統(tǒng)、人工智能等領域發(fā)揮著至關重要的作用。然而，促使SAT問題成為持續(xù)研究熱點的主要原因在于其在現實應用中的重要性。許多包含數以萬計變量和數百萬約束的組合問題都可運用SAT求解技術處理。SAT求解器作為核心搜索引擎應用廣泛，文獻[4]對此進行了介紹，下面列出一部分應用。

（1）數學領域：數學密碼、判定圖和子圖同構、尋找圖生成樹、自動機同態(tài)、歐拉回路、布爾函數的函數依賴識別、旅行商、圖著色等問題。

（2）人工智能領域：知識編譯、規(guī)劃問題、機器識別、彈道軌跡、任務計劃、神經網絡計算、自動推理、DNA智能可編程片段生成等問題。SAT求解技術是人工智能的核心技術。

（3）計算機科學領域：約束滿足問題、難組合類問題、N皇后問題、工作流可滿足性問題、護理調度問題、擴展推理、真值維護、定理證明、數據庫檢索與維護、數據挖掘、AES密鑰調度、語義信息處理等。

（4）計算機輔助設計與制造領域：軟件模型檢查、硬件模型檢測、計算機系統(tǒng)結構設計、VLSI集成電路設計與驗證、錯誤診斷、有限狀態(tài)系統(tǒng)的模型檢測、FGPA路由、邏輯合成的技術映射、圖像解釋、寄存器分配、時序問題等。

（5）生物信息領域：單模標本推理、系譜一致性檢查等。

SAT問題越來越多地應用到生產和生活中，迫切需要提升當前SAT求解技術的健壯性和綜合性能[5]。

3SAT問題研究成果

自1960年Davis和Putnam提出DP算法[6]以來，SAT求解研究逐步受到關注。然而1971年Cook證明SAT問題是NPC之后，人們對SAT的重視程度減弱。后來人們對SAT問題有了新的認識。自1991年起，世界各國研究機構紛紛舉辦SAT競賽，眾多學者的研究熱情空前高漲，SAT算法及其實現程序的求解效率大幅提高，SAT問題逐漸在許多實際應用中顯現出強大的作用。SAT協(xié)會是目前推動SAT問題理論和應用進展的主要驅動力量，其Satlive網站[7]隨時更新SAT研究動態(tài)，發(fā)布了一系列有關會議、競賽、技術報告、論文、圖書等信息；每年舉辦一次SAT理論和應用國際學術會議，目前已召開16屆； SAT國際競賽始于2002年，每隔兩年或一年舉辦，2016年成功舉行了第10屆，匯聚了大批優(yōu)秀的SAT求解器，影響力很大。

3.1SAT問題編碼方法

實際生產中的NP難題可以轉化為SAT問題進行求解，因此，首先要進行規(guī)約和編碼，目前SAT問題編碼多采用CNF形式。DIMACS [8]作為標準格式廣泛用于CNF布爾公式，也被歷屆SAT國際競賽采用。DIMACS文件用字符“c”引導的注釋文字行開始。緊接注釋之后的一行“p cnf ”表示該實例是CNF形式的公式，nbvar指公式包含的變量數目，nbclauses指公式包含的子句數目，要求1至nbvar之間的每個變量至少在某個子句中出現一次。然后下面各行是子句序列，每個子句由一系列互不相同的介于-nbvar和nbvar的非空數字組成，并以0結束。正的數字表示相應序號變量的正文字形式，負的數字表示對應序號變量的負文字形式。

實際上，對于同一個實例，即使使用同一個求解器，不同編碼方法轉換成的SAT問題求解效率是不一樣的，SAT編碼方法是研究熱點之一。

3.2SAT問題預處理技術

最近幾年的SAT國際競賽結果證明，預處理技術對SAT求解器性能至關重要。早期的預處理技術使用原始DPLL[9]（DavisPutnamLogemannLoveland，簡稱DPLL）提出的單元傳播和純文字規(guī)則，后來發(fā)展了一些更復雜的技術如超二元解析、單元子句和探針等。近年來預處理技術出現了大量優(yōu)秀成果，如Eén 等人首次解決了化簡問題的規(guī)模性和復雜性，Marijn Heule等人提出和分析了子句消除化簡規(guī)則，Tomas Balyo等人擴展了阻塞子句消除化簡規(guī)則，Manthey提出CP3以模塊化的方式將諸多預處理技術集成到SAT求解器中，等等。

3.3SAT問題求解算法

目前典型的SAT求解算法包括確定性算法和隨機搜索算法兩大類。確定性算法采取窮舉和回溯思想，從理論上保證給定命題公式的可滿足性，并在實例無解的情況下給出完備證明，但不適用于求解大規(guī)模的SAT問題。隨機搜索算法主要基于局部搜索思想，絕大多數隨機搜索算法不能判斷SAT問題的不可滿足性，但由于采用了啟發(fā)式策略來指導搜索，在處理可滿足的大規(guī)模隨機類問題時，往往能比確定性算法更快得到一個解。

3.3.1確定性SAT求解算法

當前流行的確定性SAT求解算法幾乎都是由基于深度優(yōu)先搜索的DPLL[9]算法衍生而來的，沖突驅動子句學習（Conflict Driven Clause Learning，簡稱CDCL）[10]算法主要框架基于DPLL，是目前最重要的SAT求解算法，在沖突分析與子句學習、非時序回溯、重啟、數據結構等方面作了一系列改進。

沖突分析和子句學習方面，GRASP算法在DPLL基礎上引入沖突學習策略CDCL，Holldobler[11]進一步擴展并提出了通用的CDCL形式化描述；非時序回溯方面，一些新的智能啟發(fā)式被先后引入到求解算法中，進一步減小了問題規(guī)模和搜索空間；重啟策略方面，Wu研究了隨機化問題和重啟策略，Huang分析了基于子句學習效率的重啟效果， Haim等人則認為相比一組相對固定的回溯間隔，應更加頻繁進行重啟；數據結構方面，出現了雙觀察文字、改進存儲訪問模式等新技術。

當前代表性的CDCL求解器包括Chaff、MiniSAT[12]、Lingeling[13]、Glucose[14]、Sparrow[15]等。其中Moskewicz等人提出的Chaff算法集合了laziness、線性學習和一系列啟發(fā)式策略，強調“快速和低廉”的低負荷決策方法，是SAT求解算法的重要突破，形成流行求解器的相關思想。Lingeling、Glucose、Sparrow等近年來在SAT國際競賽中屢獲佳績。

3.3.2隨機搜索SAT求解算法

隨機搜索SAT求解算法主要基于局部搜索思想。隨機局部搜索（Stochastic Local Search，簡稱SLS）算法是最早提出的隨機搜索SAT求解算法。Selman等人提出了基于SLS思想的貪心局部搜索法GSAT，之后又針對局部最優(yōu)提出了框架性的WalkSAT。近年來，SLS算法研究取得了新進展，如避免重復翻轉的方法[16]、工程隨機搜索算法[17]、雙重配置檢查方法等。

研究人員開辟了利用進化算法（Evolutionary Algorithms，簡稱EA）求解SAT問題的新途徑。例如早期用于求解SAT問題的EA算法包括遺傳算法、擬物擬人算法Solar、禁忌搜索算法、量子免疫克隆算法、粒子群算法、量子算法、組織進化算法等，近年來一些新的SAT求解算法如人工蜂群算法[18]、模擬DNA算法[19]等。

4SAT求解面臨的挑戰(zhàn)

求解SAT問題的目標是作出正確有效的判定，這可能需要指數級運行時間。在追求越來越快且有效執(zhí)行的求解方法時，不可避免會遇到一些錯誤[20]。一些SAT求解技術過于復雜，且需要大量的專業(yè)知識去理解概念的正確性，以及如何有效運行。盡管現有的SAT求解方法已經取得巨大成功，但仍有一些問題沒有得到高效解決，已經解決的問題可能還存在更好求解方法。一些高效求解器忽視了算法的正確性和完備性，因此研究并實現高效率的求解方法仍是當前要解決的中心問題[21]。未來研究主要包括編碼、預處理、確定性算法、隨機類算法、求解器實現、并行求解等問題。

參考文獻參考文獻：

[1]BALINT A， BELOV A， JARVISALO M， et al. Overview and analysis of the SAT challenge 2012 solver competition[J]. Artificial Intelligence， 2015（223）： 120155.

[2]KUMAR T K S， NGUYEN D T， YEOH W， et al. A simple polynomialtime randomized distributed algorithm for connected row convex constraints[C].TwentyEighth AAAI Conference on Artificial Intelligence，2014.

[3]COOK S A. The complexity of theorem proving procedures[C].Proceedings of the 3rd Annual ACM Symposium on the Theory of Computing， New York， 1971：151158.

[4]VARDI M Y. Boolean satisfiability：theory and engineering[J].Commun.ACM，2014，57（3）： 56.

[5]SAT COMPETITION.Description of the Tracks[EB/OL].http：//satcompetition.org/2014 /description.shtml， 2014.

[6]DAVIS M， PUTNAM H. A computing procedure for quantification theory[J]. Journal of the ACM （JACM）， 1960， 7（3）： 201215.

[7]SAT ASSOCIATION. SAT live [EB/OL].http：//www.satlive.org/， 2015.

[8]CHALLENGE D I M A C S. Satisfiability：suggested format[J].DIMACS Challenge， DIMACS， 1993（6）：2529.

[9]DAVIS M， LOGEMANN G， LOVELAND D. A machine program for theoremproving[J].Communications of the ACM，1962，5（7）：394397.

[10]EEN N， SORENSSON N. An extensible SATsolver[C]. Theory and applications of satisfiability testing，Springer Berlin Heidelberg， 2004：502518.

[11]HOLLDOBLER S， MANTHEY N， PHILIPP T， et al. Generic CDCLA formalization of modern propositional satisfiability solvers[C].Young Scientists' International Workshop on Trends in Information Processing， 2014： 2534.

[12]CHEN J. MiniSAT blbd[C].Proceedings of SAT Competition 2014： Solver and Benchmark Descriptions， 2014： 45.

[13]BIERE A. Yet another local search solver and Lingeling and friends entering the SAT Competition 2014[C]. SAT Competition， 2014： 3940.

[14]BELOV A， DIEPOLD D， HEULE M J H， et al. Glucose in the SAT 2014 Competition[C].SAT competition，2014：3132.

[15]BALINT A， MANTHEY N. SparrowToRiss[C].SAT Competition，2014： 7778.

[16]DUONG T T， PHAM D N， SATTAR A. A method to avoid duplicative flipping in local search for SAT[M].Advances in Artificial Intelligence， Springer Berlin Heidelberg， 2012：218229.

[17]BALINT A. Engineering stochastic local search for the satisfiability problem[C].Universitat Ulm：Fakultat für Ingenieurwissenschaften und Informatik， 2014.

[18]郭瑩， 張長勝，張斌.一種求解 SAT 問題的人工蜂群算法[J].東北大學學報：自然科學版， 2014， 35（1）：2932.

[19]DAI P， ZHOU K， WEI Z， et al. Simulation DNA algorithm[M].BioInspired ComputingTheories and Applications， Springer Berlin Heidelberg， 2014： 8387.

[20]WETZLER N D. Efficient， mechanicallyverified validation of satisfiability solvers[D]. Wichita St Austin：the University of Texas At Austin， 2015.

[21]BALINT A， BELOV A， JARVISALO M， et al. Overview and analysis of the SAT challenge 2012 solver competition[J]. Artificial Intelligence， 2015（223）： 120155.

責任編輯（責任編輯：杜能鋼）