如何使用 or-tools 在 bool 数组中制作 K 个不同的元素？答案

【问题标题】：how to make K different elements in bool array with or-tools?如何使用 or-tools 在 bool 数组中制作 K 个不同的元素？
【发布时间】：2020-09-28 11:16:01
【问题描述】：

我想在 bool 数组中创建 K 个不同的元素，我使用代码：model.Add(len(set([shifts[(i)] for i in range(10)]))==4) ，但不是工作！我该怎么做？

model = cp_model.CpModel()
solver = cp_model.CpSolver()

shifts = {}
ones = [model.NewBoolVar("") for _ in range(10)]
for i in range(10):
    shifts[(i)] = model.NewIntVar(0, 10, "shifts(%i)" % i)
    
for i in range(10):
    model.Add(shifts[(i)] >0).OnlyEnforceIf(ones[(i)])
    model.Add(shifts[(i)] == 0).OnlyEnforceIf(ones[(i)].Not())
    
model.Add(sum(ones[(i)] for i in range(10)) == 5)

# I want make 4 different but it not work!
#model.Add(len(set([shifts[(i)] for i in range(10)]))==4)

status = solver.Solve(model)
print("status:",status)

res=[]
for i in range(10):
        res.append(solver.Value(shifts[(i)]))
print(res)

【问题讨论】：

我认为你应该使用所有布尔值而不是 intvars（例如：shifts[i, 0], ... shifts[i, 10]）
您需要了解set([shifts[(i)] for i in range(10)]))==4 根本不会构建您所期望的。 shifts[(i)] 永远不能被评估为 True 或 False。它的值可以在搜索期间分配，但是 (1) 这可以使用专用 API 进行查询，并且 (2) 它是延迟的，而您的 python 代码将简单地假设shifts[(i)] 是一个对象，因此总是True。
嗨，@Laurent Perron：2年前，你回答了一个问题：link，当时你说：“只需为每个x[i] == j创建bool vars，然后有value[j] = max(x[i] == j)，然后 sum(value[j]) >= 2。这适用于 CP-SAT。在这种情况下，max 可以通过隐含和一个大子句来实现."，能不能具体点？谢谢！！！

标签： or-tools

【解决方案1】：

使用布尔值对整数进行编码，并为每个值添加另一个布尔值以将其标记为已使用

from ortools.sat.python import cp_model

model = cp_model.CpModel()
solver = cp_model.CpSolver()

shifts = {}
used = [model.NewBoolVar("") for j in range(10)]
for i in range(10):
    for j in range(10):
        shifts[i, j] = model.NewBoolVar(f"shifts({i}, {j})")
        # shifts[i,j] => used[j]
        model.AddImplication(shifts[i, j], used[j])
    model.Add(sum(shifts[i, j] for j in range(10)) == 1)

model.Add(sum(shifts[i, 0].Not() for i in range(10)) == 5)

for j in range(10):
    # all(shifts[_, j] == 0) => used[j].Not()
    model.AddBoolOr([shifts[i, j] for i in range(10)] + [used[j].Not()])

model.Add(sum(used) == 4)

status = solver.Solve(model)
print("status:", status)

res = []
for i in range(10):
    for j in range(10):
        if solver.Value(shifts[i, j]):
            res.append(j)
print(res)

【讨论】：

嗨，@Stradivari：非常感谢您的帮助！