解決中國“卡脖子”問題：研究求解器的少數(shù)者

在人工智能時代，他們不做深度學(xué)習(xí)。

”

作者 | 陳彩嫻

編輯 | 岑峰

1

少數(shù)者

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

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

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

不過，蔡少偉似乎對這份“孤軍作戰(zhàn)”的寂寞也早已見慣不慣。當(dāng)時，他在北京大學(xué)計算機系的理論實驗室攻讀博士，師從蘇開樂，是當(dāng)時組里唯一一位研究 SAT 求解算法的人。作為數(shù)理邏輯基礎(chǔ)問題又是NP完全問題，SAT 求解同時注重符號推理與算法設(shè)計，還需要巧妙的數(shù)據(jù)結(jié)構(gòu)和精致的代碼實現(xiàn)，難度極高。

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

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

讀博期間，他師從運籌學(xué)泰斗、馮·諾依曼理論獎的唯一華人獲獎?wù)呷~蔭宇，主要研究大規(guī)模優(yōu)化理論與算法，并不直接研究求解器，只是在研究某些整數(shù)規(guī)劃的問題時經(jīng)常需要調(diào)用。但回國后，他卻發(fā)現(xiàn)，國內(nèi)居然沒有人開發(fā)商用求解器。凡是需要用到求解器的企業(yè)，都是直接購買美國的 CPLEX、GUROBI 與 XPRESS。

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

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

 圖 / 剛步入教職的葛冬冬 

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

事實上，在深度學(xué)習(xí)興起之前，人工智能十分注重邏輯推理（reasoning），當(dāng)時偏符號主義的 SAT 問題比深度學(xué)習(xí)還流行。

從“解題”的角度看，一切人工智能系統(tǒng)都可以歸結(jié)為“問題求解”（Problem Solving）系統(tǒng)，即為了實現(xiàn)給定目標(biāo)而展開的動作序列的過程。而解決特定問題的算法，被稱為“求解器”（solver）。無論是 SAT 求解器，還是整數(shù)規(guī)劃求解器，都是經(jīng)典的離散約束算法問題。

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

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

2

從 SAT = NP-Complete 談起

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

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

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

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

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

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

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

甲乙丙想?yún)渍f：乙參會我就參會，乙說：丙參會我就參會，而丙說：甲參會我就不參會，那么能不能同時滿足甲乙丙的參會需求？

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

比方說，在進行機場飛機調(diào)度時，研究人員要考慮的狀態(tài)非常多，包括待起飛的飛機數(shù)量，飛機分布的跑道數(shù)量與位置，飛機的運行方向，風(fēng)向等等。一個布爾變元表示單一時空下的一種狀態(tài)。由此可見，布爾變元所表達的信息非常小，只有 0 與 1 。如果要表達完全部有用信息，那么涉及到的變元數(shù)量可能是成千上萬億。

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

2006年，蔡少偉在本科班主任王家兵的帶領(lǐng)下首次接觸 SAT 問題。當(dāng)時，他正就讀于華南理工大學(xué)計算機科學(xué)與技術(shù)專業(yè)，剛上大二。王家兵對 SAT 問題很感興趣，見蔡少偉數(shù)學(xué)底子不錯，就讓他協(xié)助研究。為了完成這些工作，蔡少偉跑去圖書館查找資料，由此入門。

本科畢業(yè)后，蔡少偉直博北大。在確定研究方向時，蔡少偉先是摸索了一年，最后發(fā)現(xiàn)還是求解算法方向最有趣，就選擇繼續(xù)研究 SAT 求解器。

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

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

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

導(dǎo)師蘇開樂擅長的是邏輯系統(tǒng)，卻支持他選擇自己喜歡的求解算法研究。他是當(dāng)時實驗室里唯一做求解器的學(xué)生。在這種先天條件不足、后天支持有限的情況下，蔡少偉獨自探索，過程的艱難可想而知。

 圖 / 蔡少偉 

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

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

到了90年代，沖突分析子句學(xué)習(xí)（CDCL）方法與局部搜索方法出現(xiàn)。其中，CDCL在系統(tǒng)搜索算法中加入了沖突分析等關(guān)鍵技術(shù)，而局部搜索算法作為主要的啟發(fā)式算法為人所知。1992年，Bart Selman 提出的局部搜索算法 GSAT 在 N 皇后與圖著色等多個經(jīng)典問題上取得了比 DPLL 算法更好的效果，引起了人工智能領(lǐng)域啟發(fā)式搜索社群的興趣，期間出現(xiàn)各類局部搜索算法。而 CDCL 方法極大提高了 DPLL 算法的性能，使得 SAT 求解器的應(yīng)用得到推廣。

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

在蔡少偉讀博時，許多人都認(rèn)為，SAT 問題經(jīng)過多年的快速發(fā)展，已經(jīng)很難取得進一步的突破。比如，當(dāng)時他想解決的問題是局部搜索算法求解大規(guī)模SAT實例。但是，在他入場時，局部搜索已經(jīng)不被大多數(shù)人看好，處于被邊緣化的地位。

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

蔡少偉的口頭禪是，“做研究就是要有自己的 label（標(biāo)簽）?！?/span>

3

與巨人同行

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

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

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

 圖 / 李初民 

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

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

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

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

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

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

“就像今年奧運會的蘇炳添，在百米賽跑中兩次跑進 10 秒。雖然沒有拿金牌，但我們都知道他非常了不起，因為他每進步百分之一秒，都是難上加難?！崩畛趺裥稳?，“SAT問題的后繼研究者也是一樣?！?/span>

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

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

李初民有這方面的親身經(jīng)歷。2017年，他指導(dǎo)學(xué)生實現(xiàn)了一項子句精簡技術(shù)，非常有效，投到 IJCAI 后，有審稿專家就說，很多人都已經(jīng)實現(xiàn)過這個技術(shù)，因此論文沒有創(chuàng)新?！靶液糜幸粋€行家指出我們與別人的不同，論文才逃過了被‘槍斃’的命運?！焙髞?，憑借這項技術(shù)，他們獲得了當(dāng)年 SAT 競賽的金牌，這項技術(shù)與他們的實現(xiàn)方式也成為了SAT求解器的標(biāo)準(zhǔn)配置。

除了自己研究 SAT 求解器，李初民也樂于指導(dǎo)對SAT求解有興趣的年青人。

蔡少偉也許是李初民指導(dǎo)過的學(xué)生中，堅持研究 SAT 最久的學(xué)生。他從2009年正式開始 SAT 以及相關(guān)問題的算法研究，第一個成果是利用 SAT 求解的約束加權(quán)技術(shù)設(shè)計另一個經(jīng)典NP 難問題---最小頂點覆蓋問題的局部搜索算法，該算法 EWLS 在一個著名挑戰(zhàn)實例 frb100-40 上打破了當(dāng)時的世界紀(jì)錄。之后，他繼續(xù)深入局部搜索算法研究，嘗試解決其重要缺陷，即循環(huán)問題。

系統(tǒng)搜索與隨機（局部）搜索是SAT問題中的兩大方向。拿走地圖舉例，系統(tǒng)搜索是：走走剪剪，走到地圖的哪一塊，就將哪一塊剪掉，所以這張地圖會越走越小，最后走空了，就知道所有地方都走過了；而隨機搜索是：你在地圖上跑來跑去，但是你不記得你跑過哪些地方，沒有“剪枝能力”，無法剪掉，造成循環(huán)訪問的現(xiàn)象。

如果說 SAT 問題是計算機科學(xué)世界的大門，那么相變現(xiàn)象則是大門的鎖芯，因此相變區(qū)實例也成為 SAT 求解的熱門測試集。而隨機搜索是求解相變區(qū)實例的最有希望的方法，但對于大規(guī)模相變實例仍然有較大障礙。導(dǎo)致相變區(qū)難解的本質(zhì)原因，就是隨機搜索的循環(huán)現(xiàn)象。

針對這個問題，當(dāng)時已有的解決方法主要是馮·諾依曼獎獲得者 Fred Glover 在1998年提出的禁忌搜索策略（tabu search）與荷蘭萊頓大學(xué)教授 Holger Hoos 在2002年提出的隨機擾動方法。但是，它們沒有利用問題結(jié)構(gòu)，無法針對問題結(jié)構(gòu)做出調(diào)整，且?guī)в袇?shù)，在使用的時候常常需要大量的調(diào)參工作。

所以，蔡少偉思考如何克服隨機搜索中的循環(huán)缺陷，希望設(shè)計出一種兩全其美的方法，既能保留隨機搜索的優(yōu)勢，又能克服其循環(huán)搜索的缺陷。但這并不簡單，蔡少偉苦苦思索，停滯數(shù)月，毫無進展。心情自然十分郁悶。

那段時間，他讀了許多無關(guān)本領(lǐng)域的書，尤其是博弈論與社會學(xué)。其中，許多篇章談到個體與群體的關(guān)系。帶著“如何克服循環(huán)缺陷”的問題，蔡少偉雖然是閱讀課外書籍，卻時時忍不住將這個問題與書中的章節(jié)內(nèi)容聯(lián)系起來，讀著讀著，突然冒出一個想法：可以利用環(huán)境信息減輕循環(huán)！

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

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

格局檢測的核心是：如果變量的環(huán)境信息沒有改變，則不允許改變?nèi)≈?，而環(huán)境信息可以是由該變量的鄰居變量的取值構(gòu)成，也可以由該變量的關(guān)聯(lián)子句的狀態(tài)構(gòu)成。通過避免局部結(jié)構(gòu)循環(huán)，減輕搜索的循環(huán)現(xiàn)象。利用問題的結(jié)構(gòu)信息，不僅可以避免循環(huán)現(xiàn)象，還能通過設(shè)置多層評分函數(shù)克服“短視”。

 圖 / 格局檢測策略示意圖 

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

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

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

2011年年底，他開始著手準(zhǔn)備，雖然算法在當(dāng)時已達到國際前沿，但并沒有太大的把握。過完寒假回校，他一邊忙畢業(yè)的事，一邊備戰(zhàn) SAT 比賽。有兩位師弟幫忙，研究進度加快不少，“開始只是小優(yōu)化，如隔靴搔癢，一直到比賽截止兩個禮拜前才有了質(zhì)的飛躍?！?/span>

果然，比賽結(jié)果公布，三條主賽道，蔡少偉組的算法（CCSat）贏得了隨機組（測試集為相變區(qū)實例）的第一名，并且遙遙領(lǐng)先于第二名，求解效率比是 423（70.5%）vs 321（53.5%）。

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

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

蔡少偉的算法以明顯優(yōu)勢奪冠，在當(dāng)時的學(xué)術(shù)界也引起了較大反響。

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

2012年從北大博士畢業(yè)后，蔡少偉繼續(xù)在SAT求解器上鉆研。他用兩年時間從澳大利亞格里菲斯大學(xué)獲得應(yīng)用數(shù)學(xué)博士學(xué)位，2014年回國加盟中科院軟件研究所，開始挑戰(zhàn)康奈爾大學(xué)計算機系教授 Bart Sellman 等人在1997年所提出的命題邏輯推理與搜索十大挑戰(zhàn)之一：結(jié)合系統(tǒng)搜索與隨機搜索設(shè)計出比這兩種方法更高效的算法。

4

與巨人同行（2）

在蔡少偉深入 SAT 求解研究的同時，時任上海財經(jīng)大學(xué)交叉科學(xué)研究院院長的葛冬冬開始琢磨線性規(guī)劃求解器的開發(fā)。

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

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

 圖 / SAT與混合整數(shù)規(guī)劃（MIP）、約束整數(shù)規(guī)劃（CIP）及約束規(guī)劃（CP）的關(guān)系 

葛冬冬是運籌學(xué)出身。運籌學(xué)研究問題主要分兩步，第一步是建模，第二步是求解：將現(xiàn)實中的問題通過算法建成標(biāo)準(zhǔn)的數(shù)學(xué)模型（如線性不等式）后，再對數(shù)學(xué)模型進行求解，從而解決現(xiàn)實問題。如果變量少，只有x與y，那么我們可以進行手算；但當(dāng)數(shù)學(xué)模型涉及到幾百萬變量，則必須借助軟件（如matlab）來自動計算。

本質(zhì)上，求解器就是一個專業(yè)的數(shù)學(xué)/計算軟件，用于實現(xiàn)復(fù)雜的數(shù)學(xué)算法。當(dāng)軟件對線性方程組求解時，該軟件可以稱為“線性方程組的求解器”。計算機歷史上最早的求解器，就是線性規(guī)劃求解器。

葛冬冬對求解器有所耳聞，要追溯到他在斯坦福讀博的師門關(guān)系：

1947年，“線性規(guī)劃之父”、斯坦福大學(xué)教授 George Dantzig （葛冬冬的師爺）提出了第一個用于優(yōu)化線性系統(tǒng)的算法，叫“單純形法”（Simplex Method），第一次使大規(guī)模優(yōu)化問題得到求解。單純形法一直雄踞二十世紀(jì)最偉大的算法前五之列。30年后，隨著計算機技術(shù)的發(fā)展，人們又開始嘗試用計算機開發(fā)求解軟件。1979年，第一個求解器軟件在美國誕生，名為 LINGO。

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

1980年代，美國又有多位學(xué)者提出了內(nèi)點法（Interior-Point algorithm）。此前，線性系統(tǒng)優(yōu)化一直是單純形法的天下，直到內(nèi)點法出現(xiàn)。內(nèi)點法在某些問題上比單純形法的求解速度更快，可以處理許多非線性規(guī)劃問題，從而成為新的潮流，并也被用于商用求解器的開發(fā)。George Dantzig 的得意門生葉蔭宇（葛冬冬的導(dǎo)師）也是公認(rèn)的內(nèi)點法奠基者之一，因此獲得了運籌學(xué)的最高獎——馮·諾依曼理論獎。

 圖 / 葉蔭宇 

歷史上線性規(guī)劃求解的兩大流派，都是由葛冬冬的師長創(chuàng)立。因此，讀博期間，他也跟著學(xué)習(xí)、琢磨了很多線性規(guī)劃求解實例。

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

毫無疑問，求解器的開發(fā)是一個大規(guī)模系統(tǒng)工程，動輒上百萬行代碼。此外，求解器軟件對開發(fā)人員的數(shù)學(xué)能力要求特別高，而中國的情況是：同時精通數(shù)學(xué)與大規(guī)模軟件開發(fā)能力的人幾乎不存在。這一點與美國形成鮮明的對比，美國學(xué)生通常是一邊思考數(shù)學(xué)問題，一邊思考如何用代碼復(fù)現(xiàn)問題。

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

“不重視形式邏輯，也許是科學(xué)在中國發(fā)展緩慢的原因之一，因為科學(xué)需要大量的邏輯推理?！崩畛趺裾劦馈?/span>

此外，研究求解器不容易發(fā)論文。研究求解器的老員工常說一句話：“求解器的秘密就在于它沒有秘密?！本褪钦f，求解器中的數(shù)學(xué)問題與實現(xiàn)算法都能在數(shù)學(xué)論文中找到，但不同求解器寫出來的代碼質(zhì)量良莠不齊。一方面，這要考驗人的系統(tǒng)開發(fā)與數(shù)學(xué)結(jié)合能力；另一方面，需要花費許多時間與精力去做大量的嘗試，俗稱“踩坑”。

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

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

從2013年加入上海財經(jīng)大學(xué)后，葛冬冬便開始有意識地招收一些擅長做優(yōu)化算法的年青人。那時，他有些猶豫：“求解器這事究竟能不能做？”心里沒底，跑去咨詢導(dǎo)師，葉老師很支持，說：“中國總得要自己的求解器，不要老覺得做不成，總得有人挑頭。”

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

最初，他們是從上海財大的交叉科學(xué)院調(diào)配人手，加上杉數(shù)科技的創(chuàng)始團隊，從零開始探索做一個開源求解器。葛冬冬與創(chuàng)始團隊自學(xué)、找專家、找導(dǎo)師，花了很多力氣琢磨求解器開發(fā)，比如單純形法與內(nèi)點法如何在軟件開發(fā)上走通全流程，弄清楚求解器開發(fā)的核心部件，矩陣數(shù)據(jù)簡化等等。

期間，葉蔭宇給了許多指導(dǎo)，甚至親自下場幫他們寫開源代碼。

經(jīng)過兩年的摸索，他們在2017年發(fā)布了中國第一個開源優(yōu)化求解器 LEAVES，但性能并不突出。這使他們意識到，開發(fā)求解器是一個很大的系統(tǒng)工程，光靠學(xué)校的力量、投入小的成本是做不成的。所以，杉數(shù)開始在國際上秘密尋求有經(jīng)驗的人，組建團隊。

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

 圖 / 葛冬冬在杉數(shù)科技擔(dān)任首席科學(xué)官 

幸運的是，他們最終在XPRESS找到了一個志同道合的中國人，本科就讀于北航計算機系，畢業(yè)后去英國讀博，博士期間的內(nèi)容就是研發(fā)求解器。之后，他們又陸陸續(xù)續(xù)從CPLEX、XPRESS與LINGO等處挖到了多個程序員。

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

又過了兩年，2019年5月，杉數(shù)推出中國首個商用線性規(guī)劃求解器COPT。COPT的出現(xiàn)，給國內(nèi)大廠傳遞了一個重要信息：開發(fā)求解器的難度確實極高，但也不是全無可能。

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

5

求解器在中國

與歐美數(shù)十年前就將求解器用于航空、鐵路交通規(guī)劃不同，工業(yè)求解器在中國的落地歷史很短，最早可以追溯到2000年代初期，寶鋼采用 ILOG CPLEX 優(yōu)化生產(chǎn)規(guī)劃系統(tǒng)。

在COPT出現(xiàn)之前，商業(yè)求解器三大廠 CPLEX、GUROBI 與 XPRESS 憑借豐富的商業(yè)開發(fā)經(jīng)驗，以及較好的性能，在國際市場上占了超過90%的份額。

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

 圖 / Robert E. Bixby 

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

與此同時，英國愛丁堡的Dash Optimization團隊在1983年開發(fā)了 XPRESS，1986 年開始應(yīng)用于混合整數(shù)規(guī)劃求解。該團隊的開發(fā)人員大約有10人，一直相對穩(wěn)定。2008年，XPRESS 由美國金融信用商 FICO 收購，將求解器用于制定金融場景的大規(guī)模優(yōu)化方案。收購后，F(xiàn)ICO 不做過多干涉，XPRESS 的開發(fā)團隊繼續(xù)留在英國，保持了自身的競爭力，在市場上占有一定份額。

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

近兩年，華為與阿里也開始布局求解器開發(fā)。華為開發(fā)求解器，主要用于EDA設(shè)計、供應(yīng)鏈規(guī)劃等，而阿里做求解器，則主要用于阿里云的資源調(diào)度優(yōu)化。

阿里也是從線性規(guī)劃入手，先做單純形法，再做內(nèi)點法。2020年，阿里達摩院決策智能實驗室發(fā)布數(shù)學(xué)規(guī)劃求解器 MindOpt。根據(jù)阿里的官方說法，在發(fā)布 MindOpt 時，他們已在內(nèi)部使用了一段時間，幫阿里云節(jié)省了數(shù)億元成本?，F(xiàn)在，求解器在阿里云上每天被調(diào)用的次數(shù)以十億計。

過去兩年，杉數(shù)、阿里與GUROBI在線性規(guī)劃權(quán)威榜單 Mittlemann 測試上競爭激烈。在單純形法測試上，阿里與杉數(shù)輪流當(dāng)?shù)谝唬?0%的時間是杉數(shù)領(lǐng)先；而在內(nèi)點法上，杉數(shù)一直穩(wěn)居榜首。在線性規(guī)劃單純形法上，GUROBI 已經(jīng)被擠到第三很久了。

但是在整數(shù)規(guī)劃這一最重要的求解器開發(fā)上，國內(nèi)與美國還有著很大的差距。目前求解器軟件，國內(nèi)只有COPT具備了求解大規(guī)模整數(shù)規(guī)劃問題的能力。“目前我們的800家用戶，79%的問題來自整數(shù)規(guī)劃。雖然在榜上排名世界第二，但是實際上我們與三大廠都還有著不小差距。整數(shù)規(guī)劃能力的提升，難度是線性的幾十倍，是一個漫長的旅程。我們還需要持續(xù)艱苦的努力?！备鸲偨Y(jié)。

就制造業(yè)而言，求解器是最核心的軟件。比方說，國家電網(wǎng)的調(diào)度優(yōu)化、無功優(yōu)化、電力市場清算等等環(huán)節(jié)，背后有上千個求解器在不停地計算。杉數(shù)的線性規(guī)劃求解器 COPT 自誕生以來，已應(yīng)用于能源、航空、制造、物流、零售等多個行業(yè)，合作的企業(yè)包括國網(wǎng)/南網(wǎng)、南航、華為、小米等大廠。

杉數(shù)與這些大廠的其中一項合作是排產(chǎn)排程。對于 ICT（信息通信技術(shù)）這類大廠，設(shè)想一下，工廠數(shù)量多，數(shù)百個工廠有上千個生產(chǎn)車間，用到的零部件大約有10萬多種。如果同時收到幾百個訂單，規(guī)定在未來的20周內(nèi)完成，這時就需要全局優(yōu)化思想，避免造成資源浪費。

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

“一開始大家覺得（上億級變量問題）只能用 GUROBI 算，我們也沒什么信心。最后發(fā)現(xiàn)，我們不但能算出來，而且計算速度比 GUROBI 快了大概 30% 以上。”

不同領(lǐng)域的求解器在底層思想上有相通的地方。比如，現(xiàn)在華為就開始將SAT求解器中通行的沖突分析思想應(yīng)用在整數(shù)規(guī)劃求解器中。

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

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

工業(yè) SAT 求解的挑戰(zhàn)主要是變量依賴與超大規(guī)模，前者需要系統(tǒng)搜索，后者需要隨機搜索。換言之，用于工業(yè)的SAT求解器，需要將系統(tǒng)搜索與隨機搜索相結(jié)合。這也是 Bart Sellman 命題邏輯推理與搜索十大挑戰(zhàn)中的第七個挑戰(zhàn)。

蔡少偉從2014年開始研究混合搜索求解器。此前，這方面的求解器有 ANC、WalkSatz 等等，但它們都是側(cè)重系統(tǒng)搜索與局部搜索在求解能力上的互補，黑盒調(diào)用，在工業(yè)實例上的表現(xiàn)無法超越單一的系統(tǒng)搜索方法。

他深入探索了系統(tǒng)搜索和隨機搜索的算法行為以及在合作中的作用，經(jīng)過近幾年的研究，放棄了走求解能力互補的道路，提出了以隨機局部搜索采樣，以系統(tǒng)搜索求解，進行基于信息交互的深度合作。

實驗結(jié)果顯示，與 2011 年到 2019 年 SAT 比賽的工業(yè)組冠軍與主賽道冠軍算法相比，蔡少偉所設(shè)計的混合搜索求解器比單搜索求解器平均比每個benchmark多解約30個算例，且能求出許多系統(tǒng)搜索與局部搜索均求不出來的實例（平均占求解實例的12%）。

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

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

在解決 EDA 等中國“卡脖子”問題中，SAT 求解的地位無異于人的命門。同時，一個不容忽略的現(xiàn)實是：無論是 SAT 求解器，還是數(shù)學(xué)規(guī)劃求解器（包括線性規(guī)劃），中國人才始終占極少數(shù)。

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

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

6

適千里者，三月聚糧

路漫漫其修遠兮。

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

從廣義上看，求解器的意義不僅僅在于工業(yè)的發(fā)展。葉蔭宇一直認(rèn)為，國內(nèi)應(yīng)該形成一個將數(shù)學(xué)與代碼相結(jié)合的研究生態(tài)，而開發(fā)求解器是一個很好的結(jié)合點。通過研究求解器，我們可以培養(yǎng)一大批既精通數(shù)學(xué)、又擅長編程的人才。

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

而李初民則提到，SAT求解講究從沖突中學(xué)習(xí)變元之間的精確邏輯關(guān)系，機器學(xué)習(xí)是從大數(shù)據(jù)中學(xué)習(xí)數(shù)據(jù)的統(tǒng)計性質(zhì)，兩者可以相互促進、相互補充，從而人工智能更好地發(fā)展。機器學(xué)習(xí)中的一些問題（比如決策樹），也可以表述為SAT問題。

從這些優(yōu)秀學(xué)者的經(jīng)歷來看，我們不難發(fā)現(xiàn)，求解器是一項大工程：李初民從1994年開始研究，專注三年才開發(fā)出 Satz 求解器；蔡少偉從2014年挑戰(zhàn)系統(tǒng)搜索與局部搜索相結(jié)合，直到2020年才算“拿下”這個問題；葛冬冬等人從2015年開始研究，只做求解器，用了4年才開發(fā)了他們的王牌solver — COPT。

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

相比機器學(xué)習(xí)，求解器的熱度相形見絀。生于深度學(xué)習(xí)時代，無論是蔡少偉，還是葛冬冬，他們都沒有被外界的浪潮卷動，始終堅持自己最初的追求，以內(nèi)因戰(zhàn)外因，做沒有深度學(xué)習(xí)的 AI 研究。

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

致敬！

本文由雷鋒網(wǎng)原創(chuàng)，作者：陳彩嫻。李揚霞對本文亦有貢獻。申請授權(quán)請回復(fù)“轉(zhuǎn)載”，未經(jīng)授權(quán)不得轉(zhuǎn)載。

END

推薦閱讀

谷歌健康「分拆」內(nèi)幕：憋屈的CEO、傲慢的Jeff Dean、狂熱的AI信徒

教培已死，硬件方生

AI 商業(yè)模式的脫靶、崩塌、救贖