有条件的约束解决

Question

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

• 我有一组整数变量 x [i] ，可以在 [1,4] 范围内仅获取4个
• 值是表单的约束 c＆lt; = x [i] ， x [i]＆lt; = c 和 x [i]＆lt; = x [ j]
• 也有有条件约束，但仅具有“如果 2＆lt; = x [i] ，然后 3＆lt; = x [j] “
• 我想最大程度地减少具有值 3 编辑的变量数量

：因为我有大量（数千）变量，约束和性能很重要，所以我m寻找专用算法，不使用通用约束求解器。

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]

上述编码，可以直接写入连词正常形式（。例如 satinterface 或 bc2cnf 有助于自动化此翻译。

为了最大程度地减少具有值 3 的变量数量，可以构建/建模与数字比较器的计数电路结合使用。

变量 x [i] 具有值 3 ，如果（x2 [i]和！x1 [i]）是正确的。这些表达式可以是计数器的输入。然后可以将计数结果与一些值进行比较，该值将减少，直到找不到更多解决方案为止。

底线：
可以使用通用求解器来解决该问题https://github.com/arminbiere/cadical“ rel =“ nofollow noreferrer”> cadical ，， cryptominisat ）或像 minizinc 。我不知道有一种专用算法，该算法的表现会优于通用求解器。

Answer 2

实际上，对于此特定问题，有一种相当简单有效的算法。
当下限变为＆gt; = 2 时，维持和传播间隔并开始传播条件约束就足够了。
最后，如果间隔完全 [3,4] ，最佳解决方案是选择 4 。

更准确地说：

• 初始化 l [i]：= 1 ， u [i]：= 4
• 传播约束，直到fixpoint如下：
  • 约束“ c＆lt; = x [i] “： l [i]：= max（l [i]，c）
  • 约束“ x [i]＆lt; = c “： u [i]：= min（u [i]，c）
  • 约束“ x [i]＆lt; = x [j] “： l [j]：= max（l [j]，l [i]））和 u [i]：= min（u [i]，u [j]）
  • 约束 2＆lt; = x [i] ==＆gt; 3＆lt; = x [j] ：如果 2＆lt; = l [i] ，然后 l [j]：= max（l [j]，3）
• 如果 u [i]＆lt; l [i] ，则没有解决方案
• ，否则请选择：
  • x [i] = l [i] 如果 u [i]＆lt; = 3
  • x [i] = u [i] 否则

否则是正确且最佳的，因为：

• 任何解决方案都以至于 l [i]＆lt; = x [i]＆lt; = u [i] ，因此，如果 u [i]＆lt; l [ i] ，没有解决方案
• ，否则 x [i] = l [i] 显然是一种解决方案（但不是 x [i] = u [i] 因为可以是 u [i]＆gt; = 2 ，但 u [j] 不是＆gt; = 3
• ） 到 4 在可能的情况下仍然是解决方案
• x [i] 从 3 被迫为 3 的变量（ l [i] = u [i] = 3 ），因此我们找到了一个解决方案，该解决方案的最小数量 3

在更多详细信息中，这是一个完整的证明：

• 假设解决方案 x [i] 使得 l [i]＆lt; = x [i]＆lt; = u [i] ，让我们证明通过应用任何传播规则来保留此不变性：
  • 约束“ x [i]＆lt; = x [j] “： x [i]＆lt; = x [j]＆lt; = u [j] 因此 x [i] 既是＆lt; = u [i] and ＆lt; = u [j] ，因此＆lt ; = min（u [i]，u [j]）。同样， l [i]＆lt; = x [i]＆lt; = x [j] so max（l [i]，l [j]）＆lt; = x [j]
  • 约束“ x [i]＆lt; = c “和” c＆lt; = x [i] “相似
  • 对于约束“ 2＆lt; = x [i] ==＆gt; 3＆lt; = x [j] “： l [i]＆lt; 2 和传播规则不应用或 2＆lt; = l [i] ，然后 2＆lt; = l [i]＆lt; = x [i] 暗示 3＆lt ; = x [j] 。 3＆lt; = x [j] 和 l [j]＆lt; = x [j] 因此 max（3，l [j]）＆lt; = = x [j]
• 结果， 当达到fixpoint并且无法应用不再应用规则时，如果任何 i 是如此，那么 u [i]＆lt; l [i ] ，然后没有解决方案
• ，否则，让我们证明此 x [i] 是一个解决方案，其中： x [i] = l [i] 如果 u [i]＆lt; = 3 和 x [i] = u [i] 否则：否则：
  • 请注意， X [i] 是 l [i] 或 u [i] ，所以 l [i] ＆lt; = x [i]＆lt; = u [i]
  • 对于所有约束，“ c＆lt; = x [i] ”，在fixpoint，我们有 l [i] = max（l [i]，c），即， c＆lt; = l [i]＆lt; = x [i] ，并且满足约束
  • 对于所有约束，“ x [i]＆lt; = c ”，在FIXPOINT上，我们同样具有 u [i]＆lt; = C and code> x [i]＆lt; = u [i]＆lt; = c ，并且满足约束
  • 对于所有“ x [i]＆lt; = x [j] '，在fixpoint上，我们有： u [i] = min（u [i]，u [j ]） so u [i]＆lt; = u [j] 和 l [j] = max（l [j]，l [i]） ，因此 l [i]＆lt; = l [j] 。然后：
    • 如果 u [j]＆lt; = 3 然后 u [i]＆lt; = u [j]＆lt; = 3 so x [i] = l [i]＆lt; = l [j] = x [j]
    • 否则， x [j] = u [j] 和 x [i]＆lt; = u [i]＆lt; = u [j] = x [j]

    


    


  • 对于所有“ 2＆lt; = x [i] ==＆gt; 3＆lt; = x [j] “：假设 2＆lt; = x [i] ：
    • 如果 u [i]＆lt; = 3 ，则是：
      • l [i]＆lt; = 2 ，fixpoint表示 l [j]：= max（l [j]，3） so 3＆lt; = l [j]＆lt; = x [j]
      • 或 l [i] = 3 和 3 = l [i]＆lt; = l [j]＆lt; = x [j]
    • 如果 u [i]＆gt; 3 ，则 3＆lt; u [i]＆lt; = u [j] and 3＆lt; u [i] ＆lt; = u [j] = x [j]

  


• 最后该解决方案是最佳的，因为：
  • 如果 l [i] = u [i] = 3 ，任何解决方案都必须具有 x [i] = 3
  • 否则， x [i]！= 3 ：如果 u [i]＆lt; = 3 ，那么 u [i] = 3 和 x [i] = l [i]＆lt; 3 或 x [i]＆lt; = u [i]＆lt; 3 ;如果 u [i]＆gt; 3 然后 x [i] = u [i]！= 3