作者：智源社群 賈偉
AI 這個詞被偷走了。
圖靈獎得主Alan Kay在智源大會上曾經這樣說：因為在深度學習帶來人工智慧的一波熱潮下，很多人被誤導，認為人工智慧就等於機器學習。而事實上，機器學習只是整個智慧研究中的子領域。
因此，我們始終要意識到，儘管機器學習在近十年取得了令人矚目的成就，但在此之外，仍有大量值得深度探究的其他人工智慧研究。
例如：布林可滿足性問題（Boolean satisfiability problem，SAT）。
SAT ，即確定是否存在滿足給定布林公式的解的問題。舉例來說，針對公式“a AND NOT b”，詢問是否存在一個 a 和 b 的解，能夠使公式為真，如果存在，則說這個公式可滿足；反之，則稱不滿足。例如“a AND NOT a”便是不滿足的，因為不存在一個 a 的解使公式為真。
SAT 研究的重要性，不言而喻。首先，SAT是人工智慧領域自動推理中的一個經典問題，也是歷史上第一個被證明為 NP 完全的問題。其次，在工業領域（尤其是軟硬體驗證中），SAT求解器具有廣泛的應用，例如Intel晶片和Windows作業系統驗證中都用到了SAT求解器。
在深度學習所遇挑戰愈發艱難之際，事實上，我們需要回過頭來，去看看人工智慧的其他領域的研究，特別是包含著人類知識的研究方向，將這些研究與以深度學習為代表的機器學習方法進行結合，從而創造出下一代具有知識的人工智慧演算法。同時也只有從一個全面的角度，才能認清人工智慧的全貌，而不被深度學習這“一葉”而障了目。
智源針對SAT的研究及發展，與中科院軟體所研究員蔡少偉進行了一次深度對話，從中或可一窺 SAT 研究的進展及社群現狀。
蔡少偉，是國內少有的幾位對 SAT 有較深入研究的學者之一。他在近日與其博士生張昕荻共同開發的SAT 求解器在SAT Competition 2020比賽中獲得了Main Track SAT冠軍。此外，蔡少偉團隊也曾獲得SAT Competition 2014、2016亞軍和2012、2018冠軍的獎項，以及2018年聯合邏輯奧林匹克金牌。他所提出的約束求解技術和研製的SAT求解器被分別應用於微軟Azure雲平臺的虛擬機器預配置和異常檢測、騰訊地圖最佳化以及美聯邦通訊委員會的頻譜分配等專案中。
Q1：恭喜你再次獲得SAT國際比賽冠軍。就布林可滿足性問題（SAT）而言，目前大家似乎還比較陌生。你能不能先介紹一下？
蔡少偉：SAT也稱為命題邏輯公式可滿足性問題，就是要判斷一個命題邏輯公式是否可滿足，也即是否存在對該公式變數的一組賦值，使得公式為真。因為命題邏輯公式的變數都是布林變數，所以常常稱為布林可滿足性問題。
Q2：判定一個命題是否可滿足很有意思，但從問題研究本身以及工業應用來說，它有什麼意義呢？
蔡少偉：要談SAT的意義，得先認識到 SAT不僅僅是一個具體問題，它是個元問題，代表一種解決問題的思路。
SAT是用布林邏輯表達的，是非常底層的表達，這使得它在理論和實踐上都有很廣泛的意義。當時SAT被證明為NP完全問題，就是從圖靈機的角度去證明的。這是第一個被證明為NP完全的問題，是NP完全性理論的種子問題。很多漂亮的複雜性理論結果都和SAT有關係，隨機SAT和統計物理也有密切關係。
另一方面，SAT是有廣泛應用的，比如軟硬體驗證，數學定理的自動證明，密碼學，資源配置，生物計算，等等。SAT是軟硬體驗證的基礎引擎，像NASA，Intel，微軟這些巨頭都用到了SAT求解器去做相關的事情。
Q3：能不能從歷史角度，介紹一下SAT研究經歷過哪些階段？每個階段代表性方法及特點是什麼？
蔡少偉：SAT研究涵蓋面比較大，我就從SAT演算法相關的研究歷史講吧，比較粗糙的分可以分為三個階段。
早期階段（1960-1990）： 一般認為SAT演算法可以追溯到1960年Davis和Putnam提出的DP過程以及後來的DPLL。這也是機器定理證明歷史上的一個重要工作。1971年，SAT被證明為NP完全問題，這是另一個重要的事情，在這之後有很多複雜性方面的工作。這個時期的研究比較集中在歸結原理和複雜度研究，也包括易解子類比如2SAT和Horn SAT的研究。
快速發展階段（1990-2010）：這個階段SAT求解的研究有了巨大的進展，目前常用的SAT方法包括衝突分析子句學習（簡稱CDCL）方法和區域性搜尋方法都是在90年代提出的。
1992年，Seman和Gu幾乎同時開啟了SAT的區域性搜尋演算法研究，GSAT演算法在幾個典型的問題包括N皇后和圖著色等問題上比DPLL演算法取得了更好的效果，也引起了AI領域啟發式搜尋社群的興趣，之後出現了各種SAT區域性搜尋演算法，華裔法國教授Chumin Li老師在這方面做了一些有影響的工作。
CDCL方法是在90年代中期提出的，主要特點是非時序回溯和子句學習，之後從演算法和資料結構都有一些改進的工作。在這方面有一個典型的求解器MiniSAT，2003年研發的，後來有持續改進，基本實現了CDCL的主要技術。
另一個典型求解器就是Glucose，提出了文字區塊距離，從學習子句的管理方面對CDCL做了進一步改進。這期間，SAT求解器的應用也得到廣泛推廣。
此外，研究人員對一類特殊的SAT問題有較高的興趣，就是隨機k-SAT問題，尤其是對相變現象的研究以及對相變區隨機k-SAT的演算法研究，從理論上和求解演算法上都有不少工作，有一個基於統計物理的Survey Propagation方法在求解相變區的隨機3-SAT問題有很好的效果。
現代階段（2010至今）：2010年前後，曾經一度SAT求解的進展近乎停滯，不少人也覺得這個方向發展了那麼多年了，應該很難突破了。確實，經過快速發展的20年之後，SAT求解要進一步改進的難度更大了。
或許是停滯的期間激發了新的探索，2012年至2015年這幾年期間，出現了一批新的區域性搜尋SAT演算法，因為採用的技術和之前的有較大不同且效能上有大幅度提升，在文獻中常常被稱為現代區域性搜尋求解器，主要包括格局檢測方法和機率分佈方法，對應的代表性演算法分別是CCASat（這也是我拿到SAT比賽第一個冠軍的演算法）和ProbSAT。
在CDCL方面，對於學習子句的管理更加精緻了，並且開始有研究利用機器學習方法來改進演算法的啟發式，代表工作是Maple演算法用MAB多臂賭博機方法來改進分支啟發式。
另外，區域性搜尋和CDCL的結合引起了越來越多的興趣，尤其是最近3年，這方面的研究越來越深入，今年的SAT比賽中Main track的前三名都結合了這兩種方法。這個方向還不是很成熟，但已經顯出其潛力，我相信在接下來幾年是SAT求解的一個主要方向。
除了這兩個主要方法的發展，SAT並行處理也有了較大進展，主要是Cube-and-Conquer方法。演算法選擇器和自動演算法配置也被引入來提高SAT求解，它們是對已有的SAT演算法透過機器學習方法進行演算法或策略的自動選擇，更多的是從工程的角度去研究，SAT社群一般把它們和核心演算法區分開。此外，SAT社群對SAT應用的重視達到了新的高度，這也可以從最近幾年發表的論文看出來，從數學定理，經濟學定理的自動證明，到頻譜分配等和軟體驗證等實際專案，可以越來越多地看到SAT求解的應用，論文中的實驗也更加側重於現實資料。
Q4：你剛才提到“SAT社群”。現在以深度學習為代表的機器學習社群已經達到幾百萬的規模。那麼，研究 SAT 問題的社群目前有多大呢？
蔡少偉：這個沒有去認真統計過，也很難統計，只能從相關會議的人數和文獻的數量去估計，但有不少做這方面研究的人可能很久發一篇論文。目前SAT會議每年大概100多人，另外SAT研究的論文也主要出現在CP（約束求解領域的會議，今年錄用55篇論文）和IJCAI，AAAI等會議的相應session。總的來說，和目前比較熱的機器學習方向相比，SAT社群要小很多。
從分佈上看，最主要是歐洲，包括德國，法國，奧地利，英國，芬蘭，西班牙等，歐洲向來有邏輯和形式化的傳統，在這方面一直保持的挺好，緊接著是北美（美國和加拿大），然後，亞太地區包括中國，日本，澳大利亞，新加坡等也做，但是規模小一些。
中國在這方面的社群應該說沒有形成，做的人太少了，比較零散，學生們大都不願意做這種偏邏輯和傳統演算法的方向，可能是受到發論文和找工作的壓力的影響，不過最近幾年還是慢慢有一些人加入進來做，我覺得有個好的趨勢。
Q5：SAT比賽應該是研究SAT問題的研究者一個主要集散地了，從2002年至今，國際 SAT 學會已經舉辦了13屆SAT比賽。這個比賽對SAT社群產生了哪些有價值的影響？
蔡少偉：舉辦SAT比賽，一個是為了促進SAT求解的進展，一個也是促進SAT應用，每屆比賽都會鼓勵大家提交從現實應用編碼過來的SAT問題提交作為比賽的測試集。
我覺得SAT比賽帶來的價值是多方面的。首先是促進SAT演算法的研究，不僅是促進大家去改進演算法，而且參加比賽的程式碼大部分時候是要求開源的，這也促進大家互相學習（互相競爭），往往前一屆比賽的冠軍到了下一屆都難以保持前三名。這對學生是個很好的事情，有充分的資源可以學習。
當然，也提高了SAT社群的凝聚力和知名度，並且向工業界隨時反饋最新進展，SAT會議上也有不少來自工業界的人員去參與，去聽取最新進展，也促進了SAT求解器在工業界的應用。
Q6：這很有意思。SAT 比賽的評比過程怎樣？
蔡少偉：每屆比賽一般是在4，5月份截至求解器的提交，沒有限定你的研發時間，只要在截至時間之前提交到比賽指定的平臺即可，同時也會徵集比賽的測試集，舉辦方也會自己生成測試集並從提交的測試集裡面挑選一些作為比賽測試集。
比賽測試集只有在賽後才會公佈，每屆比賽的測試集是不一樣的。測試集來自數學問題和工業問題編碼過來的SAT問題。
當比賽提交的截至日期到了之後，組織方就會進行實驗，對提交的求解器進行評估，評估的標準主要是以給定的時間限制（比如5000秒）求解的問題個數為主，也參考求解時間。比賽結果會在當年的SAT會議上公佈。
Q7：我們注意到，從2012年起，你幾乎每屆都獲得過冠/亞軍。在每年比賽中，所使用的方法有哪些變化？而且我們也比較好奇，你每屆都能獲獎的秘訣是什麼？
蔡少偉：其實也沒有每屆都獲得過冠/亞軍，比如我在2013年SAT比賽就沒得獎。SAT Competition有時候是一年辦一次，有時候是兩年辦一次，中間一年可能是一個稱為SAT Race的活動。不過比較好的一件事是，從2012年起每一屆SAT比賽都有獲獎求解器是用到我的方法開發的。
在比較早的幾屆，也就是從2012到2016那幾年，我的SAT求解器主要是區域性搜尋求解器；從2018年開始，我主要研究對CDCL求解器的改進，這幾年主要的方法是我在2018年提出來的鬆弛CDCL方法，2018和2020我獲得冠軍的求解器都是基於該方法研發的。
說實話，我沒發現什麼獲獎的秘訣。每一屆比賽的結果公佈之前，我都不知道自己會不會得獎，所以每次到了公佈結果的時候仍然會激動。我唯一肯定的就是，我在這個方向付出了持續不斷的努力。從我本科二年級2006年第一次接觸SAT問題，我就開始喜歡這個問題，一直做到現在。現在我帶著一個博士生做這個方向，我也提醒他，這個方向的前期需要積累比較長的時間，會比較辛苦，不要羨慕其他同學發論文，我們做的事比發論文更有意義。
Q8：你在 SAT 上的研究有哪些實際應用？以及你比較關心的實際應用是哪些？
蔡少偉：我們的SAT求解器被實際專案直接呼叫的，我知道的有美聯邦通訊委員會的頻譜分配專案，義大利銀行ARC系統最佳化，以及MIT的新型材料研究專案，如果說到相關方法的應用，還包括騰訊地圖最佳化和微軟Azure雲平臺裡虛擬機預配置用到的約束求解演算法等。
目前我更加關心SAT求解在晶片驗證上的應用，實際上最近我們正在跟國內這方面的主要企業討論這方面的事情，也做了一些初步的實驗，希望有機會能為我國的晶片事業貢獻微薄的力量。
Q9：我看到你之前提到，你在人工智慧和演算法設計有著比較廣泛的興趣。那麼在這些方面，你研究思路是什麼呢？
蔡少偉：人工智慧是很大的領域，不同方法擅長求解不同型別的問題。不過現在可能很多人覺得人工智慧和機器學習是同義詞，他們可能不知道人工智慧還有約束求解和自動推理這些方向。我自己會堅持做約束求解和自動推理這些偏向於符號主義的方向。我感覺機器學習更適合於感知任務，而基於邏輯和約束的方法在認知層次會更合適一些。當然，不同的方法其實可以互相借鑑，相互融合，我相信機器學習方法可以用來提高約束求解方法。但我傾向於相信在這方面比較好的途徑是，將人類經驗知識（比如成功的演算法框架/方法）和機器學習進行結合。
此外，做求解器就是做工具，總是要找到實際問題去發揮它的價值，很多智慧應用的底層都涉及到複雜的約束問題，我們做的研究處於人工智慧比較底層的研究。
在演算法設計方面，我一直比較關心的一個事情就是，如何縮小理論演算法/複雜度理論和實驗演算法之間的距離。從現狀上，這個距離可以稱得上是鴻溝了。理論演算法有漂亮的理論結果，但是實際應用的時候卻很少有效解決問題，而實驗演算法比如SAT求解器可以很好解決實際問題，但是缺乏理論上的理解。這需要兩個方向的人互相交流合作，然而這正是目前比較缺乏的。我和幾個朋友組織了一個研討會，是關於難解問題的理論、演算法和應用，也是想促進這個事情。我和北航的許可老師就這個問題討論過很多次，談到目前對演算法的分析方法也許需要做出調整，比如理論上認為比較難的最大團問題，在實際中一些幾千萬點的大圖上卻可以在幾秒鐘精確求解，因為具體問題的難度不僅和規模有關，也和問題的結構有關，直觀上是很容易理解的事情，但是如何做就不知道了。理論演算法和實驗演算法在思路上有時候也是可以互相啟發的，比如我在SAT方面有一個關於“關鍵子句”方面的想法，就是受到一個SAT理論演算法PPSZ的啟發。上次陸品燕老師跟我討論時也提到他在考慮如何將近似演算法的方法用於啟發式演算法，我覺得很高興，越多人重視這個問題，那麼就越早有進展。
Q10：很棒，最後問一個比較寬泛的問題。你覺得做學術研究，最重要的品質是什麼？
蔡少偉：我覺得自己還是學術界的學生，現在還不適合來回答這個問題。我只知道，做學術研究，心裡得有學術，“要保守你的心，勝過保守一切。”
［博文視點贈書福利］
AI科技評論聯合博文視點贈送周志華教授“森林樹”十五本，在“周志華教授與他的森林書”一文留言區留言，談一談你和整合學習有關的學習、競賽等經歷。
AI 科技評論將會在留言區選出15名讀者，每人送出《整合學習：基礎與演算法》一本。
活動規則：
1。 在“周志華教授與他的森林書”一文留言區留言，留言點贊最高的前 15 位讀者將獲得贈書。獲得贈書的讀者請聯絡 AI 科技評論客服（aitechreview）。
2。 留言內容會有篩選，例如“選我上去”等內容將不會被篩選，亦不會中獎。
3。 本活動時間為2020年8月23日 - 2020年8月30日（23：00），活動推送內僅允許中獎一次。
