将项目分配给具有功能的组

如何解决将项目分配给具有功能的组

我在将变量分配给集合时遇到问题。每个集合都有一个可以分配给它的变量限制，每个变量可以分配给总集合的某些子集。

示例：

• 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的内置支持以声明的方式构造更复杂的约束。