与任何编程任务一样，可以有多种方法来解决这个问题。我认为以下是 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 in.)
当我运行上面的程序时，它打印：
[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 and 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 and 4 (i.e., a and d）， 尽管B包含元素3 and 5 (i.e., b and c）。你基本上可以忽略Lambda部分和有趣的样子k!0符号，并按如下方式读取：任何值1 OR 4属于A。同样对于B.
The sizeA and sizeB变量应该是不言自明的。
你可以忽略Ext价值。它由 z3 用于内部目的。
希望这向您展示如何使用内置支持以声明性方式构建更复杂的约束Sets.
