2.3 约束可满足性求解
“Constraint programming represents one of the closest approaches computer science has yet made to the Holy Grail of programming: the user states the problem, the computer solves it.”这是美国艺术与科学学院院士、AAAI Fellow、约束程序（Constraint Programming，CP）研究领域的开创者和奠基人、著名人工智能学学者、爱尔兰考克大学 Eugene
Freuder 教授 1997 年为我们描绘的约束程序未来发展愿景[105] 。这也
毫无疑问是人工智能，乃至计算机科学的最高理想，即：用户表述问 题，计算机自动求解。彼时，CP 这个源于计算机图形学 [106] [107] 的 问题求解方法刚在人工智能研究领域中占有一席之地，尚不广为人知。
进入 21 世纪后，约束程序研究得到空前快速发展，并已逐步成
为人工智能的基本支撑方法和技术[108] [109] 。2005 年 3 月，在法国成立了“国际约束程序学会”（Association for Constraint Programming, ACP）[110] ，会刊为 International Journal of Constraints，每年定期召
开 CP 学术年会。目前，在 IJCAI, AAAI 等权威人工智能国际会议上，与约束程序相关的研究论文数量呈现逐年增长的趋势，越发显示其作为人工智能问题求解方法的重要地位。IJCAI2011、IJCAI2013 、 AAAI2019 和IJCAI2020 的程序委员会主席分别是或将是澳大利亚新南威尔士大学的 Toby Walsh 教授和意大利帕多瓦大学的 Francesca Rossi 教授，美国密歇根大学 Pascal Van Hentenryck 教授（与南京大学周志华教授同为联合主席） 和法国蒙彼利埃大学的 Christian Bessiere 教授，他们都是蜚声国际专门从事约束程序研究的人工智能学者。
约束程序以人工智能领域著名的约束满足问题（ Constraint Satisfaction Problems, CSPs）的建模和求解研究[108] [109] 为核心，大量来自汽车、交通、航空、电信、教育等领域中的规划、调度、配置、推荐等问题都适合采用约束满足问题来建模和求解[108] [109] ，这为约束程序的成功应用提供了天然优越条件。当前，约束程序在工业界取得极大成功。IBM ILOG 优化引擎成已成为SAP、Oracle 等跨国IT 巨头 ERP 等软件产品的核心优化技术[111] 。2014 年 11 月 12 日，欧洲宇航局 10 年前发射的彗星探测器的着陆器“菲莱”成功登陆“丘留莫夫－格拉西缅科”彗星，完成人造探测器的首次彗星登陆壮举，在 “菲莱”执行此次任务及后续实验过程中起主导作用的软件技术是约束传播和基于约束调度方法等 CP 技术[112] [113] ，这为人工智能助力人类太空探索历史留下了浓墨重彩的一笔。
但是，和通用人工智能当前面临的困境类似[114] ：具有通用功能的约束程序的建模和求解方法的进展与我们的期望还有距离。尤其在大数据背景下，特别是 2015 年以来，在以机器学习飞速进步为代表的新人工智能浪潮冲击下，约束程序还面临不少新的挑战。如我们面对的约束满足问题呈现出开放交互、大规模、结构化不显著等多种特征[115] ，半结构甚至无明确显式结构的约束满足问题建模问题，怎样
利用大数据和机器学习方法改善现有的建模和求解方法？……约束程序从建模到求解全过程的自动化和可用性亟待加强，这也是 2017年国务院印发的《新一代人工智能发展规划》对人工智能发展提出的新要求[116] 。
当前，由 Freuder 教授创立、目前由 O'Sullivan 教授领导的爱尔兰 Cork 大学 Insight 研究中心是最具影响力的约束程序研究基地，并辐射法国、澳大利亚、美国、英国、和意大利等国研究机构。其中， O'Sullivan 教授领导的研究组在约束建模和约束组合求解等方面研究独树一帜，蒙彼利埃大学 Bessière 教授等在自适应约束传播和自动约束建模方法的研究最为突出。
国内研究主要集中在经典和分布式约束求解方法的研究，对于交互式约束建模与求解方法研究涉及不多，代表工作有：北京航空航天大学许可教授等提出了著名的 RB、RD 模型[117] 。香港中文大学的李浩文教授主要研究基于对称消除的约束求解方法[118] ；国防科技大学王怀民教授、东北大学张斌教授以及中国科技大学陈恩红教授等主要研究分布式约束优化问题的求解算法[119] [120] [121] 、中科院软件所张健教授、马菲菲博士对于混合约束满足问题求解方法及应用的研究
[122] [123] 。吉林大学研究组组早期在孙吉贵教授领导下，在国内较早开展约束程序研究，在约束求解理论、方法及约束求解系统方面做了很多颇具特色的研究工作[124] [125] ，研究结果得到 Christian Bessière教授、李浩文教授等国际知名研究者的肯定。
约束建模[126] 是约束求解的基础，模型选择的好坏将直接影响约束求解效率甚至问题是否可解，这一点已经得到约束程序界的共识
[127] [128] 。对于约束程序建模，2000 年，Simonis 曾给出了“30 条金法则”[129] ，但是多数并不具有普适性，只有“尽量不用布尔模型”、 “尽量少用变量和约束”等简单规则有一定影响。商用和学术方面取得成功的约束建模语言也层出不穷，如 OPL、Essence、MiniZinc 等功
能都十分强大，但这些建模语言都有一定的局限性：要求用户对于问题特征和求解算法有一个清晰的了解，即用户应具备相当专业的约束程序知识。
在互联网浪潮下，对于计算机系统的交互能力要求日渐提升，自动化同时也是各种人工智能系统的追求的普遍目标，对于交互建模和自动建模的能力需求迫切。基于此，先后在 2003 年和 2007 年，Bessière和 O'Sullivan 等人开创了基于问答的约束模型获取研究工作[130] [131]并开发原型系统 CONACQ。2009 年，Shchekotykhin 等人[132] ，提出了基于辩论的建模方法，以减少学习实例数。2010 年，Lallouet 等[133]提出基于归纳逻辑程序的约束模型自动获取方法。2016 年，Picard- Cantin 等[134] 针对序列约束建模问题提出了从正例中学习参数的方法。2016 年，Bessière 和 O'Sullivan 人首次提出了归纳约束程序循环理论模型[135] ，为机器学习和约束程序融合研究搭建了桥梁，同时也为约束自动模型获取研究指明了方向，但仅限于理论层面和小规模问题实例上，具体实现细节还不十分清晰。
近年来，约束求解方法的发展极为迅速[108] ，算法组合方法
（Algorithms Portfolios）和自动配置问题成为研究热点[136] [137] 。目前新的研究进展有：2010 年，Balafoutis 和 Stergiou 用统计学习方法对当前流行的变量序启发式做了一个比较系统的实验评估[138] 。对于值选择启发式，最近的代表性工作有：2005 年，Epstein、Freuder 和 Wallace 联合研制了个性哈启发式策学习、挖掘系统[139] ，2015 年， Chu 等提出了值选择启发式学习策略[140] 。同年，Ortiz-Bayliss 等首次提出了初步具备自动选择功能的“超级变量启发式”[141] 。但目前，在挖掘新的选择启发式策略和各种启发式策略组合应用方面的研究还刚起步，研究空间很大。对于算法级别的组合研究，2012 年，Amadini等人对约束求解器级别的组合求解进行了初步的实验评估[142] ，取得不错的效果，未来需要结合机器学习方法加强约束求解方法的精确选
择和深度融合。
自适应约束传播的有影响力的开创性工作是 2009 年 Stergiou 等提出的基于探查和简单学习机制实现的自适应[143] 。最新进展是2015年，Balafrej 等人提出的参数化自适应约束传播[144] ，我们研究组对此亦有贡献。但对于交互式环境的约束满足问题的自动求解研究还刚刚起步，理论基础还不足。除此之外，约束满足问题的结构特征也是影响算法求解效率的重要因素，法国阿尔多瓦大学的 Christophe Lecoutre 教授整理建立的 Benchmark 测试问题实例库[109] [145] ，涵盖各个应用领域的 2000 多个问题实例，是良好的学习和测试数据集。
2017 年，Freuder 教授为 ACP 会刊 Constraints 创刊 20 周年专门撰文“Progress towards the Holy Grail”指出[114] ：自动约束建模、自动问题求解[146] 将是约束程序下一步的研究重点。