将从1到N的至少一次赋值的约束写入到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< 100
- (假设N= 20)，那么有20个变量可能是从x_1到x_100的任何一个变量，它们是不同的。因此，这个约束将确保每个值从1到N至少有一个变量赋值。
- 剩余变量(100-N)的值可以相互重叠.
有人能给我一些建议吗？
回答 3
Stack Overflow用户
发布于 2012-09-27 15:11:30
如何结合凯尔的答案和不同的，最多n的x_i变量(随机选择)？
这将给出类似的模型(对于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个索引可以被约束，而不是随机的(并且使用一个函数来代替常量，这样写起来就更快了)：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()(请注意，如果您将此查询不放在卫星上，则可能会超时。)
Stack Overflow用户
发布于 2012-09-25 18:18:14
使用distinct谓词。请参阅：http://smtlib.cs.uiowa.edu/theories/Core.smt2
Stack Overflow用户
发布于 2012-09-27 06:24:18
我会写
(assert (or (and (> x1 0) (<= x1 n))
(and (> x2 0) (<= x2 n))
...same for x3 thru x99...
(and (> x100 0) (<= x100 n))))只要n大于或等于0，无论以后断言的是什么值，它都会工作。
https://stackoverflow.com/questions/12586811
复制相似问题
腾讯云开发者
Copyright © 2013 - 2026 Tencent Cloud. All Rights Reserved. 腾讯云 版权所有
深圳市腾讯计算机系统有限公司 ICP备案/许可证号：粤B2-20090059 
粤公网安备44030502008569号
腾讯云计算（北京）有限责任公司 京ICP证150476号 | 京ICP备11018762号