问题描述
我在将变量分配给集合时遇到问题。每个集合都有一个可以分配给它的变量限制,每个变量可以分配给总集合的某些子集。
示例:
-
a
可以位于A
或B
组中
-
b
可以放在集合B
中
-
c
可以位于A
或B
组中
-
d
可在集合A
中
因此,我们可以有A: a,d; B: b,c
或A: c,d; B: a,b
(集合中变量的顺序无关紧要)。
我目前正在使用z3(在此处使用Solve编写,也可以使用Solver表示)进行以下操作。通过以下代码,如果a_in_A = True
,则变量a
在集合A
中。
solve(If(a_in_B,1,0) + If(b_in_B,0) + If(c_in_B,0) <= 2,If(a_in_A,0) + If(c_in_A,0) + If(d_in_A,0) + If(a_in_B,0) == 1,If(b_in_B,If(c_in_A,If(d_in_A,0) == 1)
我可以对集合中的变量进行加权,如下所示。在这种情况下,尽管可以扩展,但只剩下A: a,c
作为解决方案。
solve(If(a_in_B,4,3,0) <= 6,0) <= 7,0) == 4,0) == 3,0) == 3)
但是,我还想输入c
之后的一组其他功能,例如a
。因此,我们将简化为A: a,c
的解决方案。如何将这些要求添加到z3求解器表达式中(或完全使用其他方式)?
解决方法
与任何编程任务一样,可以有很多方法来解决此问题。我认为以下是z3py中最惯用的方法。请注意内部Set
类型的使用,该类型在内部由数组建模。我选择整数作为集合的元素,但是如果愿意,可以将其设为枚举类型(或其他一些基本类型):
from z3 import *
s = Solver()
a,b,c,d = Ints('a b c d')
allElems = [a,d]
s.add(Distinct(allElems))
# We have 2 sets
A,B = Consts ('A B',SetSort(IntSort()))
allSets = [A,B]
# Generic requirement: Every element belongs to some set:
for e in allElems:
belongs = False;
for x in allSets:
belongs = Or(belongs,IsMember(e,x))
s.add(belongs)
# Capacity requirements
sizeA,sizeB = Ints('sizeA sizeB')
s.add(SetHasSize(A,sizeA))
s.add(SetHasSize(B,sizeB))
s.add(sizeA <= 2)
s.add(sizeB <= 2)
# Problem specific requirements:
s.add(Or(IsMember(a,A),IsMember(a,B)))
s.add(IsMember(b,B))
s.add(Or(IsMember(c,IsMember(c,B)))
s.add(IsMember(d,A))
# c must be in a set that's after a's set
s.add(Implies(IsMember(a,B)))
s.add(Not(IsMember(a,B))) # otherwise there wouldn't be a place to put c!
r = s.check()
if r == sat:
print(s.model())
else:
print("Solver said: " + r)
请注意如何使用sizeA
,sizeB
变量说明基数/容量要求。您可以泛化并编写您的辅助函数,以自动完成大多数操作。
您最初的问题定义比较模棱两可,但我希望以上内容为您提供了如何进行的想法。特别是,我们可以很容易地表达出c
属于一个集合a
之后的要求,因为我们只有两个集合:
s.add(Implies(IsMember(a,B))) # otherwise there wouldn't be a place to put c!
但是,如果您有两个以上的集合,则可能需要编写一个遍历这些集合的辅助函数(就像我在“通用需求”部分所做的那样)以使此过程自动化。 (从本质上讲,如果A
位于特定集合中,则c
位于“后”集合之一中。当进入最后一个集合时,您需要说出{ {1}}不在其中,否则将没有放置a
的位置。)
当我运行上述程序时,它会打印:
c
这可能有点难以理解,但是您很快就会习惯它!重要部分是:
[A = Lambda(k!0,Or(k!0 == 1,k!0 == 4)),b = 5,a = 1,d = 4,sizeB = 2,c = 3,sizeA = 2,B = Lambda(k!0,Or(k!0 == 3,k!0 == 5)),Ext = [else -> 5]]
上面应该是不言自明的。由于我们想用整数表示元素,因此z3选择了这些元素。 (请注意,我们说a = 1
b = 5
c = 3
d = 4
是为了确保它们不相同。)如果需要,可以在此处使用枚举排序。
下一部分是集合Distinct
和A
的表示形式:
B
这是说A = Lambda(k!0,
包含元素A
和1
(即4
和a
),而d
包含元素B
和3
(即5
和b
)。您通常可以忽略c
部分和看起来很有趣的Lambda
符号,并按以下方式读取它:k!0
1
OR
的任何值都属于4
。与此类似,A
。
B
和sizeA
变量应该是不言自明的。
您可以忽略sizeB
值。 z3将其用于内部目的。
希望这向您展示了如何使用对Ext
的内置支持以声明的方式构造更复杂的约束。