ORTools CP-SAT 求解器。要求从同一组整数中提取两个变量列表的约束

ORTools CP-SAT Solver. Constraint to require two lists of variables to be drawn from the same set of integers

我有两个变量列表 M 和 T。我想创建一个约束,使 M 和 T 之间的一组唯一值相同。

从我想要的解决方案变量:

set(T) == set(M) -> True

到目前为止,我已尝试创建 M 和 T 的每个元素之间的差异矩阵

diffs = M[:, None] - T

然后构建一个约束条件,即 diffs 的每个行和每个单独列中的每个元素的乘积为 0。这应该确保 M 的每个元素在 T 中都有一个元素,它等于和反之亦然。

for m in range(num_groups):
    model.AddMultiplicationEquality(0, diffs[m, :])
for t in range(num_groups):
    model.AddMultiplicationEquality(0, diffs[:, t])

在没有 objective 或其他约束的情况下求解此模型后,我收到无效状态。我是 ORTools 的新手。

完整节目

ortools==9.3.10497

from ortools.sat.python import cp_model
import numpy as np

model = cp_model.CpModel()
num_groups = 4
STATUS  = ['UNKNOWN', 'MODEL_INVALID', 'FEASIBLE', 'INFEASIBLE', 'OPTIMAL']
M = []
for m in range(num_groups):
    M.append(model.NewIntVar(lb=0, ub=num_groups, name=f'M_{m}'))
T = []
for t in range(num_groups):
    T.append(model.NewIntVar(lb=0, ub=num_groups, name=f'T_{t}'))
M = np.array(M)
T = np.array(T)


diffs = M[:, None] - T
for m in range(num_groups):
    model.AddMultiplicationEquality(0, diffs[m, :])
for tt in range(num_groups):
    model.AddMultiplicationEquality(0, diffs[:, tt])

solver = cp_model.CpSolver()
status = solver.Solve(model)
print(STATUS[status])

这是灾难性的。乘法很慢。

只需为每个值创建一个布尔变量,为每个值和每个变量创建一个布尔变量。

现在,您想 link 一切都在一起。

对于任一集合中的变量 x 和值 v:

    assign = {}
    assign[x, v] = model.NewBoolVar(f'assign_{x}_{v}')
    model.Add(x == v).OnlyEnforceIf(assign[x, v])
    model.Add(x != v).OnlyEnforceIf(assign[x, v].Not())

对于值 v:

    appears = {}
    appears[v] = model.NewBoolVar(f'appears_{v}')

    # If v does not appear, no variable can be assigned its value.
    for x in T U M:
        model.AddImplication(appears[v].Not(), assign[x, v].Not())

    # If v appears, at least one variable in both T and M must be assigned to v.
    model.AddBoolOr(assign[x, v] for x in T).OnlyEnforceIf(appears[v])
    model.AddBoolOr(assign[x, v] for x in M).OnlyEnforceIf(appears[v])