将项目分配给具有功能的组 [英] Assigning items to groups with features

问题描述

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

I have a problem where I am to assign variables to sets. Each set has a limit of variables that can be assigned to it and each variable can be assigned to some subset of the total sets.

示例:

• a 可以位于 A 或 B
的集合中
• b 可以在集合中 B
• c 可以位于 A 或 B
的集合中
• d 可以位于 A
的集合中

• a can be in sets A or B
• b can be in sets B
• c can be in sets A or B
• d can be in sets A

因此，我们可以得到 A:a，d;B:b，c 或 A:c，d；B:a，b (集合中变量的顺序无关紧要).

Thus, we can have A: a, d; B: b, c or A: c, d; B: a,b (order of variables within set does not matter).

我目前正在使用z3(在此处使用Solve编写，也可以使用Solver表示)进行以下操作.通过以下代码，如果 a_in_A = True ，则变量 a 位于集合 A 中.

I am currently doing the following using z3 (written using solve here, can also be represented using Solver). By the below code, if a_in_A = True then the variable a is in set 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 作为解决方案，尽管可以扩展.

I can weight the variables within the set, such as below. In this case, we would be left with only A: a, d; B: b, c as a solution, although this can be expanded.

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求解器表达式中(或完全使用其他方式)?

However, I would also like to input in other features like c must come in a set after a. Thus, we would be reduced to only the solution of A: a, d; B: b, c. How would I add these requirements to the z3 solver expression (or another way altogether)?

推荐答案

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

As with any programming task, there could be many ways to solve this problem. I think the following would be the most idiomatic way of doing so in z3py. Note the use of the internal Set type, which is modeled internally by arrays. I'm choosing integers as the elements of the sets, though you can make this an enumerated type (or some other base type) if you like:

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 变量说明基数/容量要求.您可以泛化并编写您的辅助函数，以自动完成大多数此类工作.

Note how the cardinality/capacity requirements are stated using sizeA, sizeB variables. You can generalize and write your helper functions to automate most of this stuff.

您最初的问题定义不太明确，但是我希望以上内容为您提供有关如何进行的想法.特别地，我们可以容易地表达出 c 属于集合"after"的要求. a ，因为我们只有两套:

Your original problem definition was rather ambiguous, but I hope the above gives you an idea on how to proceed. In particular, we can easily express the requirement that c belongs to a set "after" a since we have only two sets around:

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 .)

but if you have more than two sets you might want to write a helper function that walks over the sets (much like I did in the "Generic requirement" part) to automate this as well. (Essentially, you'd say if A is in a specific set, then c is in one of the "later" sets. When you come to the last set, you'd need to say a is not in it, as otherwise there would be no place to put c in.)

当我运行上述程序时，它会打印:

When I run the above program, it prints:

[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]]

这可能有点难以理解，但是您很快就会习惯它！重要的部分是:

This can be a bit hard to read, but you'll get used to it in no time! Important parts are:

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

上面应该是不言自明的.由于我们想用整数表示元素，因此z3选择了这些元素.(请注意，我们说了 Distinct 以确保它们不相同.)如果需要，可以在此处使用枚举排序.

Above should be self-explanatory. Since we wanted to represent elements with integers, z3 picked these ones. (Note we said Distinct to make sure they weren't the same.) You can use an enum-sort here if you want.

下一部分是集合 A 和 B 的表示形式:

The next part is the representation of the sets 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 和 4 (即 a 和 d )，而 B 包含元素 3 和 5 (即 b 和 c ).您通常可以忽略 Lambda 部分和看上去很有趣的 k！0 符号，并按以下方式读取它:任何值为 1 OR 4 属于 A .同样，对于 B .

What this is saying is that A contains the elements 1 and 4 (i.e., a and d), while B contains the elements 3 and 5 (i.e., b and c). You can mostly ignore the Lambda part and the funny looking k!0 symbol, and read it as follows: Any value that is either 1 OR 4 belongs to A. And similarly for B.

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

The sizeA and sizeB variables should be self-explanatory.

您可以忽略 Ext 值.z3将其用于内部目的.

You can ignore the Ext value. It's used for internal purposes by z3.

希望这向您展示了如何使用对 Set s的内置支持，以声明的方式构造更复杂的约束.

Hope this shows you how you can structure even more complex constraints in a declarative way using built-in support for Sets.

这篇关于将项目分配给具有功能的组的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！