布爾可滿足性問題研究綜述

郭瑩

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

關(guān)鍵詞關(guān)鍵詞：SAT問題；NP完全問題；編碼；預(yù)處理；求解算法

DOIDOI：10.11907/rjdk.162699

中圖分類號：TP301

文獻(xiàn)標(biāo)識碼：A文章編號文章編號：16727800（2017）005020403

0引言

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

1SAT問題

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

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

2SAT問題應(yīng)用領(lǐng)域

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

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

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

（3）計算機科學(xué)領(lǐng)域：約束滿足問題、難組合類問題、N皇后問題、工作流可滿足性問題、護(hù)理調(diào)度問題、擴(kuò)展推理、真值維護(hù)、定理證明、數(shù)據(jù)庫檢索與維護(hù)、數(shù)據(jù)挖掘、AES密鑰調(diào)度、語義信息處理等。

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

（5）生物信息領(lǐng)域：單模標(biāo)本推理、系譜一致性檢查等。

SAT問題越來越多地應(yīng)用到生產(chǎn)和生活中，迫切需要提升當(dāng)前SAT求解技術(shù)的健壯性和綜合性能[5]。

3SAT問題研究成果

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

3.1SAT問題編碼方法

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

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

3.2SAT問題預(yù)處理技術(shù)

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

3.3SAT問題求解算法

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

3.3.1確定性SAT求解算法

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

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

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

3.3.2隨機搜索SAT求解算法

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

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

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

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

參考文獻(xiàn)參考文獻(xiàn)：

[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].東北大學(xué)學(xué)報：自然科學(xué)版， 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.

責(zé)任編輯（責(zé)任編輯：杜能鋼）