关于约束编程的学士论文

概述

作为信息科学专业的本科生，我的研究从一个很实际的问题出发：当仿真器积累了大量可能的条件时，怎样才能让它不再去反复考虑那些已经不可能发生的条件？我为 HydLa 设计并实现了一种方法，利用变量正在变化的方向，把已经失效的条件从搜索中移除，并对它做了评估。在作为基准的模型上，仿真的总耗时减少到大约一半。

这项研究是我的设计哲学最早的地基。约束编程让我明白，复杂的结果并不总需要被直接指定：它们可以从一个经过仔细定义的规则、优先级与边界所构成的空间里生长出来。这种思考方式如今支撑着我在 AI 时代从约束出发做设计的方式——去设计一个生成系统可以自由行动的条件。

摘要

HydLa 是一种面向混成系统的建模语言，所谓混成系统，是连续变化与离散事件相互作用的系统。基于约束的设计让这类系统可以被简洁地描述，并以很高的精度加以仿真。代价是：模型一旦变大，仿真器就会一直检查数量庞大的条件规则，即使其中一些早已无关。

本研究提出在运行过程中动态削减这些守卫约束。只要能识别出单调的行为——某个值持续朝一个方向变化——仿真器就可以断定某些守卫条件在将来永远不会成立，从而安全地停止检查它们。在含有大量同类守卫对象的模型中，这一方法尤其有效：实测运行时间降到了原来的大约一半。

1. 引言

混成系统同时包含连续的行为与离散的事件。弹跳的小球就是一个简单的例子：它在空中时，位置与速度连续变化，而撞到平面的那一瞬间构成一个离散事件，改变了它的方向。恒温器、汽车与机器人，内部都藏着同一种混合，只是后果更为重大。

HydLa 让建模者用数学与逻辑的约束来描述这类系统，而不必写出一条唯一的过程序列。它的仿真器 HyLaGI 可以进行没有舍入误差的符号计算，也能处理取值不确定的参数。然而这种表达力带来了规模上的问题：当一个模型含有许多只在特定条件下才生效的规则时，仿真器必须一遍又一遍地追问，每个条件是否就是下一个将要发生的那个。

2. 仿真中的守卫约束

守卫约束是只在其守卫条件被满足时才生效的规则。在上面的基准模型里，每个平面区段都有自己的规则：如果小球的高度降到零，而它的水平位置正落在该区段之内，弹跳规则就适用。因此，把平面切得越细，仿真器要检查的守卫条件也就越多。

实验把区段数从 10 变化到 200。原有的仿真器变慢的速度，大致与这个数目的平方成正比。这件事的意义不止于一个玩具例子：更大的模型很可能正是以这种带守卫的形式，表示大量物体、接触区域或可能发生的事件。

3. 瓶颈所在

性能剖析显示，这种变慢并没有均匀地分布在仿真器各处。当平面被分成 100 个区段时，实测运行时间的 96% 都花在 FindMinTime 上——那是寻找下一个最早可能事件的操作。它在反复求值每一个候选约束的守卫条件。

这个结果让优化的目标变得具体：在完全不改变被仿真行为的前提下，减少 FindMinTime 必须考虑的守卫条件数量。

4. 守卫约束的削减

设想一个小球沿着楼梯逐级弹跳向下。一旦小球越过某一级台阶并继续向前，那一级就再也影响不到它了。看图的人会立刻忽略小球身后的台阶；而原有的算法仍在逐一检查它们。

困难之处在于证明被丢掉的守卫条件在之后永远不会再被用到。仅仅因为它此刻为假就把它移除，万一它重新变为真，就可能悄无声息地给出错误结果。因此提案使用单调性：判断某个变量在一段时间区间内，是否保证持续增大或持续减小。

4.1 一致单调性的处理方式

第一种处理方式适用于变量在整个仿真过程中只朝一个方向移动的情形。在分段平面的模型里，小球的水平位置始终增大。一旦它越过某个区段，该区段的条件就再也不可能被满足。这一性质可以在仿真之前用模型检验的技术加以确立，于是随着运行的推进，失效的守卫条件可以被安全地移除。

4.2 交替单调性的处理方式

现实中的许多系统并不会永远朝一个方向变化。一个变量可能先增大，然后转向，接着减小。因此论文勾勒了第二种处理方式：先假定一个方向，用断言监视这个假定，并从方向改变的那一点起重新开始削减的逻辑。为某个单调区间移除的守卫条件，会在下一个区间开始时被恢复。

5. 实验结果

我实现了一致单调性这一路线，并用分段平面的模型加以评估。随着区段数增加，原有算法与提案算法的耗时都还是会变长，但提案版本始终做了更少的工作。比较拟合出的曲线，最高次项系数从 1.1463 降到 0.6083；对这个基准而言，仿真的总耗时大约减半。

这并不是说任何 HydLa 模型都会快上一倍。它说明的是这一方法在哪里有用：含有大量守卫对象、变化方向可被证明、并且守卫条件会在运行过程中永久失效的模型。

6. 结论与未来工作

这项研究表明，让仿真更高效的途径不只是把低层计算做得更快，关于模型本身的知识同样可以做到。借助单调性识别出哪些可能性已经变得不可能，HyLaGI 就能在不改变结果的前提下缩小其有效约束集合。

实际实现并验证的是一致单调性这一侧。论文为后续工作留下了两个方向：评估针对交替行为的断言方法，以及利用单调性之外的不变性质，找出更多可以被安全移除的约束。