我正在使用 Gecode 来解决一个问题,即您标记多向图的弧,以便从单个源到单个接收器的每条路径中的弧标签的总和来自一个多重集。例如,我们可能有一个包含 8 条路径的图,并且希望路径弧和来自集合 {5,5,5,4,3,2,1,0}。所以我们必须恰好有 3 条路径之和为 5 和 5 条路径之和为 0..4。
您可以将此问题重新表述为询问 {5,5,5,4,3,2,1,0} 的某些排列是否在图的路径弧关联矩阵的列空间中。我用“计数”约束对这个多集匹配进行建模。弧和是线性方程。
我的图表有许多成对出现的平行边。使用对称性,我使用它对路径总和施加偏序。这也意味着存在具有相同差异的多对路径和。所以从我的例子中,如果路径是 b0...b7 我有以下对集:
b0 - b1 = b3 - b4 = b5 - b6,b0 - b2 = b5 - b7,b0 - b3 = b1 - b4,b0 - b5 = b1 - b6 = b2 - b7
b1 - b2 = b6 - b7,b3 - b5 = b4 - b6
将这些差异包含在模型中似乎将 Gecode 中的搜索空间减少了两个数量级。我对此感到满意,因为我认为它告诉我一些关于我正在研究的图表的重要信息,并且它符合我工作领域的一些猜想。
偏序现在告诉我们只有 b0,b2,b3,b5 和 b7 可以取值 5。现在可以证明这个系统不能满足。我对约束满足等技术感兴趣,这些技术可用于分析不等式系统(!=)以及“计数”。显然,Gecode 可以通过赋值和失败来证明这一点。我对一般技术感兴趣,既可以了解约束满足,也可以帮助改进模型,并可能对我正在调查的事情有所了解。
要看到这个问题是不可解的,我们可以证明 6 组对差系统中的每一个都不能有零差。如果他们这样做了,他们会生成错误值的重复项或太多的 5。
例如 b0 - b1 = b3 - b4 = b5 - b6 将有 b0 = b1 这是不可能的,因为 b1 不能是 5,这是唯一可以有重复的值。或者 b0 - b2 = b5 - b7 意味着 b0 = b2 和 b5 = b7 需要 4 个 5。
所以我们最终得到了一组路径上的不等式,其总和可能为 5:
b0 != b2, b0 != b3, b0 != b5, b2 != b7, b5 != b7
我们可以看到 b0 != 5 因为如果是,我们只能得到 2 个五。从剩下的 4 个值中,我们被迫最多可以设置 2 到 5,因此整个系统是不可解决的。