在人工智慧時代，他們不做深度學習。

蔡少偉清晰地記得，2011 年夏天他去美國密歇根大學安娜堡分校參加 SAT 會議時，一眼望去，全場只有他一箇中國人。

參會人員一半來自歐洲，四分之一來自北美（尤其是美國），另外四分之一則來自亞太地區。他將自己的“單刀赴會”列為 SAT 2011 一行的兩大記憶點之一，另一點是那年大會主席的論文被 SAT 評委“槍斃”了。

這是蔡少偉第一次參加 SAT。這個被 CCF 列為 B 類的會議全稱為“International Conference on Theory and Applications of Satisfiability Testing”（可滿足性判定的理論與應用國際會議），始設於 1997 年，主要面向研究可滿足性問題，尤其是布林可滿足性（Boolean Satisfiability Problem，簡稱“SAT”）問題的科研人員，向來少為中國學者問津。

不過，蔡少偉似乎對這份“孤軍作戰”的寂寞也早已見慣不慣。當時，他在北京大學計算機系的理論實驗室攻讀博士，師從蘇開樂，是當時組裡唯一一位研究 SAT 求解演算法的人。作為數理邏輯基礎問題又是 NP 完全問題，SAT 求解同時注重符號推理與演算法設計，還需要巧妙的資料結構和精緻的程式碼實現，難度極高。

▲圖 / 蔡少偉（左）參加 SAT 2011 時，遇到同是研究隨機區域性搜尋的德國烏爾姆大學博士生 Adrian Balint（右），討論不過癮，決定直接上機器 PK

同樣經歷過“四下無人”的少數者，還有 2009 年從斯坦福畢業回國的葛鼕鼕。那一年，他從斯坦福大學管理科學與工程系（MS&E）取得運籌學博士學位，拿到了上海交通大學的教職 offer，準備回國任教。

讀博期間，他師從運籌學泰斗、馮・諾依曼理論獎的唯一華人獲獎者葉蔭宇，主要研究大規模優化理論與演算法，並不直接研究求解器，只是在研究某些整數規劃的問題時經常需要呼叫。但回國後，他卻發現，國內居然沒有人開發商用求解器。凡是需要用到求解器的企業，都是直接購買美國的 CPLEX、GUROBI 與 XPRESS。

“求解器分為專業版、個人版與商用版，不同版本有不同的價格，5 萬到 40 萬人民幣不等。”葛鼕鼕談道，“中國沒有求解器，要從國外買，人家不可能給你降低價格。如果買幾千臺的話，幾個億的外匯就這樣出去了。”

看到國內在求解器研究上的空白，葛鼕鼕感到很奇怪：為什麼沒有人做？但那時，他剛步入教職不久，身兼數職，也沒有條件去作更多的研究。直到 2013 年，他從交大轉到上海財經大學、擔任交叉科學研究院院長，有機會組建自己的團隊，才開始帶隊探索。

▲圖 / 剛步入教職的葛鼕鼕

十年過去，再回頭看，從無人區走出來的蔡少偉與葛鼕鼕，都已成為國內研究求解器的青年先驅人物。但是，談起求解器的研究現狀，他們的結論仍與十年前無異，“就一小撮人”。

事實上，在深度學習興起之前，人工智慧十分注重邏輯推理（reasoning），當時偏符號主義的 SAT 問題比深度學習還流行。

從“解題”的角度看，一切人工智慧系統都可以歸結為“問題求解”（Problem Solving）系統，即為了實現給定目標而展開的動作序列的過程。而解決特定問題的演算法，被稱為“求解器”（solver）。無論是 SAT 求解器，還是整數規劃求解器，都是經典的離散約束演算法問題。

求解器在工業發展中的意義非凡。例如，中國戰略佈局上亟待解決的“卡脖子”難題 EDA （電子設計自動化）需要用到 SAT 求解器進行快速驗證，而製造、物流與供應鏈優化等則需要用到整數規劃求解器（尤其是線性規劃求解器）。因此，近兩年，華為與阿里也開始佈局求解器研究。

江湖傳聞，華為內部對求解器研究十分重視，多個海內外團隊同時推進，任總直接聽取彙報。由於人才供給緊缺，蔡少偉所培養的博士畢業生入職華為後，待遇直接對標“華為天才少年”，年薪近百萬。

從 SAT = NP-Complete 談起

探討 SAT 求解器之前，我們首先要了解 SAT 問題的研究歷史。

說來牛叉，SAT 問題是計算機歷史上第一個被證明為 NP-Complete 的問題，其主要貢獻者就是計算複雜理論研究方向的大神、現任多倫多大學計算機系與數學系的教授 Stephen A. Cook。

▲圖 / 1982 年圖靈獎獲得者 Stephen Cook

在 1971 年的論文“The Complexity of Theorem Proving Procedures”中，Stephen Cook 提出了著名的庫克定理（Cook Theorem），從圖靈機的角度證明所有 NP 問題都可以快速轉化為 SAT 問題。

在庫克定理裡，圖靈機的計算過程可以用 SAT 表達出來，轉化成一條條獨立的語句，十分簡單，但又極高效。庫克定理指出，如果 SAT 問題可以快速求解，那麼所有 NP 問題都可以快速求解。Cook 本人也因此獲得 1982 年圖靈獎。

廣義上，可滿足性（Satisfiability）問題是指對給定邏輯公式判定是否可滿足的問題。SAT 問題特指“布林可滿足性問題”，又稱“命題邏輯可滿足性問題”。命題邏輯是形式邏輯最基本的類別，基本元素是布林變元。每個布林變元代表一個基本命題。SAT 問題的本質，是探求一大堆布林變元之間的邏輯推理關係是否成立。

聽起來很高深，但描述十分簡單。舉個例子：

甲乙丙想參會，甲說：乙參會我就參會，乙說：丙參會我就參會，而丙說：甲參會我就不參會，那麼能不能同時滿足甲乙丙的參會需求？

這就是一個 SAT 問題，而求解的答案是：他們的需求是不可（同時）滿足的。如果命題簡單，那麼人腦可以很快判定邏輯推理關係是否成立。但隨著布林變元和約束的條件越來越多，SAT 的求解就會越來越難，需要藉助演算法來進行推理與計算。

比方說，在進行機場飛機排程時，研究人員要考慮的狀態非常多，包括待起飛的飛機數量，飛機分佈的跑道數量與位置，飛機的執行方向，風向等等。一個布林變元表示單一時空下的一種狀態。由此可見，布林變元所表達的資訊非常小，只有 0 與 1 。如果要表達完全部有用資訊，那麼涉及到的變元數量可能是成千上萬億。

這種“描述起來十分簡單、卻可以延伸出深入研究”的問題個性十分吸引蔡少偉。

2006 年，蔡少偉在本科班主任王家兵的帶領下首次接觸 SAT 問題。當時，他正就讀於華南理工大學電腦科學與技術專業，剛上大二。王家兵對 SAT 問題很感興趣，見蔡少偉數學底子不錯，就讓他協助研究。為了完成這些工作，蔡少偉跑去圖書館查詢資料，由此入門。

本科畢業後，蔡少偉直博北大。在確定研究方向時，蔡少偉先是摸索了一年，最後發現還是求解演算法方向最有趣，就選擇繼續研究 SAT 求解器。

從接觸 SAT 問題開始，他就知道這是一塊“硬骨頭”。

首先，國內研究 SAT 的學者少，知識傳承不足。上世紀 90 年代，雖然國內也有研究 SAT 問題的學者，比如北航的李未院士，華中科技大學的黃文奇教授，還有中科院軟體研究所的張健研究員。蔡少偉入門 SAT 所讀的第一本著作，就是張健的《邏輯公式的可滿足性判定 —— 方法、工具及應用》。但是，這些研究都沒有形成一個派系。

其次，研究 SAT 求解器需要紮實的數學基礎，且對演算法設計和工程實現的能力要求極高，往往需要投入數年努力才有論文產出，對研究人員的心智與耐力都是一種考驗。蔡少偉自問，雖然自己熱愛數學與演算法，但並不擅長，也無天賦。

導師蘇開樂擅長的是邏輯系統，卻支援他選擇自己喜歡的求解演算法研究。他是當時實驗室裡唯一做求解器的學生。在這種先天條件不足、後天支援有限的情況下，蔡少偉獨自探索，過程的艱難可想而知。

▲圖 / 蔡少偉

他回憶，當時研究 SAT，最大的困難是沒有足夠的機器。研究求解器要做大量實驗，而他只有一個非常普通的筆記本。由於沒日沒夜地跑實驗，這個筆記本後來還被燒壞了。無奈之下，他只有求助室友，借對方實驗室的伺服器來跑實驗。“不過，這對現在的學生來說已經不是難題，因為現在的計算資源比當時先進多了。”蔡少偉談道。

早在上世紀 60 年代，SAT 問題就有了第一個求解演算法，叫“Davis-Putnam algorithm”（又稱“DP 演算法”），由 Martin Davis 與 Hilary Putnam 提出。後來，DP 演算法又迭代為“DPLL（Davis–Putnam–Logemann–Loveland）演算法”，之後的系統搜尋演算法主要是基於 DPLL 演算法的框架，是解決約束滿足性最常用的演算法（即回溯搜尋法）。

到了 90 年代，衝突分析子句學習（CDCL）方法與區域性搜尋方法出現。其中，CDCL 在系統搜尋演算法中加入了衝突分析等關鍵技術，而區域性搜尋演算法作為主要的啟發式演算法為人所知。1992 年，Bart Selman 提出的區域性搜尋演算法 GSAT 在 N 皇后與圖著色等多個經典問題上取得了比 DPLL 演算法更好的效果，引起了人工智慧領域啟發式搜尋社群的興趣，期間出現各類區域性搜尋演算法。而 CDCL 方法極大提高了 DPLL 演算法的效能，使得 SAT 求解器的應用得到推廣。

此外，研究人員開始對隨機 k-SAT 問題產生興趣，在相變現象研究與相變區隨機 k-SAT 的演算法研究上取得了許多成果，包括 Alfredo Braunstein 等人在 2002 年提出的基於統計物理的調查傳播（Survey Propagation）方法。在中國，北航的許可教授是深入研究相變現象的研究者之一。但 2010 年前後，SAT 求解的進展近乎停滯。

在蔡少偉讀博時，許多人都認為，SAT 問題經過多年的快速發展，已經很難取得進一步的突破。比如，當時他想解決的問題是區域性搜尋演算法求解大規模 SAT 例項。但是，在他入場時，區域性搜尋已經不被大多數人看好，處於被邊緣化的地位。

明知山有虎，偏向虎山行。還是一座付出與回報不成正比的土頭山。問蔡少偉，當時研究的課題遇上關卡、停滯幾個月時，是否想過換方向，揀一個比較容易的題做。他說，那時候自己就是“執迷不悟”，不願意跟在別人的屁股後做研究，覺得沒意思。

蔡少偉的口頭禪是，“做研究就是要有自己的 label（標籤）。”

與巨人同行

所謂開闢，往往離不開前人鋪就的奠基石。

雖然蔡少偉與導師蘇開樂的研究方向不同，他只能靠自己摸索，但在蘇開樂的帶領下，他有幸結識了一群研究 SAT 問題的前輩，比如法國儒爾-凡爾納大學（University of Picardie Jules Verne）計算機系的華人教授李初民。

李初民從 1994 年開始研究 SAT 問題，是最早研究 SAT 問題的華人學者之一。他是華中工學院（現華中科技大學）計算機軟體專業的第一屆畢業生，1983 年取得學士學位，後赴法國留學，分別於 1985 年和 1990 年在貢比涅大學（University of Technology of Compiegne）計算機系取得了碩士與博士學位。

▲圖 / 李初民

博士畢業後，李初民留在法國任教。他入門 SAT，是因為在上《可計算性》這門課時，需要用圖靈機進行計算，上課過程中，他發現 SAT 求解器就像一把萬能的鑰匙，只要解決 SAT 問題，其他許多問題也可以快速求解，於是開始研究 SAT。

有句話說，“始於外貌，陷於才華，忠於人品。”這很符合 SAT 研究者的心路歷程。李初民也一樣，他被 SAT 問題吸引的原因與蔡少偉相似，“（SAT）看起來很簡單，非常容易上手，卻有著極強大的表達能力，可以很方便地用它來表達其他問題，比如圖染色問題。”

如李初民介紹，SAT 的本質是形式邏輯，表面看上去很簡單，但豐富的資訊量都隱藏在一條條語句中。既純粹，又神祕。所以，從入門 SAT 後，李初民就一心撲在了 SAT 問題的求解上。

在上世紀 90 年代所湧現的一大批演算法中，李初民與 Anbulag 在 1997 年所提出的 SATZ 求解器（發表在 IJCAI 1997）受到了極大關注，相關論文被引用了超過 500 次。直到今天，SATZ 也是求解隨機 SAT 問題最好的求解器之一。

李初民教授在 SAT 求解器的研究上堅持了二十多年，在這個領域並不常見。許多人都曾為 SAT 問題著迷，但最終能堅持下來的人卻很少，主要的原因就在於：要在 SAT 問題上取得新的成果很難。

從上世紀 60 年代至今，SAT 問題的研究已經持續了大半個世紀，傳統的、簡單的演算法都已經有許多外國學者試過。在這種相對成熟的領域去做研究，就是前人已經搭了萬丈高樓，你首先要花很長時間搭一條足夠長的梯子，瞭解前人已經研究過的知識，然後伸長手臂，站在高高的梯子上，用力往萬丈高樓上丟一顆小小的石子。

“就像今年奧運會的蘇炳添，在百米賽跑中兩次跑進 10 秒。雖然沒有拿金牌，但我們都知道他非常了不起，因為他每進步百分之一秒，都是難上加難。”李初民形容，“SAT 問題的後繼研究者也是一樣。”

▲圖 / 蘇炳添在 2021 年東京奧運會中跑進 10 秒

除了開闢的艱辛，李初民認為，研究 SAT 求解的難點還在於，具有實際意義的 SAT 求解技術通常很簡單，主要通過大量繁重的實驗來支撐，因此寫出來的論文看起來並不高深，投到頂會的論文很容易被不懂行的審稿專家“槍斃”。

李初民有這方面的親身經歷。2017 年，他指導學生實現了一項子句精簡技術，非常有效，投到 IJCAI 後，有審稿專家就說，很多人都已經實現過這個技術，因此論文沒有創新。“幸好有一個行家指出我們與別人的不同，論文才逃過了被‘槍斃’的命運。”後來，憑藉這項技術，他們獲得了當年 SAT 競賽的金牌，這項技術與他們的實現方式也成為了 SAT 求解器的標準配置。

除了自己研究 SAT 求解器，李初民也樂於指導對 SAT 求解有興趣的年青人。

蔡少偉也許是李初民指導過的學生中，堅持研究 SAT 最久的學生。他從 2009 年正式開始 SAT 以及相關問題的演算法研究，第一個成果是利用 SAT 求解的約束加權技術設計另一個經典 NP 難問題---最小頂點覆蓋問題的區域性搜尋演算法，該演算法 EWLS 在一個著名挑戰例項 frb100-40 上打破了當時的世界紀錄。之後，他繼續深入區域性搜尋演算法研究，嘗試解決其重要缺陷，即迴圈問題。

系統搜尋與隨機（區域性）搜尋是 SAT 問題中的兩大方向。拿走地圖舉例，系統搜尋是：走走剪剪，走到地圖的哪一塊，就將哪一塊剪掉，所以這張地圖會越走越小，最後走空了，就知道所有地方都走過了；而隨機搜尋是：你在地圖上跑來跑去，但是你不記得你跑過哪些地方，沒有“剪枝能力”，無法剪掉，造成迴圈訪問的現象。

如果說 SAT 問題是電腦科學世界的大門，那麼相變現象則是大門的鎖芯，因此相變區例項也成為 SAT 求解的熱門測試集。而隨機搜尋是求解相變區例項的最有希望的方法，但對於大規模相變例項仍然有較大障礙。導致相變區難解的本質原因，就是隨機搜尋的迴圈現象。

針對這個問題，當時已有的解決方法主要是馮・諾依曼獎獲得者 Fred Glover 在 1998 年提出的禁忌搜尋策略（tabu search）與荷蘭萊頓大學教授 Holger Hoos 在 2002 年提出的隨機擾動方法。但是，它們沒有利用問題結構，無法針對問題結構做出調整，且帶有引數，在使用的時候常常需要大量的調參工作。

所以，蔡少偉思考如何克服隨機搜尋中的迴圈缺陷，希望設計出一種兩全其美的方法，既能保留隨機搜尋的優勢，又能克服其迴圈搜尋的缺陷。但這並不簡單，蔡少偉苦苦思索，停滯數月，毫無進展。心情自然十分鬱悶。

那段時間，他讀了許多無關本領域的書，尤其是博弈論與社會學。其中，許多篇章談到個體與群體的關係。帶著“如何克服迴圈缺陷”的問題，蔡少偉雖然是閱讀課外書籍，卻時時忍不住將這個問題與書中的章節內容聯絡起來，讀著讀著，突然冒出一個想法：可以利用環境資訊減輕迴圈！

雖然直覺告訴蔡少偉這個思路可行，但直到不久後，他在一次交流會上聽到李初民對 SAT 演算法研究的演講，才突然受到啟發，一剎那看到了自己苦思冥想的方法！

“世界突然安靜了，只有筆尖和紙張摩擦的聲音，我飛快地寫著，很怕是個幻覺，會馬上消失。”在個人部落格中，蔡少偉記錄了這一美妙的精神過程。也是在這一瞬間，他創造了博士期間的得意之作：格局檢測策略（CC）。

格局檢測的核心是：如果變數的環境資訊沒有改變，則不允許改變取值，而環境資訊可以是由該變數的鄰居變數的取值構成，也可以由該變數的關聯子句的狀態構成。通過避免區域性結構迴圈，減輕搜尋的迴圈現象。利用問題的結構資訊，不僅可以避免迴圈現象，還能通過設定多層評分函式克服“短視”。

▲圖 / 格局檢測策略示意圖

運用這個方法，他大幅度改進了原來的演算法，產生了第二篇論文，2011 年發表在頂刊《人工智慧期刊》（AIJ）上。

蔡少偉意識到這個新方法的通用性。他花了一段時間靜心思考，把它抽象成一個通用方法，應用到 SAT 問題上。起初並不見效，但他“已陷入 SAT 問題不可自拔”，決心作出名堂。通過半年的努力，他終於超過了當時 SAT 比賽的冠軍演算法。

但好景不長，2011 年 SAT 比賽的新冠軍又讓他的演算法黯然失色。期間幾多波折，也經歷了數個低谷，直到 2012 年 SAT 比賽，蔡少偉又扳回一城，獲得冠軍！對於這場奪冠，蔡少偉印象深刻：

2011 年年底，他開始著手準備，雖然演算法在當時已達到國際前沿，但並沒有太大的把握。過完寒假回校，他一邊忙畢業的事，一邊備戰 SAT 比賽。有兩位師弟幫忙，研究進度加快不少，“開始只是小優化，如隔靴搔癢，一直到比賽截止兩個禮拜前才有了質的飛躍。”

果然，比賽結果公佈，三條主賽道，蔡少偉組的演算法（CCSat）贏得了隨機組（測試集為相變區例項）的第一名，並且遙遙領先於第二名，求解效率比是 423（70.5%）vs 321（53.5%）。

▲圖 / 蔡少偉組的 CCSat 打敗了 Kevin Leyton-Brown 等人提出的 SATzilla 求解器

這也是中國第一次在國際 SAT 協會舉辦的 SAT 比賽系列中取得冠軍，蔡少偉的心情無比激動。在做演算法設計時，他堅持演算法大師 Dijkstra 的信條，“優雅就是簡單而高效”。他的格局檢測策略是一個全新的方法，經過凝練，簡單而高效。一路堅持下來，沒想到竟成就了自己的風格。

蔡少偉的演算法以明顯優勢奪冠，在當時的學術界也引起了較大反響。

Holger Hoos 稱 CCASat 是代表性最前沿求解器，比賽舉辦方更是以 CCASat 的成功說明研究核心演算法的重要性。2012 年前後，隨機搜尋有逐漸被邊緣化的跡象。蔡少偉提出格局檢測策略後，加上當時隨機搜尋方向的其他學者的工作（如 probSAT），隨機搜尋再一次吸引了國內外學者的注意，讓大家覺得：哦，原來隨機搜尋還有很大的研究潛力。接下來幾年，隨機搜尋吸引了更多人加入其中。現在，隨機搜尋已經成為和 CDCL 的系統搜尋並駕齊驅的兩大主流演算法之一。

2012 年從北大博士畢業後，蔡少偉繼續在 SAT 求解器上鑽研。他用兩年時間從澳大利亞格里菲斯大學獲得應用數學博士學位，2014 年回國加盟中科院軟體研究所，開始挑戰康奈爾大學計算機系教授 Bart Sellman 等人在 1997 年所提出的命題邏輯推理與搜尋十大挑戰之一：結合系統搜尋與隨機搜尋設計出比這兩種方法更高效的演算法。

與巨人同行（2）

在蔡少偉深入 SAT 求解研究的同時，時任上海財經大學交叉科學研究院院長的葛鼕鼕開始琢磨線性規劃求解器的開發。

如前所述，SAT 問題有許多變元，需要判定其為 0 或 1（真或假命題）。SAT 問題也可以表現為一個線性方程組，但變元只能取 0 或 1，又被稱為“0/1 規劃問題”。

只是，在現實生活中，問題建模可能不是線性方程，而是二次方程、三次方程、對數、指數、根號等等，x 與 y 的取值也不僅僅是 0 或 1，可以是任意數，包括整數、正數、實數……

圖 / SAT 與混合整數規劃（MIP）、約束整數規劃（CIP）及約束規劃（CP）的關係

葛鼕鼕是運籌學出身。運籌學研究問題主要分兩步，第一步是建模，第二步是求解：將現實中的問題通過演算法建成標準的數學模型（如線性不等式）後，再對數學模型進行求解，從而解決現實問題。如果變數少，只有 x 與 y，那麼我們可以進行手算；但當數學模型涉及到幾百萬變數，則必須藉助軟體（如 matlab）來自動計算。

本質上，求解器就是一個專業的數學/計算軟體，用於實現複雜的數學演算法。當軟體對線性方程組求解時，該軟體可以稱為“線性方程組的求解器”。計算機歷史上最早的求解器，就是線性規劃求解器。

葛鼕鼕對求解器有所耳聞，要追溯到他在斯坦福讀博的師門關係：

1947 年，“線性規劃之父”、斯坦福大學教授 George Dantzig （葛鼕鼕的師爺）提出了第一個用於優化線性系統的演算法，叫“單純形法”（Simplex Method），第一次使大規模優化問題得到求解。單純形法一直雄踞二十世紀最偉大的演算法前五之列。30 年後，隨著計算機技術的發展，人們又開始嘗試用計算機開發求解軟體。1979 年，第一個求解器軟體在美國誕生，名為 LINGO。

▲圖 / George Dantzig，電影《心靈捕手》男主人公的原型

1980 年代，美國又有多位學者提出了內點法（Interior-Point algorithm）。此前，線性系統優化一直是單純形法的天下，直到內點法出現。內點法在某些問題上比單純形法的求解速度更快，可以處理許多非線性規劃問題，從而成為新的潮流，並也被用於商用求解器的開發。George Dantzig 的得意門生葉蔭宇（葛鼕鼕的導師）也是公認的內點法奠基者之一，因此獲得了運籌學的最高獎 —— 馮・諾依曼理論獎。

▲圖 / 葉蔭宇

歷史上線性規劃求解的兩大流派，都是由葛鼕鼕的師長創立。因此，讀博期間，他也跟著學習、琢磨了很多線性規劃求解例項。

與 SAT 求解器一樣，以往研究線性規劃、整數規劃或混合規劃的人員有許多，但真正狠得下心開發求解器的人極少。葛鼕鼕剛回國時，發現國內沒有人做求解器，覺得很奇怪，便去打聽，發現原因很簡單：高校不做求解器，是因為在學術上的價效比低，工具研發不能算科研；而企業不做求解器，根本上是覺得這是一個浩大而困難的工程，技術實力根本不可能做得到。

毫無疑問，求解器的開發是一個大規模系統工程，動輒上百萬行程式碼。此外，求解器軟體對開發人員的數學能力要求特別高，而中國的情況是：同時精通數學與大規模軟體開發能力的人幾乎不存在。這一點與美國形成鮮明的對比，美國學生通常是一邊思考數學問題，一邊思考如何用程式碼復現問題。

對於中國教育缺少對學生抽象思維的培養，葛鼕鼕與李初民的想法不謀而合。李初民認為，“邏輯就是力量”，即能夠深刻理解各種事物之間的邏輯關係，想得到一個果，要先去追求因，而這個因可能又是另一些事物的果。中國文化博大精深，而美中不足之處，是缺乏對形式邏輯培養的重視。所謂形式邏輯，即“符號邏輯”：把含義去掉，用無意義的符號來代表事物，比如“變元”（x）。

“不重視形式邏輯，也許是科學在中國發展緩慢的原因之一，因為科學需要大量的邏輯推理。”李初民談道。

此外，研究求解器不容易發論文。研究求解器的老員工常說一句話：“求解器的祕密就在於它沒有祕密。”就是說，求解器中的數學問題與實現演算法都能在數學論文中找到，但不同求解器寫出來的程式碼質量良莠不齊。一方面，這要考驗人的系統開發與數學結合能力；另一方面，需要花費許多時間與精力去做大量的嘗試，俗稱“踩坑”。

例如，就整數規劃中的啟發式演算法模組而言，德國的 Zuse Institute Berlin（ZIB）研究所花了近 20 年時間開發一個求解器 SCIP，裡面用了 57 種啟發式演算法做模組的加速。如果單看啟發式演算法相關的論文，全世界大概有上萬篇這樣的論文，這些論文裡大概提出了上千種能夠加速的啟發式演算法。如果要將這些啟發式演算法全部寫到軟體中，一個個地測試其實用性，可想而知工作量會有多龐大。

▲圖 / 位於德國柏林的 ZIB 研究所

從 2013 年加入上海財經大學後，葛鼕鼕便開始有意識地招收一些擅長做優化演算法的年青人。那時，他有些猶豫：“求解器這事究竟能不能做？”心裡沒底，跑去諮詢導師，葉老師很支援，說：“中國總得要自己的求解器，不要老覺得做不成，總得有人挑頭。”

於是，2015 年，葛鼕鼕聯合海內外的同門師兄弟羅小渠、王子卓與王曦，創立了杉數科技，開始倒騰求解器。杉數剛成立，葉蔭宇弟子、斯坦福博士等稱號，就為他們拿到了大約 200 萬美元的天使輪投資。

最初，他們是從上海財大的交叉科學院調配人手，加上杉數科技的創始團隊，從零開始探索做一個開源求解器。葛鼕鼕與創始團隊自學、找專家、找導師，花了很多力氣琢磨求解器開發，比如單純形法與內點法如何在軟體開發上走通全流程，弄清楚求解器開發的核心部件，矩陣資料簡化等等。

期間，葉蔭宇給了許多指導，甚至親自下場幫他們寫開原始碼。

經過兩年的摸索，他們在 2017 年釋出了中國第一個開源優化求解器 LEAVES，但效能並不突出。這使他們意識到，開發求解器是一個很大的系統工程，光靠學校的力量、投入小的成本是做不成的。所以，杉數開始在國際上祕密尋求有經驗的人，組建團隊。

“說白了，真正懂求解器開發的就是三大廠（XPRESS、GUROBI 與 CPLEX）的開發人員，每家的核心開發都不到 10 人，所以全世界真正精通求解器的不過 20 多人。”葛鼕鼕介紹，“加上德國柏林 ZIB 研究所的人，葉老師一位開發第三方商業求解器 MOSEK 的丹麥博士生和他的團隊。以及很少的一些成熟開源求解器的高手，也就是說，全世界的核心求解器開發人才，就這 30 多個人。”

圖 / 葛鼕鼕在杉數科技擔任首席科學官

幸運的是，他們最終在 XPRESS 找到了一個志同道合的中國人，本科就讀於北航計算機系，畢業後去英國讀博，博士期間的內容就是研發求解器。之後，他們又陸陸續續從 CPLEX、XPRESS 與 LINGO 等處挖到了多個程式設計師。

後來，又有一些人奔著杉數創始團隊都是葉蔭宇學生的份上而來。葉蔭宇提出的“內點法”的具體實現方法是各大商業求解器的底層架構，圈內有名，所以，在他的感召下，杉數找到了許多優秀的人才。國內的高校也開始了這方面的有意識嘗試。2018 年，中科院戴彧虹研究院團隊推出了國內第一款整數規劃求解器 CMIP。

又過了兩年，2019 年 5 月，杉數推出中國首個商用線性規劃求解器 COPT。COPT 的出現，給國內大廠傳遞了一個重要資訊：開發求解器的難度確實極高，但也不是全無可能。

隨著企業的數字化轉型，需要進行更多量化的、精細的智慧決策，藉助一些數學模型來建模，求解器的用途也越來越大。因此，國內有能力的大企業（比如華為和阿里巴巴）也開始自己琢磨做求解器。

求解器在中國

與歐美數十年前就將求解器用於航空、鐵路交通規劃不同，工業求解器在中國的落地歷史很短，最早可以追溯到 2000 年代初期，寶鋼採用 ILOG CPLEX 優化生產規劃系統。

在 COPT 出現之前，商業求解器三大廠 CPLEX、GUROBI 與 XPRESS 憑藉豐富的商業開發經驗，以及較好的效能，在國際市場上佔了超過 90% 的份額。

三大求解器中，歷史最坎坷的是 1988 年由美國數學家 Robert E. Bixby 所開發的 CPLEX。1997 年，CPLEX 由法國企業 ILOG 收購，2009 年，ILOG 又被 IBM 收購，從此 CPLEX 變成了 IBM 的求解器。當時，CPLEX 功能較完善，擅長各類求解，在市場上佔了統治地位。

▲圖 / Robert E. Bixby

但沒過多久，由於 IBM 的自身管理問題，以及對求解器業務不夠重視，IBM 求解器團隊的幾個最核心開發人員從 CPLEX 離職，出來創立了新的公司，叫 GUROBI。GUROBI 的唯一業務就是開發求解器，他們十分注重這一塊，很快超過了 CPLEX。隨著 IBM 的越發衰落，CPLEX 也隨之慢慢衰落，美國商用求解器成了 GUROBI 的天下。

與此同時，英國愛丁堡的 Dash Optimization 團隊在 1983 年開發了 XPRESS，1986 年開始應用於混合整數規劃求解。該團隊的開發人員大約有 10 人，一直相對穩定。2008 年，XPRESS 由美國金融信用商 FICO 收購，將求解器用於制定金融場景的大規模優化方案。收購後，FICO 不做過多幹涉，XPRESS 的開發團隊繼續留在英國，保持了自身的競爭力，在市場上佔有一定份額。

這三家均是開始商用求解器，以核數定價，核數越高，價格越高。在中國還沒有商用求解器之前，進口求解器的價格基本是賣方市場。杉數的 COPT 釋出後，無論核數多少，均以打包價出售，倒逼國外品牌將價格下降來競爭中國的市場。

近兩年，華為與阿里也開始佈局求解器開發。華為開發求解器，主要用於 EDA 設計、供應鏈規劃等，而阿里做求解器，則主要用於阿里雲的資源排程優化。

阿里也是從線性規劃入手，先做單純形法，再做內點法。2020 年，阿里達摩院決策智慧實驗室釋出數學規劃求解器 MindOpt。根據阿里的官方說法，在釋出 MindOpt 時，他們已在內部使用了一段時間，幫阿里雲節省了數億元成本。現在，求解器在阿里雲上每天被呼叫的次數以十億計。

過去兩年，杉數、阿里與 GUROBI 在線性規劃權威榜單 Mittlemann 測試上競爭激烈。在單純形法測試上，阿里與杉數輪流當第一，80% 的時間是杉數領先；而在內點法上，杉數一直穩居榜首。在線性規劃單純形法上，GUROBI 已經被擠到第三很久了。

但是在整數規劃這一最重要的求解器開發上，國內與美國還有著很大的差距。目前求解器軟體，國內只有 COPT 具備了求解大規模整數規劃問題的能力。“目前我們的 800 家使用者，79% 的問題來自整數規劃。雖然在榜上排名世界第二，但是實際上我們與三大廠都還有著不小差距。整數規劃能力的提升，難度是線性的幾十倍，是一個漫長的旅程。我們還需要持續艱苦的努力。”葛鼕鼕總結。

就製造業而言，求解器是最核心的軟體。比方說，國家電網的排程優化、無功優化、電力市場清算等等環節，背後有上千個求解器在不停地計算。杉數的線性規劃求解器 COPT 自誕生以來，已應用於能源、航空、製造、物流、零售等多個行業，合作的企業包括國網/南網、南航、華為、小米等大廠。

杉數與這些大廠的其中一項合作是排產排程。對於 ICT（資訊通訊技術）這類大廠，設想一下，工廠數量多，數百個工廠有上千個生產車間，用到的零部件大約有 10 萬多種。如果同時收到幾百個訂單，規定在未來的 20 周內完成，這時就需要全域性優化思想，避免造成資源浪費。

我們可以將這個問題建模成一個整數規劃問題，即使考慮其簡化形式線性規劃，變數與約束也都是上億級別，但求解器可以快速求解。談到求解器的變遷，葛鼕鼕感嘆，求解器的發展也很快，2009 年那會，求解器算一個百萬級別的線性規劃很吃力，但如今，上億級別的線性規劃只需一個小時的計算量。

“一開始大家覺得（上億級變數問題）只能用 GUROBI 算，我們也沒什麼信心。最後發現，我們不但能算出來，而且計算速度比 GUROBI 快了大概 30% 以上。”

不同領域的求解器在底層思想上有相通的地方。比如，現在華為就開始將 SAT 求解器中通行的衝突分析思想應用在整數規劃求解器中。

相對來說，線性規劃求解器在國內外的發展更成熟，而 SAT 求解器在國內做的人寥寥無幾，近些年來，只有蔡少偉團隊在做自己道路的 SAT 求解器。他們曾與華為合作，將 SAT 求解器用於華為晶片中的電路等價驗證，將 miter 電路轉為 SAT 問題，求解規模高達 5000 萬變數、1 億 5 千萬子句，但只用了 1 小時。

圖 / 用 SAT 求解器做電路等價驗證

工業 SAT 求解的挑戰主要是變數依賴與超大規模，前者需要系統搜尋，後者需要隨機搜尋。換言之，用於工業的 SAT 求解器，需要將系統搜尋與隨機搜尋相結合。這也是 Bart Sellman 命題邏輯推理與搜尋十大挑戰中的第七個挑戰。

蔡少偉從 2014 年開始研究混合搜尋求解器。此前，這方面的求解器有 ANC、WalkSatz 等等，但它們都是側重系統搜尋與區域性搜尋在求解能力上的互補，黑盒呼叫，在工業例項上的表現無法超越單一的系統搜尋方法。

他深入探索了系統搜尋和隨機搜尋的演算法行為以及在合作中的作用，經過近幾年的研究，放棄了走求解能力互補的道路，提出了以隨機區域性搜尋取樣，以系統搜尋求解，進行基於資訊互動的深度合作。

實驗結果顯示，與 2011 年到 2019 年 SAT 比賽的工業組冠軍與主賽道冠軍演算法相比，蔡少偉所設計的混合搜尋求解器比單搜尋求解器平均比每個 benchmark 多解約 30 個算例，且能求出許多系統搜尋與區域性搜尋均求不出來的例項（平均佔求解例項的 12%）。

圖 / 混合搜尋求解器 RelaxedNewTech 框架示意圖

這也是距 Bart Selman 在 1997 年提出十大挑戰以來，首次有人解決了第七大挑戰。蔡少偉團隊提出的鬆弛子句衝突學習方法也在 2020 年 SAT 比賽中獲得主賽道的冠軍；相關論文（“Deep Cooperation of CDCL and Local Search for SAT”）獲得 SAT 2021 最佳論文獎，這也是 SAT 會議自 1997 年設立以來，第一篇來自中國的工作獲得該獎。

在解決 EDA 等中國“卡脖子”問題中，SAT 求解的地位無異於人的命門。同時，一個不容忽略的現實是：無論是 SAT 求解器，還是數學規劃求解器（包括線性規劃），中國人才始終佔極少數。

不過，李初民很樂觀。他認為，中國研究 SAT 求解器的人一定會越來越多。

今年，他和德國形式化專家 Armin Biere，西班牙人工智慧專家 Felip Manya 等人發起、他的早年學生黃沖和華中科技大學呂志鵬參與組織 EDA 國際演算法競賽 EDA Challenge (www.eda-ai.org)，收到的求解器約有一半來自中國。

適千里者，三月聚糧

路漫漫其修遠兮。

如今，除了 SAT 求解，蔡少偉也開始研究 SMT（可滿足性模理論問題），SMT 公式可以看作是 SAT 與數學規劃等背景理論的結合，SMT 求解是更具挑戰的方向，國內更是無人問津；同樣地，葛鼕鼕與杉數的研究重心也從線性規劃求解轉到了整數規劃和非線性規劃求解。無論是從 SAT 到 SMT，還是從線性規劃到整數規劃，蔡少偉與葛鼕鼕所傳達的訊號是一致的：用求解器加速中國的工業發展。

從廣義上看，求解器的意義不僅僅在於工業的發展。葉蔭宇一直認為，國內應該形成一個將數學與程式碼相結合的研究生態，而開發求解器是一個很好的結合點。通過研究求解器，我們可以培養一大批既精通數學、又擅長程式設計的人才。

葛鼕鼕談道：“導師的想法是要鼓勵大家去研究求解器。所以後來，其他大廠或者高校做求解器，有時候遇到棘手的問題，跑來問我們。只要不涉及到核心機密，我們一般都會給他們義務解答。”

而李初民則提到，SAT 求解講究從衝突中學習變元之間的精確邏輯關係，機器學習是從大資料中學習資料的統計性質，兩者可以相互促進、相互補充，從而人工智慧更好地發展。機器學習中的一些問題（比如決策樹），也可以表述為 SAT 問題。

從這些優秀學者的經歷來看，我們不難發現，求解器是一項大工程：李初民從 1994 年開始研究，專注三年才開發出 Satz 求解器；蔡少偉從 2014 年挑戰系統搜尋與區域性搜尋相結合，直到 2020 年才算“拿下”這個問題；葛鼕鼕等人從 2015 年開始研究，只做求解器，用了 4 年才開發了他們的王牌 solver — COPT。

蔡少偉感嘆，求解器適合馬拉松型選手，“很巧的是，我以前讀書時參加百米短跑，總是壓著及格線過關。但如果是跑 5000 米，我往往就能跑得比較好。”

相比機器學習，求解器的熱度相形見絀。生於深度學習時代，無論是蔡少偉，還是葛鼕鼕，他們都沒有被外界的浪潮捲動，始終堅持自己最初的追求，以內因戰外因，做沒有深度學習的 AI 研究。

十年過去，他們成為了中國少數研究求解器的青年砥柱。如果沒有他們的堅持，我國求解器的研究也許仍是空白狀態。熱潮自有大眾追捧，但對人才本就稀缺的領域來說，一個人的堅持，很可能就決定了全域性的命運。