为 Sat Solver 中的一组变量编写从 1 到 N 的至少一个赋值的约束答案

【问题标题】：Writing Constraints for At least one assignment from 1 to N to a set of variables in Sat Solver为 Sat Solver 中的一组变量编写从 1 到 N 的至少一个赋值的约束
【发布时间】：2012-09-25 16:03:22
【问题描述】：

我在 sat 求解器的上下文中问这个问题。假设我有 100 个整数变量 x1, x2, x3 ... x100，它们在 1 to N 之间随机分配一个值。我想确保x1 to x100 的至少一个变量应该具有来自1 to N 的每个值。

现在我想在 sat 求解器约束中编码这个问题。由于在编写约束时我不知道值N，所以我很难编写如下代码 -

(assert (x1 = 0 or x2 = 0 or ... x100 = 0))
(assert (x1 = 1 or x2 = 1 or ... x100 = 1))
(assert (x1 = 2 or x2 = 2 or ... x100 = 2))
...
(assert (x1 = N or x2 = N or ... x100 = N))

假设最后，我断言 N 的值为 2，那么上述约束将不起作用。此外，出于性能原因，我不想使用数组或未解释的函数。

更新：

简而言之，约束如下 -

N
（假设 N = 20），那么有 20 个变量，它们可能是从 x_1 到 x_100 中的任何一个，它们是不同的。因此，此约束将确保为从 1 到 N 的每个值分配至少一个变量。
剩余变量 (100-N) 的值可以相互重叠。

谁能给我一些建议？

【问题讨论】：

标签： z3 smt

【解决方案1】：

对于最多 n 个 x_i 变量（随机选择），如何将 Kyle 的答案与 distinct 结合起来？

这将给出一个模型（对于 N = 50 和 100 个 x_i 变量）：

 x = [0 -> 1,
  1 -> 11,
  2 -> 50,
  3 -> 1,
  4 -> 2,
  5 -> 1,
  6 -> 36,
  7 -> 1,
  8 -> 34,
  9 -> 1,
  10 -> 13,
  11 -> 5,
  12 -> 7,
  13 -> 23,
  14 -> 1,
  15 -> 40,
  16 -> 42,
  17 -> 1,
  18 -> 1,
  19 -> 1,
  20 -> 16,
  21 -> 33,
  22 -> 1,
  23 -> 17,
  24 -> 20,
  25 -> 1,
  26 -> 9,
  27 -> 44,
  28 -> 1,
  29 -> 49,
  30 -> 26,
  31 -> 1,
  32 -> 29,
  33 -> 46,
  34 -> 8,
  35 -> 1,
  36 -> 27,
  37 -> 1,
  38 -> 1,
  39 -> 32,
  40 -> 1,
  41 -> 31,
  42 -> 1,
  43 -> 1,
  44 -> 14,
  45 -> 1,
  46 -> 1,
  47 -> 1,
  48 -> 1,
  49 -> 1,
  50 -> 35,
  51 -> 19,
  52 -> 43,
  53 -> 22,
  54 -> 1,
  55 -> 1,
  56 -> 1,
  57 -> 1,
  58 -> 21,
  59 -> 1,
  60 -> 1,
  61 -> 39,
  62 -> 28,
  63 -> 12,
  64 -> 1,
  65 -> 1,
  66 -> 1,
  67 -> 1,
  68 -> 1,
  69 -> 41,
  70 -> 1,
  71 -> 25,
  72 -> 1,
  73 -> 6,
  74 -> 1,
  75 -> 1,
  76 -> 1,
  77 -> 1,
  78 -> 1,
  79 -> 24,
  80 -> 1,
  81 -> 30,
  82 -> 38,
  83 -> 3,
  84 -> 4,
  85 -> 1,
  86 -> 1,
  87 -> 1,
  88 -> 1,
  89 -> 1,
  90 -> 18,
  91 -> 1,
  92 -> 47,
  93 -> 37,
  94 -> 1,
  95 -> 45,
  96 -> 1,
  97 -> 15,
  98 -> 48,
  99 -> 10,
  else -> 1],

这是一个完成此操作的 Z3Py 脚本，假设可以限制前 N 个索引，而不是随机索引（并且使用 x 函数代替常量，因此编写起来更快）：http://rise4fun.com/Z3Py/M3TG

接下来是为一组随机索引执行此操作的代码，但您不能在 Z3Py@Rise 上运行它，因为它不允许使用导入，因此您必须在本地运行它。

from random import *
from z3 import *

x = Function('x', IntSort(), IntSort())

M = 100
N = 50

s = Solver()
idxs = sample(xrange(M),N) # get N random ids from sequence {1,...M}
print idxs

distinctlist = []
for i in range(M):
  s.add(And(x(i) >= 1, x(i) <= N))
  if i in idxs:
    distinctlist.append(x(i))

print distinctlist

s.add(Distinct(distinctlist))

print "checking..."

r = s.check()
print r
if r == sat:
  print s.model()

（请注意，如果您不满足此查询，它可能会超时。）

【讨论】：

感谢您的精彩回答。但是我认为它仍然不是解决方案。这是因为，我可以看到您正在强制 x1 到 x_50 不同，而休息不在乎。但是，我可能希望有一种可能性，即我不知道哪些是不同的，哪些是相同的。我认为这种编码是不可能的。非常感谢！
@Raj 我认为您需要重写您的问题。我们似乎都无法弄清楚全套约束是什么。
我在问题中添加了一个小总结。
我认为在断言中你将不得不以某种方式约束 x_i，以便获得所有分配的值。您可以使用此解决方案和随机生成的 id 向量来（在某种程度上）不确定地分配将受到约束的索引。您可以使用 python 的random.sample(xrange(M),N) 来做到这一点，它从序列 {1,...M} 中获取 N 个随机 id。这是 Z3Py 中的链接（但请注意，您必须在本地运行此脚本，因为 Z3Py 不允许使用导入，这需要 python 随机库）：rise4fun.com/Z3Py/jeZ
这不是我想要的。但是，我会接受它作为答案。谢谢！

【解决方案2】：

使用distinct 谓词。见：http://smtlib.cs.uiowa.edu/theories/Core.smt2

【讨论】：

使用distinct 谓词将确保每个变量都具有唯一值。但是，如果 N 小于 100，则某些变量 will 具有 equal 值。所以我认为，使用distinct 谓词是行不通的。

【解决方案3】：

我会写

(assert (or (and (> x1 0) (<= x1 n))
            (and (> x2 0) (<= x2 n))
            ...same for x3 thru x99...
            (and (> x100 0) (<= x100 n))))

无论n 的值稍后被断言，只要它大于或等于0，它都会起作用。

【讨论】：

这是真的，我就是这样做的。然而，这并不能确保至少有一个变量设置在 1 到 n 之间。想象一下，如果所有变量 x1 到 x100 都被赋值为 1，它就满足条件。但是我希望至少一个变量的每个值都从 1 到 n。