袁绍大军兵力 强盛，对兵力较少的曹营是个严峻挑战
曹营的张辽提议采用五人楔形阵 进攻，有利于冲击袁绍大军
楔形阵由奇数匹战马及其骑兵按楔形陈列而成
为保持阵型，每一匹马 都应比后方的马跑得快
另外，越位于前方的士兵，与敌军交锋更多 因此每位骑兵也需比其后方的骑兵更有耐力
军中的马匹也有偏好，只可以被特定的部分骑兵驾驭
如今需要从中选择合适的骑兵与马匹
配搭组成楔形阵，从而使阵中骑兵的战斗力最强
关羽取出神算法板，却发觉无法求解
因此，关羽利用神算法板 呼叫大师求助。
>> 在这个骑兵阵 的问题里面呢，我们需要根据我们的骑兵的
耐力，跟他们的战斗力，而且马的 速度，来安排一个楔形的阵出来
意思就是在这个阵里面，每一个位置我们应该放哪一 头马，跟哪一个骑兵
这个楔形阵呢，其实就好像英文字母 里面这个
V 这个字差不多，尖头的地方就是我们这个阵的前方
好了，当然这个问题里面有不同的条件，第一个条件呢就是
要求排在前面的马，比在它后方的马，一定速度要快一点
这个理由是非常简单，不然呢，后面的马 就可以把前面的马赶过，就破坏了这个队形了
第二个条件呢，就是我们要求排在前方的
骑兵，他比排在他后面的骑兵呢，他们的耐力也比较高一点
为什么呢？排在前面的骑兵呢，他们要跟 敌人去交锋的机会是大很多的
我们知道，人跟人要匹配
但是原来人跟马也需要是匹配的。
我们要求呢就是 每一个骑兵，他给他的马呢，是配合的
当然最后，我们需要是优化就是
我们整个团队的战斗力，就是所有骑兵的战斗力的总和，是最大化
这个呢就是我们这个骑兵阵的问题的一个 文字的描述了。
在这里呢，我们需要强调两点 第一，在这个楔形阵里面呢，我们的马的数目是需要是一个奇数
其实看看这个简单的例子，我们就可以理解为什么需要是这个奇数了
另外呢就是我们怎么标识我们这个阵里面每一个位置
我们看见呢，在这个左方的时候，我们的 越前呢，我们的数字是越大的
但是在右方的时候呢，我们越前呢，数字是越小的 这个我们需要是留意。
好了，我们看看这个骑兵阵 问题的模型，我们先看它的数据跟它的变量
首先呢，就是两个 枚举类型的数据来代表我们的马跟我们的骑兵
在后面呢，就是四个不同的数组来代表
每一头马它的速度，每一个骑兵他的
耐力，每一个骑兵他的战斗力，而且呢还有
就是，每一头马，它跟哪几个骑兵呢，它是配合的
然后我们也需要有一个数据，就是我们这个阵
的数目，我刚才已经提过了，它需要是一个奇数 我们之前也学过，如果我们的
输入的数据是有一个假设的话，我们需要利用一个断言来去
检测一下，所以我们下面呢，就需要一个断言来看看，我们这个 n 是否一个奇数来的
还有呢就是我们的变量了，我们有两个数组的 变量，第一个呢，就是我们这个阵里面，每一个
位置放什么的马，然后就是 每一个位置，我们要配合哪一个的骑兵
我们来看看这个模型里面的 约束跟它的目标。
第一组的约束呢就是说，我们要求呢，在这个
阵里面，每一个位置的马，都是不相同的，当然了，每一个位置的骑兵也是不相同的
下面呢我们有两组的 约束，它们就是去保证呢
在前面的马，比后面的马呢，要快一点，在前面的骑兵比后面的骑兵呢 他们的耐力是更高的。
你们还记得，在左边的时候呢，我们的位置的数字
是越前越大的，所以呢你们可以看见，前面的马的速度，是比后面的马的速度呢 要更快的。
前面的骑兵，他的 耐力比后面的骑兵的耐力呢，要高
到了我们的这个阵的右边的时候呢，我们呢的数字是
越前边是越来越小的，所以呢我们需要是前面的马
是比后面的马要更快，前面的骑兵比后面的骑兵，他的耐力要更高
然后呢，我们也要求每一个 骑兵呢，跟他的马呢，是配合的
最后就是我们的目标函数，就是把我们选取的骑兵，他们的
战斗力它的总和，我们加起来之后，我们需要把它最大化
这个就是我们 这个问题里面的数据呢，我们分别有十头马
十一个骑兵，然后每一头马有它的速度 每一个骑兵有他的耐力跟他的战斗力，而且我们也标明了
不同的马跟哪几个骑兵呢，它们是匹配的
然后我们要求我们要做这个阵呢，需要有五头马
好了，我们把我们的模型建好，也把
我们的数据准备好，我们应该可以跑我们的模型呢，就得到我们要求的结果了
一跑出来结果，又是不可以满足 这个，而且呢还有一大堆的警告
到底呢，在哪里出了问题呢？ 其实我们知道呢，有时候我们呢
在建模的时候，我们经常要利用到循环跟
推导式，有时候我们发觉呢，非常难判断我们的循环是在做什么的
所以，我们提议一个非常好的方法 就是我们一起来跟踪一下我们的循环
到底在做什么，好不好？在 MiniZinc 里面呢 我们有一个内建函数叫
trace，帮助我们跟踪 在模型编译的时候可以输出一些信息，来帮助我们去
理解到底在编译的时候发生了什么事情。
这个 trace
这个函数呢 它有两个参数，第一个参数是一个字符串的表达式，另外呢就是一个普通的表达式
它的语义呢就是要输出字符串表达式
的值，然后就返回这个表达式的值 我们利用这个
trace 呢，就可以来观察在模型
展开跟展平这两个编译过程里面，非常主要的步骤里面，看看
到底发生了什么事情了。
所谓是展开呢，就是把一个 循环，它的每一步的迭代
的过程里面，里面的内容一一地列出来 展平呢，就是把一个复杂的表达式
转化成多条的，而且是更简单的一些的表达式
在这个过程里面，我们就可以利用这个 trace
来帮助我们去理解它们是怎么做展开，怎么做展平了
好了，我们就可以把 trace 呢
加进我们刚才的模型里面，因为最难理解的就是这两个 循环。
我们希望看看这样两个循环里面 到底是什么的约束给列出来呢？
好了，加了 Trace 之后，我们就可以要求这个
MiniZinc 把我们的模型求解了，然后我们就得到下面的输出
啊，还是不可以满足 但是我们发觉有一个地方出了错误
出了什么错误呢？就是你们看，我们要访问这个 h
这个数组 要访问它的元素呢是第六个。
如果你们还记得，我们这个
骑兵阵我们要求的是五个骑兵，所以我们根本就不应该有第六个
马出现的，所以呢，我们这个访问呢 这个数组呢，是越界了。
我们再看看我们的模型 发觉呢，原来是我们第二个循环出了问题
出的问题呢就是，我们在它的 上限的时候停得太晚
所以呢我们就可以做一点点的调整，就是我们 不是到 n ，是到了
n-1 ，就可以把这个问题呢改过了 我们再跑，还是不可以满足
但是我们再看看我们跟踪的输出呢，我们 再发现有另外的问题。
在这里呢，我们要求呢 第三
头马要比第二头马的速度要快 这个非常正常，因为第三头马在第二头马前面的
但是在下面呢，有看见我们要求第二头马的 速度要比第三头马的速度要快。
首先，这个跟上面就是有矛盾的 另外呢，根本就没有可能，第二头马在第三头马的后面
不应该它的速度比前面的马要快的 我们再看清楚呢，在我们的模型里面呢
就是原来我们第二个循环还是有 漏洞，原来我们发现它开始得太早了
所以呢，我们要把它做一点点的调整，要求它 +1
晚一点才开始，就可以把上面这个问题呢 去解决了。
然后我们再跑 终于，我们可以找到一个解了，我们完成做了一个
骑兵阵出来了。
好了 我们做了一个五头马的一个骑兵阵
我们可不可以做一个七头马的骑兵阵呢？ 我们一跑，改一改数据一跑，发现不可以满足的。
这个就是答案 不可以满足。
但是如果我们利用我们刚才这个跟踪输出的一些
信息呢，我们看清楚好像在这个两个循环里面都没有发生问题，原来呢
我们的模型呢 根据现在的数据呢，是真的是没有解的
好了，我们来一个小结 我们之前也有提过，我们建模的时候经常用到这个
循环跟这个推导式 而且呢，它们有时候是非常难去理解的
所以呢，当你不确定你对你的推导式还是你的循环
你是否对它要做的事情是理解的话，我们建议你们应该用到 trace
在 MiniZinc 里面呢，在任何可以用表达式的地方我们都可以用
trace 这个 trace 这个内建的函数呢，对我们理解我们的模型
跟它的编译过程呢是非常宝贵的。
但是有一件事情呢就是 你们不应该期望它可以帮你们把你们模型
里面所有的漏洞跟所有的错误都可以帮你们找出来，这个 期望是不合理的
[空白_录音]
Prof. Jimmy Ho Man LeeProfessor
Prof. Peter James StuckeyProfessor
