1

我有一个（可满足的）（线性）整数可满足性问题。除其他外，该问题包含一堆布尔值变量，称它们为 x 1 ...x n，其中一个约束是 sum(x 1 ...x n ) = C。我希望确定哪个这些变量中的一些是固定的，并且所述变量的固定值（如：在所有可能的解决方案中，这些变量中的哪些取特定值（0 或 1，因为它们又是布尔值））。

我有一个可行的解决方案，只是很慢（委婉地说）：

  1. 添加 x 1 == 0的约束
  2. 检查问题是否可以解决
  3. 删除在步骤 1 中添加的约束。
  4. 添加 x 1 == 1的约束
  5. 检查问题是否可以解决
  6. 移除第 4 步中添加的约束
  7. 断言至少 2 和 5 之一成功。
  8. 如果两者都成功，则变量不固定。否则，该变量将固定为问题仍然可以满足的任何约束。
  9. 对 x 2 ...x n重复 1...8

这样做的问题是它很慢。特别是，它需要解决问题 O(n)，或者更确切地说是 2*n 次。（我传递了以前的解决方案来热启动求解器，但只是启动求解器几乎需要所有时间。）

有没有更快的方法？特别是，需要更少调用求解器的次数？

我正在考虑的事情，不幸的是不能按原样工作，是将它变成一个 ILP 问题并解决它两次，一次以最大化 sum(x 1 ...x n) 为目标，一次以最大化 sum(x 1 ...x n ) 为目标最小化相同，并检查哪些变量发生变化。不幸的是，这通常不起作用。对于（反）示例：布尔变量x和y，其中x+y=1。即使两个变量都不是固定的，最大化和最小化也可以产生相同的结果。

4

2 回答 2

2

您在问题中描述的对变量所做的通常在 MILP（混合整数线性规划）社区中被称为探测，不幸的是，理论上没有什么比您能做的更好了。但是，在实践中，您可以加快速度。

正如您在自己的答案中指出的那样，对于每个变量，您可以跟踪您是否在某些解决方案中将该变量视为 False 和 True，并仅测试您以前从未见过的设置。（请注意，您在修复 x_1 时获得的第一个解决方案将为每个变量设置一个 seenFalse 或 seenTrue ，从而将要解决的实例数量减半。）

你可以做更多。当您查看特定实例时（例如，当未设置 seenFalse_i 并且您将 x_i 设置为 False 时），您可以使用随机目标将 ILSAT 转换为 ILP。有一个目标有几个目的

  • 通过在每个实例中使用不同的随机目标，你必须解决希望你能得到各种各样的解决方案，你将能够设置许多可见的……标志。
  • 使用此 ILP 的最优解值和 ILP 的 LP 松弛，您可能能够执行降低的成本固定，即，基于降低的基础布尔变量的成本，您可能能够证明它们可以' t 取除当前值之外的任何其他值，因此可能能够设置更多可见的...标志。
于 2014-06-27T01:39:55.103 回答
0

看起来好像我对自己的问题有一个解决方案。这并不理想，因此我会接受其他答案，但这里有：

  1. 将 ILSAT 变成 ILP。
  2. 对于每个要检查、设置的变量seenTrue以及要检查seenFalse的变量False
  3. 设置目标函数以最大化已经看到但不是的变量总和，减去已经看到False但不是True的变量True总和False。
  4. 解决 ILP。
  5. 如果自上次迭代以来没有任何未知的未知值发生变化，则中断为 8。
  6. 对于解决方案中的每个变量，设置seenTrue或seenFalse至True，具体取决于变量是True还是False。
  7. 转到 2
  8. 对于每个变量，如果它只被视为True或之一False，则该变量固定为该值。否则（它被认为是两者）它不是固定的。

实际上，我所做的总是试图最大化设置为尚未设置的值的变量数量。

于 2014-06-27T01:13:34.237 回答