条件约束求解

Question

您将如何处理以下约束优化问题：

• 我有一组整数变量x[i]，它只能在[1,4]范围内取 4 个值
• 有形式C <= x[i]、x[i] <= C和x[i] <= x[j]形式的约束
• 也有条件约束，但仅限于"如果2 <= x[i]则3 <= x[j]">
的形式
• 我想尽量减少具有值3的变量的数量

编辑：因为我有大量(数千)变量和约束，并且性能至关重要，所以我正在寻找专用算法，而不是使用通用约束求解器。

Answer 1

您可以将每个变量编码为一对二进制变量：

x[i] = 1 + 2*x2[i] + x1[i]

不平等约束现在可以部分解决：

1 <= x[i]   can be ignored, as always true for any variable
2 <= x[i]   implies (x2[i] or x1[i])
3 <= x[i]   implies x2[i]
4 <= x[i]   implies (x2[i] and x1[i])
1 >= x[i]   implies (!x2[i] and !x1[i])
2 >= x[i]   implies !x2[i]
3 >= x[i]   implies (!x2[i] or !x1[i])
4 >= x[i]   can be ignored, as always true for any variable
x[i] <= x[j] implies (!x2[i] or x2[j]) and 
(!x1[i] or x2[j] o x1[j]) and
(!x2[i] or !x1[i] or x1[j])

条件约束

if 2 <= x[i] then 3 <= x[j]

翻译为

x2[j] or !x1[i]

上面显示的编码可以直接编写为适合 SAT 求解器的合取范式 (CNF)。SATInterface或bc2cnf等工具有助于自动化此翻译。

为了尽量减少具有值3的变量的数量，可以构建/建模一个计数电路和一个数字比较器。

变量x[i]的值3，如果(x2[i] and !x1[i])为真。这些表达式可以是计数器的输入。然后可以将计数结果与某个值进行比较，该值会减小，直到找不到更多的解决方案。

底线：
这个问题可以用像SAT求解器(CaDiCal，Z3，Cryptominisat)这样的通用求解器或像Minizinc这样的约束求解器来解决。我不知道有哪种专用算法会胜过通用求解器。

Answer 2

实际上，对于这个特定问题，有一个相当简单有效的算法。 维护和传播区间并在下限变得>= 2时开始传播条件约束就足够了。 最后，如果区间正好[3,4]，最优解是选择4。

更准确地说：

• 初始化l[i]:=1，u[i]:=4
• 将约束传播到定点，如下所示：
  • 约束 "C<=x[i]"：l[i]:=max(l[i],C)
  • 约束 "x[i]<=C"：u[i]:=min(u[i],C)
  • 约束"x[i]<=x[j]"：l[j]:=max(l[j],l[i])和u[i]:=min(u[i],u[j])
  • 约束2<=x[i] ==> 3<=x[j]：如果2<=l[i]，则l[j]:=max(l[j], 3)
• 如果u[i]<l[i]，则没有解决方案
• 否则，请选择：
  • x[i]=l[i]如果u[i]<=3
  • x[i]=u[i]否则

这是正确和最佳的，因为：

• 任何解决方案都是这样的l[i]<=x[i]<=u[i]，所以如果u[i]<l[i]，则没有解决方案
• 否则，x[i]=l[i]显然是一个解决方案(但不x[i]=u[i]因为它可能是u[i]>=2但u[j]不是>=3)
• 尽可能将所有x[i]从3提升到4仍然是一种解决方案，因为此更改不会激活任何新的条件约束
• 剩下的是被迫3的变量(l[i]=u[i]=3)，因此我们找到了3数量最少
的解决方案

更详细地说，这里有一个完整的证明：

• 假设解决方案x[i]是这样的，l[i]<=x[i]<=u[i]，让我们证明通过应用任何传播规则来保持这种不变性：
  • 约束 "x[i]<=x[j]"：x[i]<=x[j]<=u[j]等x[i]既<=u[i]又<=u[j]，因此<=min(u[i],u[j])。同样，l[i]<=x[i]<=x[j]如此max(l[i],l[j])<=x[j]
  • 约束 "x[i]<=C" 和C<=x[i]" 相似
  • 对于约束"2<=x[i] ==> 3<=x[j]"：要么l[i]<2并且传播规则不适用，要么2<=l[i]然后2<=l[i]<=x[i]暗示3<=x[j]。因此3<=x[j]和l[j]<=x[j]max(3,l[j])<=x[j]
• 结果，当达到固定点并且无法再应用任何规则时，如果任何i是这样的u[i]<l[i]，那么就没有解决方案
• 否则，让我们证明此x[i]是一个解决方案，其中：x[i]=l[i]如果u[i]<=3，否则x[i]=u[i]：
  • 请注意，x[i]要么是l[i]要么是u[i]，所以l[i]<=x[i]<=u[i]
  • 对于所有约束 "C<=x[i]"，在固定点，我们有l[i]=max(l[i],C)，即C<=l[i]<=x[i]并且约束满足
  • 对于所有约束 "x[i]<=C"，在固定点，我们同样具有u[i]<=C和x[i]<=u[i]<=C并且约束满足
  • 对于所有"x[i]<=x[j]"，在固定点，我们有：u[i] = min(u[i],u[j])如此u[i]<=u[j]和l[j] = max(l[j],l[i])，如此l[i]<=l[j]。然后：
    • 如果是u[j]<=3那么u[i]<=u[j]<=3如此x[i]=l[i]<=l[j]=x[j]
    • 否则，x[j]=u[j]和x[i]<=u[i]<=u[j]=x[j]
  • 对于所有 "2<=x[i] ==> 3<=x[j]"：假设2<=x[i]：
    • 如果u[i]<=3，则任一项：
      • l[i]<=2和固定点意味着l[j]:=max(l[j], 3)如此3<=l[j]<=x[j]
      • 或l[i]=3和3=l[i]<=l[j]<=x[j]
    • 如果u[i]>3，则3<u[i]<=u[j]并3<u[i]<=u[j]=x[j]
• 最后，解决方案是最佳的，因为：
  • 如果l[i]=u[i]=3，任何解决方案都必须具有x[i]=3
  • 否则，x[i] != 3：如果u[i]<=3，则u[i]=3x[i]=l[i]<3或x[i]<=u[i]<3;如果u[i]>3则x[i]=u[i]!=3