将项目分配给具有特征的组

Question

我有一个问题，我要将变量分配给集合。每个集合都有可以分配给它的变量的限制，并且每个变量都可以分配给总集合的某个子集。

例子：

• 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, 1, 0) + If(c_in_B, 1, 0) <= 2,
      If(a_in_A, 1, 0) + If(c_in_A, 1, 0) + If(d_in_A, 1, 0) <= 2, 
      If(a_in_A, 1, 0) + If(a_in_B, 1, 0) == 1, 
      If(b_in_B, 1, 0) == 1, 
      If(c_in_A, 1, 0) + If(c_in_B, 1, 0) == 1, 
      If(d_in_A, 1, 0) == 1)

我可以对集合中的变量进行加权，如下所示。在这种情况下，我们将只剩下A: a, d; B: b, c 作为解决方案，尽管这可以扩展。

solve(If(a_in_B, 4, 0) + If(b_in_B, 3, 0) + If(c_in_B, 3, 0) <= 6,
      If(a_in_A, 4, 0) + If(c_in_A, 3, 0) + If(d_in_A, 3, 0) <= 7, 
      If(a_in_A, 4, 0) + If(a_in_B, 4, 0) == 4, 
      If(b_in_B, 3, 0) == 3, 
      If(c_in_A, 3, 0) + If(c_in_B, 3, 0) == 3, 
      If(d_in_A, 3, 0) == 3)

但是，我还想在c 等其他特征中输入必须在a 之后的集合。因此，我们将被简化为只有A: a, d; B: b, c 的解决方案。我如何将这些要求添加到 z3 求解器表达式（或完全以其他方式）？

Answer 1

与任何编程任务一样，可以有很多方法来解决这个问题。我认为以下将是在 z3py 中这样做的最惯用的方式。请注意内部Set 类型的使用，该类型在内部由数组建模。我选择整数作为集合的元素，但如果您愿意，可以将其设为枚举类型（或其他一些基本类型）：

from z3 import *

s = Solver()

a, b, c, d = Ints('a b c d')
allElems = [a, b, c, 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, A), 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, A), IsMember(c, 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, A), IsMember(c, B)))
s.add(Not(IsMember(a, B))) # otherwise there wouldn't be a place to put c!

但是如果您有两个以上的集合，您可能需要编写一个遍历集合的辅助函数（就像我在“通用要求”部分中所做的那样）以自动执行此操作。 （基本上，你会说如果A 在一个特定的集合中，那么c 在一个“后来的”集合中。当你来到最后一个集合时，你需要说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]]

这可能有点难以阅读，但您很快就会习惯的！重要的部分是：

a = 1
b = 5
c = 3
d = 4

上面应该是不言自明的。因为我们想用整数表示元素，所以 z3 选择了这些。 （请注意，我们说Distinct 是为了确保它们不一样。）如果需要，您可以在此处使用枚举排序。

下一部分是集合A和B的表示：

A = Lambda(k!0, Or(k!0 == 1, k!0 == 4)),
B = Lambda(k!0, Or(k!0 == 3, k!0 == 5)),

这是说A 包含元素1 和4（即a 和d），而B 包含元素3 和5（即、b 和 c)。您几乎可以忽略Lambda 部分和看起来很有趣的k!0 符号，并按如下方式阅读：任何为1 OR 4 的值都属于A。 B 也是如此。

sizeA 和 sizeB 变量应该是不言自明的。

您可以忽略Ext 值。它被 z3 用于内部目的。

希望这向您展示了如何使用对Sets 的内置支持以声明性方式构建更复杂的约束。