蔡少偉清晰地記得，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年所提出的命題邏輯推理與搜索十大挑戰之一：結合系統搜索與隨機搜索設計出比這兩種方法更高效的算法。在蔡少偉深入 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 研究。十年過去，他們成為了中國少數研究求解器的青年砥柱。如果沒有他們的堅持，我國求解器的研究也許仍是空白狀態。熱潮自有大眾追捧，但對人才本就稀缺的領域來說，一個人的堅持，很可能就決定了全局的命運。
作者注：人物/采訪、交流、爆料、抬杠，歡迎添加微信（302703941）。???????????????
雷鋒網雷鋒網雷鋒網
雷峰網原創文章，未經授權禁止轉載。詳情見轉載須知。
???????????????
