導(dǎo)語：在人工智能時(shí)代，他們不做深度學(xué)習(xí)。
蔡少偉清晰地記得，2011年夏天他去美國(guó)密歇根大學(xué)安娜堡分校參加 SAT 會(huì)議時(shí)，一眼望去，全場(chǎng)只有他一個(gè)中國(guó)人。
參會(huì)人員一半來自歐洲，四分之一來自北美（尤其是美國(guó)），另外四分之一則來自亞太地區(qū)。他將自己的“單刀赴會(huì)”列為 SAT 2011一行的兩大記憶點(diǎn)之一，另一點(diǎn)是那年大會(huì)主席的論文被 SAT 評(píng)委“槍斃”了。
這是蔡少偉第一次參加 SAT。這個(gè)被 CCF 列為 B 類的會(huì)議全稱為“International Conference on Theory and Applications of Satisfiability Testing”（可滿足性判定的理論與應(yīng)用國(guó)際會(huì)議），始設(shè)于1997年，主要面向研究可滿足性問題，尤其是布爾可滿足性（Boolean Satisfiability Problem，簡(jiǎn)稱“SAT”）問題的科研人員，向來少為中國(guó)學(xué)者問津。
不過，蔡少偉似乎對(duì)這份“孤軍作戰(zhàn)”的寂寞也早已見慣不慣。當(dāng)時(shí)，他在北京大學(xué)計(jì)算機(jī)系的理論實(shí)驗(yàn)室攻讀博士，師從蘇開樂，是當(dāng)時(shí)組里唯一一位研究 SAT 求解算法的人。作為數(shù)理邏輯基礎(chǔ)問題又是NP完全問題，SAT 求解同時(shí)注重符號(hào)推理與算法設(shè)計(jì)，還需要巧妙的數(shù)據(jù)結(jié)構(gòu)和精致的代碼實(shí)現(xiàn)，難度極高。
圖 / 蔡少偉（左）參加 SAT 2011 時(shí)，遇到同是研究隨機(jī)局部搜索的德國(guó)烏爾姆大學(xué)博士生Adrian Balint（右），討論不過癮，決定直接上機(jī)器 PK 同樣經(jīng)歷過“四下無人”的少數(shù)者，還有 2009 年從斯坦福畢業(yè)回國(guó)的葛冬冬。那一年，他從斯坦福大學(xué)管理科學(xué)與工程系（MS&E）取得運(yùn)籌學(xué)博士學(xué)位，拿到了上海交通大學(xué)的教職 offer，準(zhǔn)備回國(guó)任教。
讀博期間，他師從運(yùn)籌學(xué)泰斗、馮·諾依曼理論獎(jiǎng)的唯一華人獲獎(jiǎng)?wù)呷~蔭宇，主要研究大規(guī)模優(yōu)化理論與算法，并不直接研究求解器，只是在研究某些整數(shù)規(guī)劃的問題時(shí)經(jīng)常需要調(diào)用。但回國(guó)后，他卻發(fā)現(xiàn)，國(guó)內(nèi)居然沒有人開發(fā)商用求解器。凡是需要用到求解器的企業(yè)，都是直接購買美國(guó)的 CPLEX、GUROBI 與 XPRESS。
“求解器分為專業(yè)版、個(gè)人版與商用版，不同版本有不同的價(jià)格，5萬到40萬人民幣不等?！备?/span>冬冬談道，“中國(guó)沒有求解器，要從國(guó)外買，人家不可能給你降低價(jià)格。如果買幾千臺(tái)的話，幾個(gè)億的外匯就這樣出去了?！?/span>
看到國(guó)內(nèi)在求解器研究上的空白，葛冬冬感到很奇怪：為什么沒有人做？但那時(shí)，他剛步入教職不久，身兼數(shù)職，也沒有條件去作更多的研究。直到2013年，他從交大轉(zhuǎn)到上海財(cái)經(jīng)大學(xué)、擔(dān)任交叉科學(xué)研究院院長(zhǎng)，有機(jī)會(huì)組建自己的團(tuán)隊(duì)，才開始帶隊(duì)探索。
十年過去，再回頭看，從無人區(qū)走出來的蔡少偉與葛冬冬，都已成為國(guó)內(nèi)研究求解器的青年先驅(qū)人物。但是，談起求解器的研究現(xiàn)狀，他們的結(jié)論仍與十年前無異，“就一小撮人”。
事實(shí)上，在深度學(xué)習(xí)興起之前，人工智能十分注重邏輯推理（reasoning），當(dāng)時(shí)偏符號(hào)主義的 SAT 問題比深度學(xué)習(xí)還流行。
從“解題”的角度看，一切人工智能系統(tǒng)都可以歸結(jié)為“問題求解”（Problem Solving）系統(tǒng)，即為了實(shí)現(xiàn)給定目標(biāo)而展開的動(dòng)作序列的過程。而解決特定問題的算法，被稱為“求解器”（solver）。無論是 SAT 求解器，還是整數(shù)規(guī)劃求解器，都是經(jīng)典的離散約束算法問題。
求解器在工業(yè)發(fā)展中的意義非凡。例如，中國(guó)戰(zhàn)略布局上亟待解決的“卡脖子”難題 EDA （電子設(shè)計(jì)自動(dòng)化）需要用到 SAT 求解器進(jìn)行快速驗(yàn)證，而制造、物流與供應(yīng)鏈優(yōu)化等則需要用到整數(shù)規(guī)劃求解器（尤其是線性規(guī)劃求解器）。因此，近兩年，華為與阿里也開始布局求解器研究。
江湖傳聞，華為內(nèi)部對(duì)求解器研究十分重視，多個(gè)海內(nèi)外團(tuán)隊(duì)同時(shí)推進(jìn)，任總直接聽取匯報(bào)。由于人才供給緊缺，蔡少偉所培養(yǎng)的博士畢業(yè)生入職華為后，待遇直接對(duì)標(biāo)“華為天才少年”，年薪近百萬。
（二）從 SAT = NP-Complete 談起
探討 SAT 求解器之前，我們首先要了解 SAT 問題的研究歷史。
說來牛叉，SAT 問題是計(jì)算機(jī)歷史上第一個(gè)被證明為 NP-Complete 的問題，其主要貢獻(xiàn)者就是計(jì)算復(fù)雜理論研究方向的大神、現(xiàn)任多倫多大學(xué)計(jì)算機(jī)系與數(shù)學(xué)系的教授 Stephen A. Cook。
圖 / 1982 年圖靈獎(jiǎng)獲得者 Stephen Cook 在1971年的論文“The Complexity of Theorem Proving Procedures”中，Stephen Cook 提出了著名的庫克定理（Cook Theorem），從圖靈機(jī)的角度證明所有 NP 問題都可以快速轉(zhuǎn)化為 SAT 問題。
在庫克定理里，圖靈機(jī)的計(jì)算過程可以用 SAT 表達(dá)出來，轉(zhuǎn)化成一條條獨(dú)立的語句，十分簡(jiǎn)單，但又極高效。庫克定理指出，如果 SAT 問題可以快速求解，那么所有 NP 問題都可以快速求解。Cook 本人也因此獲得 1982 年圖靈獎(jiǎng)。
廣義上，可滿足性（Satisfiability）問題是指對(duì)給定邏輯公式判定是否可滿足的問題。SAT問題特指“布爾可滿足性問題”，又稱“命題邏輯可滿足性問題”。命題邏輯是形式邏輯最基本的類別，基本元素是布爾變?cè)?。每個(gè)布爾變?cè)硪粋€(gè)基本命題。SAT 問題的本質(zhì)，是探求一大堆布爾變?cè)g的邏輯推理關(guān)系是否成立。
聽起來很高深，但描述十分簡(jiǎn)單。舉個(gè)例子：
甲乙丙想?yún)?huì)，甲說：乙參會(huì)我就參會(huì)，乙說：丙參會(huì)我就參會(huì)，而丙說：甲參會(huì)我就不參會(huì)，那么能不能同時(shí)滿足甲乙丙的參會(huì)需求？
這就是一個(gè) SAT 問題，而求解的答案是：他們的需求是不可（同時(shí)）滿足的。如果命題簡(jiǎn)單，那么人腦可以很快判定邏輯推理關(guān)系是否成立。但隨著布爾變?cè)图s束的條件越來越多，SAT 的求解就會(huì)越來越難，需要借助算法來進(jìn)行推理與計(jì)算。
比方說，在進(jìn)行機(jī)場(chǎng)飛機(jī)調(diào)度時(shí)，研究人員要考慮的狀態(tài)非常多，包括待起飛的飛機(jī)數(shù)量，飛機(jī)分布的跑道數(shù)量與位置，飛機(jī)的運(yùn)行方向，風(fēng)向等等。一個(gè)布爾變?cè)硎締我粫r(shí)空下的一種狀態(tài)。由此可見，布爾變?cè)磉_(dá)的信息非常小，只有 0 與 1 。如果要表達(dá)完全部有用信息，那么涉及到的變?cè)獢?shù)量可能是成千上萬億。
這種“描述起來十分簡(jiǎn)單、卻可以延伸出深入研究”的問題個(gè)性十分吸引蔡少偉。
2006年，蔡少偉在本科班主任王家兵的帶領(lǐng)下首次接觸 SAT 問題。當(dāng)時(shí)，他正就讀于華南理工大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)專業(yè)，剛上大二。王家兵對(duì) SAT 問題很感興趣，見蔡少偉數(shù)學(xué)底子不錯(cuò)，就讓他協(xié)助研究。為了完成這些工作，蔡少偉跑去圖書館查找資料，由此入門。
本科畢業(yè)后，蔡少偉直博北大。在確定研究方向時(shí)，蔡少偉先是摸索了一年，最后發(fā)現(xiàn)還是求解算法方向最有趣，就選擇繼續(xù)研究 SAT 求解器。
從接觸 SAT 問題開始，他就知道這是一塊“硬骨頭”。
首先，國(guó)內(nèi)研究 SAT 的學(xué)者少，知識(shí)傳承不足。上世紀(jì)90年代，雖然國(guó)內(nèi)也有研究 SAT 問題的學(xué)者，比如北航的李未院士，華中科技大學(xué)的黃文奇教授，還有中科院軟件研究所的張健研究員。蔡少偉入門 SAT 所讀的第一本著作，就是張健的《邏輯公式的可滿足性判定——方法、工具及應(yīng)用》。但是，這些研究都沒有形成一個(gè)派系。
其次，研究 SAT求解器需要扎實(shí)的數(shù)學(xué)基礎(chǔ)，且對(duì)算法設(shè)計(jì)和工程實(shí)現(xiàn)的能力要求極高，往往需要投入數(shù)年努力才有論文產(chǎn)出，對(duì)研究人員的心智與耐力都是一種考驗(yàn)。蔡少偉自問，雖然自己熱愛數(shù)學(xué)與算法，但并不擅長(zhǎng)，也無天賦。
導(dǎo)師蘇開樂擅長(zhǎng)的是邏輯系統(tǒng)，卻支持他選擇自己喜歡的求解算法研究。他是當(dāng)時(shí)實(shí)驗(yàn)室里唯一做求解器的學(xué)生。在這種先天條件不足、后天支持有限的情況下，蔡少偉獨(dú)自探索，過程的艱難可想而知。
他回憶，當(dāng)時(shí)研究 SAT，最大的困難是沒有足夠的機(jī)器。研究求解器要做大量實(shí)驗(yàn)，而他只有一個(gè)非常普通的筆記本。由于沒日沒夜地跑實(shí)驗(yàn)，這個(gè)筆記本后來還被燒壞了。無奈之下，他只有求助室友，借對(duì)方實(shí)驗(yàn)室的服務(wù)器來跑實(shí)驗(yàn)?！安贿^，這對(duì)現(xiàn)在的學(xué)生來說已經(jīng)不是難題，因?yàn)楝F(xiàn)在的計(jì)算資源比當(dāng)時(shí)先進(jìn)多了?！辈躺賯フ劦馈?/span>
早在上世紀(jì)60年代，SAT問題就有了第一個(gè)求解算法，叫“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 皇后與圖著色等多個(gè)經(jīng)典問題上取得了比 DPLL 算法更好的效果，引起了人工智能領(lǐng)域啟發(fā)式搜索社群的興趣，期間出現(xiàn)各類局部搜索算法。而 CDCL 方法極大提高了 DPLL 算法的性能，使得 SAT 求解器的應(yīng)用得到推廣。
此外，研究人員開始對(duì)隨機(jī) k-SAT 問題產(chǎn)生興趣，在相變現(xiàn)象研究與相變區(qū)隨機(jī) k-SAT 的算法研究上取得了許多成果，包括 Alfredo Braunstein 等人在2002年提出的基于統(tǒng)計(jì)物理的調(diào)查傳播（Survey Propagation）方法。在中國(guó)，北航的許可教授是深入研究相變現(xiàn)象的研究者之一。但 2010 年前后，SAT 求解的進(jìn)展近乎停滯。
在蔡少偉讀博時(shí)，許多人都認(rèn)為，SAT 問題經(jīng)過多年的快速發(fā)展，已經(jīng)很難取得進(jìn)一步的突破。比如，當(dāng)時(shí)他想解決的問題是局部搜索算法求解大規(guī)模SAT實(shí)例。但是，在他入場(chǎng)時(shí)，局部搜索已經(jīng)不被大多數(shù)人看好，處于被邊緣化的地位。
明知山有虎，偏向虎山行。還是一座付出與回報(bào)不成正比的土頭山。問蔡少偉，當(dāng)時(shí)研究的課題遇上關(guān)卡、停滯幾個(gè)月時(shí)，是否想過換方向，揀一個(gè)比較容易的題做。他說，那時(shí)候自己就是“執(zhí)迷不悟”，不愿意跟在別人的屁股后做研究，覺得沒意思。
蔡少偉的口頭禪是，“做研究就是要有自己的 label（標(biāo)簽）?！?/span>
所謂開辟，往往離不開前人鋪就的奠基石。
雖然蔡少偉與導(dǎo)師蘇開樂的研究方向不同，他只能靠自己摸索，但在蘇開樂的帶領(lǐng)下，他有幸結(jié)識(shí)了一群研究 SAT 問題的前輩，比如法國(guó)儒爾-凡爾納大學(xué)（University of Picardie Jules Verne）計(jì)算機(jī)系的華人教授李初民。
李初民從 1994 年開始研究 SAT 問題，是最早研究 SAT 問題的華人學(xué)者之一。他是華中工學(xué)院（現(xiàn)華中科技大學(xué)）計(jì)算機(jī)軟件專業(yè)的第一屆畢業(yè)生，1983年取得學(xué)士學(xué)位，后赴法國(guó)留學(xué)，分別于1985年和1990年在貢比涅大學(xué)（University of Technology of Compiegne）計(jì)算機(jī)系取得了碩士與博士學(xué)位。
圖 / 李初民
博士畢業(yè)后，李初民留在法國(guó)任教。他入門 SAT，是因?yàn)樵谏稀犊捎?jì)算性》這門課時(shí)，需要用圖靈機(jī)進(jìn)行計(jì)算，上課過程中，他發(fā)現(xiàn) SAT 求解器就像一把萬能的鑰匙，只要解決 SAT 問題，其他許多問題也可以快速求解，于是開始研究 SAT。
有句話說，“始于外貌，陷于才華，忠于人品?！边@很符合 SAT 研究者的心路歷程。李初民也一樣，他被 SAT 問題吸引的原因與蔡少偉相似，“（SAT）看起來很簡(jiǎn)單，非常容易上手，卻有著極強(qiáng)大的表達(dá)能力，可以很方便地用它來表達(dá)其他問題，比如圖染色問題?！?/span>
如李初民介紹，SAT的本質(zhì)是形式邏輯，表面看上去很簡(jiǎn)單，但豐富的信息量都隱藏在一條條語句中。既純粹，又神秘。所以，從入門 SAT 后，李初民就一心撲在了 SAT 問題的求解上。
在上世紀(jì)90年代所涌現(xiàn)的一大批算法中，李初民與 Anbulag 在1997年所提出的 SATZ 求解器（發(fā)表在 IJCAI 1997）受到了極大關(guān)注，相關(guān)論文被引用了超過 500 次。直到今天，SATZ 也是求解隨機(jī) SAT 問題最好的求解器之一。
李初民教授在 SAT 求解器的研究上堅(jiān)持了二十多年，在這個(gè)領(lǐng)域并不常見。許多人都曾為 SAT 問題著迷，但最終能堅(jiān)持下來的人卻很少，主要的原因就在于：要在 SAT 問題上取得新的成果很難。
從上世紀(jì) 60 年代至今，SAT 問題的研究已經(jīng)持續(xù)了大半個(gè)世紀(jì)，傳統(tǒng)的、簡(jiǎn)單的算法都已經(jīng)有許多外國(guó)學(xué)者試過。在這種相對(duì)成熟的領(lǐng)域去做研究，就是前人已經(jīng)搭了萬丈高樓，你首先要花很長(zhǎng)時(shí)間搭一條足夠長(zhǎng)的梯子，了解前人已經(jīng)研究過的知識(shí)，然后伸長(zhǎng)手臂，站在高高的梯子上，用力往萬丈高樓上丟一顆小小的石子。
“就像今年奧運(yùn)會(huì)的蘇炳添，在百米賽跑中兩次跑進(jìn) 10 秒。雖然沒有拿金牌，但我們都知道他非常了不起，因?yàn)樗窟M(jìn)步百分之一秒，都是難上加難?！崩畛趺裥稳?，“SAT問題的后繼研究者也是一樣?！?/span>
圖 / 蘇炳添在2021年東京奧運(yùn)會(huì)中跑進(jìn)10秒
除了開辟的艱辛，李初民認(rèn)為，研究 SAT 求解的難點(diǎn)還在于，具有實(shí)際意義的 SAT 求解技術(shù)通常很簡(jiǎn)單，主要通過大量繁重的實(shí)驗(yàn)來支撐，因此寫出來的論文看起來并不高深，投到頂會(huì)的論文很容易被不懂行的審稿專家“槍斃”。李初民有這方面的親身經(jīng)歷。2017年，他指導(dǎo)學(xué)生實(shí)現(xiàn)了一項(xiàng)子句精簡(jiǎn)技術(shù)，非常有效，投到 IJCAI 后，有審稿專家就說，很多人都已經(jīng)實(shí)現(xiàn)過這個(gè)技術(shù)，因此論文沒有創(chuàng)新?！靶液糜幸粋€(gè)行家指出我們與別人的不同，論文才逃過了被‘槍斃’的命運(yùn)?！焙髞恚瑧{借這項(xiàng)技術(shù)，他們獲得了當(dāng)年 SAT 競(jìng)賽的金牌，這項(xiàng)技術(shù)與他們的實(shí)現(xiàn)方式也成為了SAT求解器的標(biāo)準(zhǔn)配置。除了自己研究 SAT 求解器，李初民也樂于指導(dǎo)對(duì)SAT求解有興趣的年青人。蔡少偉也許是李初民指導(dǎo)過的學(xué)生中，堅(jiān)持研究 SAT 最久的學(xué)生。他從2009年正式開始 SAT 以及相關(guān)問題的算法研究，第一個(gè)成果是利用 SAT 求解的約束加權(quán)技術(shù)設(shè)計(jì)另一個(gè)經(jīng)典NP 難問題---最小頂點(diǎn)覆蓋問題的局部搜索算法，該算法 EWLS 在一個(gè)著名挑戰(zhàn)實(shí)例 frb100-40 上打破了當(dāng)時(shí)的世界紀(jì)錄。之后，他繼續(xù)深入局部搜索算法研究，嘗試解決其重要缺陷，即循環(huán)問題。系統(tǒng)搜索與隨機(jī)（局部）搜索是SAT問題中的兩大方向。拿走地圖舉例，系統(tǒng)搜索是：走走剪剪，走到地圖的哪一塊，就將哪一塊剪掉，所以這張地圖會(huì)越走越小，最后走空了，就知道所有地方都走過了；而隨機(jī)搜索是：你在地圖上跑來跑去，但是你不記得你跑過哪些地方，沒有“剪枝能力”，無法剪掉，造成循環(huán)訪問的現(xiàn)象。如果說 SAT 問題是計(jì)算機(jī)科學(xué)世界的大門，那么相變現(xiàn)象則是大門的鎖芯，因此相變區(qū)實(shí)例也成為 SAT 求解的熱門測(cè)試集。而隨機(jī)搜索是求解相變區(qū)實(shí)例的最有希望的方法，但對(duì)于大規(guī)模相變實(shí)例仍然有較大障礙。導(dǎo)致相變區(qū)難解的本質(zhì)原因，就是隨機(jī)搜索的循環(huán)現(xiàn)象。針對(duì)這個(gè)問題，當(dāng)時(shí)已有的解決方法主要是馮·諾依曼獎(jiǎng)獲得者 Fred Glover 在1998年提出的禁忌搜索策略（tabu search）與荷蘭萊頓大學(xué)教授 Holger Hoos 在2002年提出的隨機(jī)擾動(dòng)方法。但是，它們沒有利用問題結(jié)構(gòu)，無法針對(duì)問題結(jié)構(gòu)做出調(diào)整，且?guī)в袇?shù)，在使用的時(shí)候常常需要大量的調(diào)參工作。所以，蔡少偉思考如何克服隨機(jī)搜索中的循環(huán)缺陷，希望設(shè)計(jì)出一種兩全其美的方法，既能保留隨機(jī)搜索的優(yōu)勢(shì)，又能克服其循環(huán)搜索的缺陷。但這并不簡(jiǎn)單，蔡少偉苦苦思索，停滯數(shù)月，毫無進(jìn)展。心情自然十分郁悶。那段時(shí)間，他讀了許多無關(guān)本領(lǐng)域的書，尤其是博弈論與社會(huì)學(xué)。其中，許多篇章談到個(gè)體與群體的關(guān)系。帶著“如何克服循環(huán)缺陷”的問題，蔡少偉雖然是閱讀課外書籍，卻時(shí)時(shí)忍不住將這個(gè)問題與書中的章節(jié)內(nèi)容聯(lián)系起來，讀著讀著，突然冒出一個(gè)想法：可以利用環(huán)境信息減輕循環(huán)！雖然直覺告訴蔡少偉這個(gè)思路可行，但直到不久后，他在一次交流會(huì)上聽到李初民對(duì) SAT 算法研究的演講，才突然受到啟發(fā)，一剎那看到了自己苦思冥想的方法！“世界突然安靜了，只有筆尖和紙張摩擦的聲音，我飛快地寫著，很怕是個(gè)幻覺，會(huì)馬上消失。”在個(gè)人博客中，蔡少偉記錄了這一美妙的精神過程。也是在這一瞬間，他創(chuàng)造了博士期間的得意之作：格局檢測(cè)策略（CC）。格局檢測(cè)的核心是：如果變量的環(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è)置多層評(píng)分函數(shù)克服“短視”。
圖 / 格局檢測(cè)策略示意圖
運(yùn)用這個(gè)方法，他大幅度改進(jìn)了原來的算法，產(chǎn)生了第二篇論文，2011年發(fā)表在頂刊《人工智能期刊》（AIJ）上。蔡少偉意識(shí)到這個(gè)新方法的通用性。他花了一段時(shí)間靜心思考，把它抽象成一個(gè)通用方法，應(yīng)用到 SAT 問題上。起初并不見效，但他“已陷入 SAT 問題不可自拔”，決心作出名堂。通過半年的努力，他終于超過了當(dāng)時(shí) SAT 比賽的冠軍算法。但好景不長(zhǎng)，2011 年 SAT 比賽的新冠軍又讓他的算法黯然失色。期間幾多波折，也經(jīng)歷了數(shù)個(gè)低谷，直到 2012 年 SAT 比賽，蔡少偉又扳回一城，獲得冠軍！對(duì)于這場(chǎng)奪冠，蔡少偉印象深刻：2011年年底，他開始著手準(zhǔn)備，雖然算法在當(dāng)時(shí)已達(dá)到國(guó)際前沿，但并沒有太大的把握。過完寒假回校，他一邊忙畢業(yè)的事，一邊備戰(zhàn) SAT 比賽。有兩位師弟幫忙，研究進(jìn)度加快不少，“開始只是小優(yōu)化，如隔靴搔癢，一直到比賽截止兩個(gè)禮拜前才有了質(zhì)的飛躍?！?/span>果然，比賽結(jié)果公布，三條主賽道，蔡少偉組的算法（CCSat）贏得了隨機(jī)組（測(cè)試集為相變區(qū)實(shí)例）的第一名，并且遙遙領(lǐng)先于第二名，求解效率比是 423（70.5%）vs 321（53.5%）。
圖 / 蔡少偉組的 CCSat 打敗了 Kevin Leyton-Brown 等人提出的 SATzilla 求解器
這也是中國(guó)第一次在國(guó)際SAT協(xié)會(huì)舉辦的 SAT 比賽系列中取得冠軍，蔡少偉的心情無比激動(dòng)。在做算法設(shè)計(jì)時(shí)，他堅(jiān)持算法大師 Dijkstra 的信條，“優(yōu)雅就是簡(jiǎn)單而高效”。他的格局檢測(cè)策略是一個(gè)全新的方法，經(jīng)過凝練，簡(jiǎn)單而高效。一路堅(jiān)持下來，沒想到竟成就了自己的風(fēng)格。蔡少偉的算法以明顯優(yōu)勢(shì)奪冠，在當(dāng)時(shí)的學(xué)術(shù)界也引起了較大反響。Holger Hoos 稱 CCASat是代表性最前沿求解器，比賽舉辦方更是以CCASat的成功說明研究核心算法的重要性。2012年前后，隨機(jī)搜索有逐漸被邊緣化的跡象。蔡少偉提出格局檢測(cè)策略后，加上當(dāng)時(shí)隨機(jī)搜索方向的其他學(xué)者的工作（如probSAT），隨機(jī)搜索再一次吸引了國(guó)內(nèi)外學(xué)者的注意，讓大家覺得：哦，原來隨機(jī)搜索還有很大的研究潛力。接下來幾年，隨機(jī)搜索吸引了更多人加入其中?，F(xiàn)在，隨機(jī)搜索已經(jīng)成為和CDCL的系統(tǒng)搜索并駕齊驅(qū)的兩大主流算法之一。2012年從北大博士畢業(yè)后，蔡少偉繼續(xù)在SAT求解器上鉆研。他用兩年時(shí)間從澳大利亞格里菲斯大學(xué)獲得應(yīng)用數(shù)學(xué)博士學(xué)位，2014年回國(guó)加盟中科院軟件研究所，開始挑戰(zhàn)康奈爾大學(xué)計(jì)算機(jī)系教授 Bart Sellman 等人在1997年所提出的命題邏輯推理與搜索十大挑戰(zhàn)之一：結(jié)合系統(tǒng)搜索與隨機(jī)搜索設(shè)計(jì)出比這兩種方法更高效的算法。在蔡少偉深入 SAT 求解研究的同時(shí)，時(shí)任上海財(cái)經(jīng)大學(xué)交叉科學(xué)研究院院長(zhǎng)的葛冬冬開始琢磨線性規(guī)劃求解器的開發(fā)。如前所述，SAT 問題有許多變?cè)?，需要判定其?或1（真或假命題）。SAT問題也可以表現(xiàn)為一個(gè)線性方程組，但變?cè)荒苋?或1，又被稱為“0/1規(guī)劃問題”。只是，在現(xiàn)實(shí)生活中，問題建?？赡懿皇蔷€性方程，而是二次方程、三次方程、對(duì)數(shù)、指數(shù)、根號(hào)等等，x與y的取值也不僅僅是0或1，可以是任意數(shù)，包括整數(shù)、正數(shù)、實(shí)數(shù)……
圖 / SAT與混合整數(shù)規(guī)劃（MIP）、約束整數(shù)規(guī)劃（CIP）及約束規(guī)劃（CP）的關(guān)系
葛冬冬是運(yùn)籌學(xué)出身。運(yùn)籌學(xué)研究問題主要分兩步，第一步是建模，第二步是求解：將現(xiàn)實(shí)中的問題通過算法建成標(biāo)準(zhǔn)的數(shù)學(xué)模型（如線性不等式）后，再對(duì)數(shù)學(xué)模型進(jìn)行求解，從而解決現(xiàn)實(shí)問題。如果變量少，只有x與y，那么我們可以進(jìn)行手算；但當(dāng)數(shù)學(xué)模型涉及到幾百萬變量，則必須借助軟件（如matlab）來自動(dòng)計(jì)算。本質(zhì)上，求解器就是一個(gè)專業(yè)的數(shù)學(xué)/計(jì)算軟件，用于實(shí)現(xiàn)復(fù)雜的數(shù)學(xué)算法。當(dāng)軟件對(duì)線性方程組求解時(shí)，該軟件可以稱為“線性方程組的求解器”。計(jì)算機(jī)歷史上最早的求解器，就是線性規(guī)劃求解器。葛冬冬對(duì)求解器有所耳聞，要追溯到他在斯坦福讀博的師門關(guān)系：1947年，“線性規(guī)劃之父”、斯坦福大學(xué)教授 George Dantzig （葛冬冬的師爺）提出了第一個(gè)用于優(yōu)化線性系統(tǒng)的算法，叫“單純形法”（Simplex Method），第一次使大規(guī)模優(yōu)化問題得到求解。單純形法一直雄踞二十世紀(jì)最偉大的算法前五之列。30年后，隨著計(jì)算機(jī)技術(shù)的發(fā)展，人們又開始嘗試用計(jì)算機(jī)開發(fā)求解軟件。1979年，第一個(gè)求解器軟件在美國(guó)誕生，名為 LINGO。 圖 / George Dantzig，電影《心靈捕手》男主人公的原型
1980年代，美國(guó)又有多位學(xué)者提出了內(nèi)點(diǎn)法（Interior-Point algorithm）。此前，線性系統(tǒng)優(yōu)化一直是單純形法的天下，直到內(nèi)點(diǎn)法出現(xiàn)。內(nèi)點(diǎn)法在某些問題上比單純形法的求解速度更快，可以處理許多非線性規(guī)劃問題，從而成為新的潮流，并也被用于商用求解器的開發(fā)。George Dantzig 的得意門生葉蔭宇（葛冬冬的導(dǎo)師）也是公認(rèn)的內(nèi)點(diǎn)法奠基者之一，因此獲得了運(yùn)籌學(xué)的最高獎(jiǎng)——馮·諾依曼理論獎(jiǎng)。
歷史上線性規(guī)劃求解的兩大流派，都是由葛冬冬的師長(zhǎng)創(chuàng)立。因此，讀博期間，他也跟著學(xué)習(xí)、琢磨了很多線性規(guī)劃求解實(shí)例。與SAT求解器一樣，以往研究線性規(guī)劃、整數(shù)規(guī)劃或混合規(guī)劃的人員有許多，但真正狠得下心開發(fā)求解器的人極少。葛冬冬剛回國(guó)時(shí)，發(fā)現(xiàn)國(guó)內(nèi)沒有人做求解器，覺得很奇怪，便去打聽，發(fā)現(xiàn)原因很簡(jiǎn)單：高校不做求解器，是因?yàn)樵趯W(xué)術(shù)上的性價(jià)比低，工具研發(fā)不能算科研；而企業(yè)不做求解器，根本上是覺得這是一個(gè)浩大而困難的工程，技術(shù)實(shí)力根本不可能做得到。毫無疑問，求解器的開發(fā)是一個(gè)大規(guī)模系統(tǒng)工程，動(dòng)輒上百萬行代碼。此外，求解器軟件對(duì)開發(fā)人員的數(shù)學(xué)能力要求特別高，而中國(guó)的情況是：同時(shí)精通數(shù)學(xué)與大規(guī)模軟件開發(fā)能力的人幾乎不存在。這一點(diǎn)與美國(guó)形成鮮明的對(duì)比，美國(guó)學(xué)生通常是一邊思考數(shù)學(xué)問題，一邊思考如何用代碼復(fù)現(xiàn)問題。對(duì)于中國(guó)教育缺少對(duì)學(xué)生抽象思維的培養(yǎng)，葛冬冬與李初民的想法不謀而合。李初民認(rèn)為，“邏輯就是力量”，即能夠深刻理解各種事物之間的邏輯關(guān)系，想得到一個(gè)果，要先去追求因，而這個(gè)因可能又是另一些事物的果。中國(guó)文化博大精深，而美中不足之處，是缺乏對(duì)形式邏輯培養(yǎng)的重視。所謂形式邏輯，即“符號(hào)邏輯”：把含義去掉，用無意義的符號(hào)來代表事物，比如“變?cè)保▁）。“不重視形式邏輯，也許是科學(xué)在中國(guó)發(fā)展緩慢的原因之一，因?yàn)榭茖W(xué)需要大量的邏輯推理?！崩畛趺裾劦?。此外，研究求解器不容易發(fā)論文。研究求解器的老員工常說一句話：“求解器的秘密就在于它沒有秘密?！?/span>就是說，求解器中的數(shù)學(xué)問題與實(shí)現(xiàn)算法都能在數(shù)學(xué)論文中找到，但不同求解器寫出來的代碼質(zhì)量良莠不齊。一方面，這要考驗(yàn)人的系統(tǒng)開發(fā)與數(shù)學(xué)結(jié)合能力；另一方面，需要花費(fèi)許多時(shí)間與精力去做大量的嘗試，俗稱“踩坑”。例如，就整數(shù)規(guī)劃中的啟發(fā)式算法模塊而言，德國(guó)的 Zuse Institute Berlin（ZIB）研究所花了近20年時(shí)間開發(fā)一個(gè)求解器 SCIP，里面用了57種啟發(fā)式算法做模塊的加速。如果單看啟發(fā)式算法相關(guān)的論文，全世界大概有上萬篇這樣的論文，這些論文里大概提出了上千種能夠加速的啟發(fā)式算法。如果要將這些啟發(fā)式算法全部寫到軟件中，一個(gè)個(gè)地測(cè)試其實(shí)用性，可想而知工作量會(huì)有多龐大。
圖 / 位于德國(guó)柏林的ZIB研究所
從2013年加入上海財(cái)經(jīng)大學(xué)后，葛冬冬便開始有意識(shí)地招收一些擅長(zhǎng)做優(yōu)化算法的年青人。那時(shí)，他有些猶豫：“求解器這事究竟能不能做？”心里沒底，跑去咨詢導(dǎo)師，葉老師很支持，說：“中國(guó)總得要自己的求解器，不要老覺得做不成，總得有人挑頭?！?/span>于是，2015年，葛冬冬聯(lián)合海內(nèi)外的同門師兄弟羅小渠、王子卓與王曦，創(chuàng)立了杉數(shù)科技，開始倒騰求解器。杉數(shù)剛成立，葉蔭宇弟子、斯坦福博士等稱號(hào)，就為他們拿到了大約200萬美元的天使輪投資。最初，他們是從上海財(cái)大的交叉科學(xué)院調(diào)配人手，加上杉數(shù)科技的創(chuàng)始團(tuán)隊(duì)，從零開始探索做一個(gè)開源求解器。葛冬冬與創(chuàng)始團(tuán)隊(duì)自學(xué)、找專家、找導(dǎo)師，花了很多力氣琢磨求解器開發(fā)，比如單純形法與內(nèi)點(diǎn)法如何在軟件開發(fā)上走通全流程，弄清楚求解器開發(fā)的核心部件，矩陣數(shù)據(jù)簡(jiǎn)化等等。期間，葉蔭宇給了許多指導(dǎo)，甚至親自下場(chǎng)幫他們寫開源代碼。經(jīng)過兩年的摸索，他們?cè)?017年發(fā)布了中國(guó)第一個(gè)開源優(yōu)化求解器 LEAVES，但性能并不突出。這使他們意識(shí)到，開發(fā)求解器是一個(gè)很大的系統(tǒng)工程，光靠學(xué)校的力量、投入小的成本是做不成的。所以，杉數(shù)開始在國(guó)際上秘密尋求有經(jīng)驗(yàn)的人，組建團(tuán)隊(duì)。“說白了，真正懂求解器開發(fā)的就是三大廠（XPRESS、GUROBI與CPLEX）的開發(fā)人員，每家的核心開發(fā)都不到10人，所以全世界真正精通求解器的不過20多人?！备鸲榻B，“加上德國(guó)柏林ZIB研究所的人，葉老師一位開發(fā)第三方商業(yè)求解器 MOSEK 的丹麥博士生和他的團(tuán)隊(duì)。以及很少的一些成熟開源求解器的高手，也就是說，全世界的核心求解器開發(fā)人才，就這30多個(gè)人。” 圖 / 葛冬冬在杉數(shù)科技擔(dān)任首席科學(xué)官
幸運(yùn)的是，他們最終在XPRESS找到了一個(gè)志同道合的中國(guó)人，本科就讀于北航計(jì)算機(jī)系，畢業(yè)后去英國(guó)讀博，博士期間的內(nèi)容就是研發(fā)求解器。之后，他們又陸陸續(xù)續(xù)從CPLEX、XPRESS與LINGO等處挖到了多個(gè)程序員。后來，又有一些人奔著杉數(shù)創(chuàng)始團(tuán)隊(duì)都是葉蔭宇學(xué)生的份上而來。葉蔭宇提出的“內(nèi)點(diǎn)法”的具體實(shí)現(xiàn)方法是各大商業(yè)求解器的底層架構(gòu)，圈內(nèi)有名，所以，在他的感召下，杉數(shù)找到了許多優(yōu)秀的人才。國(guó)內(nèi)的高校也開始了這方面的有意識(shí)嘗試。2018年，中科院戴彧虹研究院團(tuán)隊(duì)推出了國(guó)內(nèi)第一款整數(shù)規(guī)劃求解器CMIP。又過了兩年，2019年5月，杉數(shù)推出中國(guó)首個(gè)商用線性規(guī)劃求解器COPT。COPT的出現(xiàn)，給國(guó)內(nèi)大廠傳遞了一個(gè)重要信息：開發(fā)求解器的難度確實(shí)極高，但也不是全無可能。隨著企業(yè)的數(shù)字化轉(zhuǎn)型，需要進(jìn)行更多量化的、精細(xì)的智能決策，借助一些數(shù)學(xué)模型來建模，求解器的用途也越來越大。因此，國(guó)內(nèi)有能力的大企業(yè)（比如華為和阿里巴巴）也開始自己琢磨做求解器。與歐美數(shù)十年前就將求解器用于航空、鐵路交通規(guī)劃不同，工業(yè)求解器在中國(guó)的落地歷史很短，最早可以追溯到2000年代初期，寶鋼采用 ILOG CPLEX 優(yōu)化生產(chǎn)規(guī)劃系統(tǒng)。在COPT出現(xiàn)之前，商業(yè)求解器三大廠 CPLEX、GUROBI 與 XPRESS 憑借豐富的商業(yè)開發(fā)經(jīng)驗(yàn)，以及較好的性能，在國(guó)際市場(chǎng)上占了超過90%的份額。三大求解器中，歷史最坎坷的是1988年由美國(guó)數(shù)學(xué)家 Robert E. Bixby 所開發(fā)的 CPLEX。1997年，CPLEX 由法國(guó)企業(yè) ILOG 收購，2009年，ILOG 又被 IBM 收購，從此 CPLEX 變成了 IBM 的求解器。當(dāng)時(shí)，CPLEX功能較完善，擅長(zhǎng)各類求解，在市場(chǎng)上占了統(tǒng)治地位。
圖 / Robert E. Bixby
但沒過多久，由于 IBM 的自身管理問題，以及對(duì)求解器業(yè)務(wù)不夠重視，IBM求解器團(tuán)隊(duì)的幾個(gè)最核心開發(fā)人員從 CPLEX 離職，出來創(chuàng)立了新的公司，叫 GUROBI。GUROBI 的唯一業(yè)務(wù)就是開發(fā)求解器，他們十分注重這一塊，很快超過了CPLEX。隨著 IBM 的越發(fā)衰落，CPLEX也隨之慢慢衰落，美國(guó)商用求解器成了 GUROBI 的天下。與此同時(shí)，英國(guó)愛丁堡的Dash Optimization團(tuán)隊(duì)在1983年開發(fā)了 XPRESS，1986 年開始應(yīng)用于混合整數(shù)規(guī)劃求解。該團(tuán)隊(duì)的開發(fā)人員大約有10人，一直相對(duì)穩(wěn)定。2008年，XPRESS 由美國(guó)金融信用商 FICO 收購，將求解器用于制定金融場(chǎng)景的大規(guī)模優(yōu)化方案。收購后，F(xiàn)ICO 不做過多干涉，XPRESS 的開發(fā)團(tuán)隊(duì)繼續(xù)留在英國(guó)，保持了自身的競(jìng)爭(zhēng)力，在市場(chǎng)上占有一定份額。這三家均是開始商用求解器，以核數(shù)定價(jià)，核數(shù)越高，價(jià)格越高。在中國(guó)還沒有商用求解器之前，進(jìn)口求解器的價(jià)格基本是賣方市場(chǎng)。杉數(shù)的 COPT 發(fā)布后，無論核數(shù)多少，均以打包價(jià)出售，倒逼國(guó)外品牌將價(jià)格下降來競(jìng)爭(zhēng)中國(guó)的市場(chǎng)。近兩年，華為與阿里也開始布局求解器開發(fā)。華為開發(fā)求解器，主要用于EDA設(shè)計(jì)、供應(yīng)鏈規(guī)劃等，而阿里做求解器，則主要用于阿里云的資源調(diào)度優(yōu)化。阿里也是從線性規(guī)劃入手，先做單純形法，再做內(nèi)點(diǎn)法。2020年，阿里達(dá)摩院決策智能實(shí)驗(yàn)室發(fā)布數(shù)學(xué)規(guī)劃求解器 MindOpt。根據(jù)阿里的官方說法，在發(fā)布 MindOpt 時(shí)，他們已在內(nèi)部使用了一段時(shí)間，幫阿里云節(jié)省了數(shù)億元成本?，F(xiàn)在，求解器在阿里云上每天被調(diào)用的次數(shù)以十億計(jì)。過去兩年，杉數(shù)、阿里與GUROBI在線性規(guī)劃?rùn)?quán)威榜單 Mittlemann 測(cè)試上競(jìng)爭(zhēng)激烈。在單純形法測(cè)試上，阿里與杉數(shù)輪流當(dāng)?shù)谝唬?0%的時(shí)間是杉數(shù)領(lǐng)先；而在內(nèi)點(diǎn)法上，杉數(shù)一直穩(wěn)居榜首。在線性規(guī)劃單純形法上，GUROBI 已經(jīng)被擠到第三很久了。但是在整數(shù)規(guī)劃這一最重要的求解器開發(fā)上，國(guó)內(nèi)與美國(guó)還有著很大的差距。目前求解器軟件，國(guó)內(nèi)只有COPT具備了求解大規(guī)模整數(shù)規(guī)劃問題的能力?！澳壳拔覀兊?00家用戶，79%的問題來自整數(shù)規(guī)劃。雖然在榜上排名世界第二，但是實(shí)際上我們與三大廠都還有著不小差距。整數(shù)規(guī)劃能力的提升，難度是線性的幾十倍，是一個(gè)漫長(zhǎng)的旅程。我們還需要持續(xù)艱苦的努力?！备鸲偨Y(jié)。就制造業(yè)而言，求解器是最核心的軟件。比方說，國(guó)家電網(wǎng)的調(diào)度優(yōu)化、無功優(yōu)化、電力市場(chǎng)清算等等環(huán)節(jié)，背后有上千個(gè)求解器在不停地計(jì)算。杉數(shù)的線性規(guī)劃求解器 COPT 自誕生以來，已應(yīng)用于能源、航空、制造、物流、零售等多個(gè)行業(yè)，合作的企業(yè)包括國(guó)網(wǎng)/南網(wǎng)、南航、華為、小米等大廠。杉數(shù)與這些大廠的其中一項(xiàng)合作是排產(chǎn)排程。對(duì)于 ICT（信息通信技術(shù)）這類大廠，設(shè)想一下，工廠數(shù)量多，數(shù)百個(gè)工廠有上千個(gè)生產(chǎn)車間，用到的零部件大約有10萬多種。如果同時(shí)收到幾百個(gè)訂單，規(guī)定在未來的20周內(nèi)完成，這時(shí)就需要全局優(yōu)化思想，避免造成資源浪費(fèi)。我們可以將這個(gè)問題建模成一個(gè)整數(shù)規(guī)劃問題，即使考慮其簡(jiǎn)化形式線性規(guī)劃，變量與約束也都是上億級(jí)別，但求解器可以快速求解。談到求解器的變遷，葛冬冬感嘆，求解器的發(fā)展也很快，2009年那會(huì)，求解器算一個(gè)百萬級(jí)別的線性規(guī)劃很吃力，但如今，上億級(jí)別的線性規(guī)劃只需一個(gè)小時(shí)的計(jì)算量。“一開始大家覺得（上億級(jí)變量問題）只能用 GUROBI 算，我們也沒什么信心。最后發(fā)現(xiàn)，我們不但能算出來，而且計(jì)算速度比 GUROBI 快了大概 30% 以上?！?/span>不同領(lǐng)域的求解器在底層思想上有相通的地方。比如，現(xiàn)在華為就開始將SAT求解器中通行的沖突分析思想應(yīng)用在整數(shù)規(guī)劃求解器中。相對(duì)來說，線性規(guī)劃求解器在國(guó)內(nèi)外的發(fā)展更成熟，而 SAT 求解器在國(guó)內(nèi)做的人寥寥無幾，近些年來，只有蔡少偉團(tuán)隊(duì)在做自己道路的 SAT 求解器。他們?cè)c華為合作，將 SAT 求解器用于華為芯片中的電路等價(jià)驗(yàn)證，將miter電路轉(zhuǎn)為SAT問題，求解規(guī)模高達(dá)5000萬變量、1億5千萬子句，但只用了1小時(shí)。 圖 / 用 SAT 求解器做電路等價(jià)驗(yàn)證
工業(yè) SAT 求解的挑戰(zhàn)主要是變量依賴與超大規(guī)模，前者需要系統(tǒng)搜索，后者需要隨機(jī)搜索。換言之，用于工業(yè)的SAT求解器，需要將系統(tǒng)搜索與隨機(jī)搜索相結(jié)合。這也是 Bart Sellman 命題邏輯推理與搜索十大挑戰(zhàn)中的第七個(gè)挑戰(zhàn)。蔡少偉從2014年開始研究混合搜索求解器。此前，這方面的求解器有 ANC、WalkSatz 等等，但它們都是側(cè)重系統(tǒng)搜索與局部搜索在求解能力上的互補(bǔ)，黑盒調(diào)用，在工業(yè)實(shí)例上的表現(xiàn)無法超越單一的系統(tǒng)搜索方法。他深入探索了系統(tǒng)搜索和隨機(jī)搜索的算法行為以及在合作中的作用，經(jīng)過近幾年的研究，放棄了走求解能力互補(bǔ)的道路，提出了以隨機(jī)局部搜索采樣，以系統(tǒng)搜索求解，進(jìn)行基于信息交互的深度合作。實(shí)驗(yàn)結(jié)果顯示，與 2011 年到 2019 年 SAT 比賽的工業(yè)組冠軍與主賽道冠軍算法相比，蔡少偉所設(shè)計(jì)的混合搜索求解器比單搜索求解器平均比每個(gè)benchmark多解約30個(gè)算例，且能求出許多系統(tǒng)搜索與局部搜索均求不出來的實(shí)例（平均占求解實(shí)例的12%）。
圖 / 混合搜索求解器 RelaxedNewTech 框架示意圖
這也是距 Bart Selman 在1997年提出十大挑戰(zhàn)以來，首次有人解決了第七大挑戰(zhàn)。蔡少偉團(tuán)隊(duì)提出的松弛子句沖突學(xué)習(xí)方法也在2020年SAT比賽中獲得主賽道的冠軍；相關(guān)論文（“Deep Cooperation of CDCL and Local Search for SAT”）獲得 SAT 2021 最佳論文獎(jiǎng)，這也是SAT會(huì)議自1997年設(shè)立以來，第一篇來自中國(guó)的工作獲得該獎(jiǎng)。在解決 EDA 等中國(guó)“卡脖子”問題中，SAT 求解的地位無異于人的命門。同時(shí)，一個(gè)不容忽略的現(xiàn)實(shí)是：無論是 SAT 求解器，還是數(shù)學(xué)規(guī)劃求解器（包括線性規(guī)劃），中國(guó)人才始終占極少數(shù)。不過，李初民很樂觀。他認(rèn)為，中國(guó)研究SAT求解器的人一定會(huì)越來越多。今年，他和德國(guó)形式化專家Armin Biere，西班牙人工智能專家Felip Manya等人發(fā)起、他的早年學(xué)生黃沖和華中科技大學(xué)呂志鵬參與組織 EDA 國(guó)際算法競(jìng)賽 EDA Challenge (www.eda-ai.org)，收到的求解器約有一半來自中國(guó)。如今，除了SAT求解，蔡少偉也開始研究SMT（可滿足性模理論問題），SMT公式可以看作是SAT與數(shù)學(xué)規(guī)劃等背景理論的結(jié)合，SMT求解是更具挑戰(zhàn)的方向，國(guó)內(nèi)更是無人問津；同樣地，葛冬冬與杉數(shù)的研究重心也從線性規(guī)劃求解轉(zhuǎn)到了整數(shù)規(guī)劃和非線性規(guī)劃求解。無論是從SAT到SMT，還是從線性規(guī)劃到整數(shù)規(guī)劃，蔡少偉與葛冬冬所傳達(dá)的訊號(hào)是一致的：用求解器加速中國(guó)的工業(yè)發(fā)展。從廣義上看，求解器的意義不僅僅在于工業(yè)的發(fā)展。葉蔭宇一直認(rèn)為，國(guó)內(nèi)應(yīng)該形成一個(gè)將數(shù)學(xué)與代碼相結(jié)合的研究生態(tài)，而開發(fā)求解器是一個(gè)很好的結(jié)合點(diǎn)。通過研究求解器，我們可以培養(yǎng)一大批既精通數(shù)學(xué)、又擅長(zhǎng)編程的人才。葛冬冬談道：“導(dǎo)師的想法是要鼓勵(lì)大家去研究求解器。所以后來，其他大廠或者高校做求解器，有時(shí)候遇到棘手的問題，跑來問我們。只要不涉及到核心機(jī)密，我們一般都會(huì)給他們義務(wù)解答?！?/span>而李初民則提到，SAT求解講究從沖突中學(xué)習(xí)變?cè)g的精確邏輯關(guān)系，機(jī)器學(xué)習(xí)是從大數(shù)據(jù)中學(xué)習(xí)數(shù)據(jù)的統(tǒng)計(jì)性質(zhì)，兩者可以相互促進(jìn)、相互補(bǔ)充，從而人工智能更好地發(fā)展。機(jī)器學(xué)習(xí)中的一些問題（比如決策樹），也可以表述為SAT問題。從這些優(yōu)秀學(xué)者的經(jīng)歷來看，我們不難發(fā)現(xiàn)，求解器是一項(xiàng)大工程：李初民從1994年開始研究，專注三年才開發(fā)出 Satz 求解器；蔡少偉從2014年挑戰(zhàn)系統(tǒng)搜索與局部搜索相結(jié)合，直到2020年才算“拿下”這個(gè)問題；葛冬冬等人從2015年開始研究，只做求解器，用了4年才開發(fā)了他們的王牌solver — COPT。蔡少偉感嘆，求解器適合馬拉松型選手，“很巧的是，我以前讀書時(shí)參加百米短跑，總是壓著及格線過關(guān)。但如果是跑5000米，我往往就能跑得比較好?！?/span>相比機(jī)器學(xué)習(xí)，求解器的熱度相形見絀。生于深度學(xué)習(xí)時(shí)代，無論是蔡少偉，還是葛冬冬，他們都沒有被外界的浪潮卷動(dòng)，始終堅(jiān)持自己最初的追求，以內(nèi)因戰(zhàn)外因，做沒有深度學(xué)習(xí)的 AI 研究。十年過去，他們成為了中國(guó)少數(shù)研究求解器的青年砥柱。如果沒有他們的堅(jiān)持，我國(guó)求解器的研究也許仍是空白狀態(tài)。熱潮自有大眾追捧，但對(duì)人才本就稀缺的領(lǐng)域來說，一個(gè)人的堅(jiān)持，很可能就決定了全局的命運(yùn)。
作者注：人物/采訪、交流、爆料、抬杠，歡迎添加微信（302703941）。???????????????
雷鋒網(wǎng)雷鋒網(wǎng)雷鋒網(wǎng)
雷峰網(wǎng)原創(chuàng)文章，未經(jīng)授權(quán)禁止轉(zhuǎn)載。詳情見轉(zhuǎn)載須知。
???????????????
