关于约束型编程的毕业论文

概要

模拟器会随着可能事件的增加，重复检查更多的条件。那么，如果可以从进展中判断“这个条件再也不会成立”，是否可以安全地停止该检查呢？本研究以数值变化的方向作为线索，设计并实现了一种在运行中的搜索中剔除不再需要的条件的方法，针对混合系统建模语言HydLa。

在评价模型中，在不改变仿真结果的情况下，将执行时间缩短到传统方法的大约一半。重要的是，并不是把所有计算都统一加速，而是利用问题的结构，减少了需要考虑的可能性本身。

在这项研究中学到的约束型编程的思路，正成为当前我的设计哲学的基础。不是逐一直接指定结果，而是定义规则、优先级、边界，并从其中导出成立的解的态度。

问题——可能性越多，计算就越慢

HydLa 是一种用于将连续变化和离散事件相结合的“混合系统”以数学和逻辑约束形式进行描述的语言。即使不写出所有步骤的顺序，也可以通过声明应当成立的条件来模拟满足条件的行为。

另一方面，在根据条件生效的规则较多的模型中，模拟器会反复检查大量候选项。由于已经过去且将来也不成立的条件仍然留在候选项中，因此随着模型变大，不必要的计算不断累积。

题材——连续与离散混合的系统

弹跳的球是混合系统的一个易于理解的例子。在空中时，位置和速度连续变化，而在接触地面的一瞬间，会发生弹回这样的离散事件。温控器、汽车、机器人也是如此，虽然规模不同，但内部也存在相同的两种变化。

为了评估，使用了一个模型，即水平移动的球在被分成多个区块的面上反弹。每个区块都有一个条件规则：“球如果进入这个范围就会反弹”。增加区块的数量可以扩展可表达的对象，同时也增加了模拟器需要检查的条件。

瓶颈——条件的数量推高了计算量

只有在满足条件时才会生效的规则称为“带守卫的约束”。在评估模型中，只有当球到达地面且其水平位置在特定区域内时，该区域的反弹规则才会生效。

将区画数从10增加到200时，以往的模拟器大约按照区画数的平方比例变慢。在规模较大的模型中，由于物体、接触区域和可能发生的事件增多，同样的问题会变得更大。

调查——处理时间的96%集中在哪儿

测量处理时间时，在区块数为100的模型中，整体的96%用于FindMinTime。这是在候选事件中寻找“最早发生的事件”的处理。因此，所有的守卫条件都被反复评估。

需要改进的地方已经明确。不需要重做整个计算方法，只需安全地减少传递给FindMinTime的候选对象即可。目标是改变模拟结果之前，只排除不需要检查的可能性。

方法——安全地去除永远无法成立的条件

请想象一个沿着台阶跳下的球。如果球越过某一台阶并继续向前，那么这个台阶将不再影响球。看到图的人会立即忽略球身后的台阶。原来的算法则会继续检查每一个台阶。

困难的是，要证明被移除的守卫之后不会再需要。如果仅仅因为现在为假就移除，当它再次为真时，可能会默默地返回错误的结果。因此，所提出的方法使用单调性——即能否保证某个变量在某一时间区间内持续增加或持续减少。

变化的方向不改变的情况

第一个对应适用于变量在整个模拟过程中朝一个方向变化的情况。在将面分割的模型中，球的水平位置总是增加。一旦超过某个区间，该区间的条件将不再被满足。这一特性可以通过模型检查技术在模拟前确认，因此在执行过程中可以安全地移除不再需要的守卫。

变化的方向在途中发生变化的情况

现实中的许多系统，并不是永远朝一个方向运行。变量会增加，改变方向，然后可能减少。因此论文展示了第二种对应方法。首先假设方向，通过断言进行监控，并且从方向改变的时间点重新执行减少的处理。为一个单调区间移除的保护措施，会在下一个区间开始时恢复。

结果——将评估模型的运行时间大约减半

实现了对统一单调性的处理，并在分割面的模型上进行了评估。无论是原算法还是提案方法，区块数增加时所需时间都会增长。但提案方法的工作量始终较少。对比拟合的曲线后发现，最高次的系数从1.1463下降到0.6083，在这一基准测试中，整个模拟所需的时间大约减半。

这并不是说所有的 HydLa 模型都会加倍变快。这里所展示的是，这种方法有效的场景——即拥有许多守卫的对象，可以证明变化的方向，并且在执行过程中守卫会永久地变得无关的模型。

从这项研究中获得的视角

在这项研究中进行的不是逐步加快各个计算的速度。而是利用对系统行为已有的了解，缩小需要考虑的可能性集合。缩小搜索空间而不改变结果的这种思路，是约束型编程的优势所在。

实现和评估的是变量持续向一个方向变化的情况。如果变化方向在中途改变，则只停留在设计阶段，评估成为今后的课题。还有利用单调性以外的性质，进一步发现不必要约束的余地。

现在的我，不是直接设计AI的输出，而是试图设计AI可以探索的条件和边界，这也与这种经历有关。在处理复杂结果时，定义哪些可以不用考虑，与计算什么同样重要。