如何在ortools中实现除0之外的所有不同约束

Question

我正在使用 ortools，CP-SAT 求解器，并且我正在努力编写一个约束，该约束将允许一个可以有多个零的解决方案，但其余的决策变量值必须是唯一的。所以

alldifferent

但我可以有多个零。 下面是启动代码：

from ortools.sat.python import cp_model as cp
x = [model.NewIntVar(lb=0, ub=10, name = "") for _ in range(5)]
# so if I constrain x[0], x[1] to zero, and maximise the sum of x
# then the objective function value should be = 27 [0, 0, 8, 9, 10]

上面是一个非常简化的版本，但上面的答案将帮助我完成更大的程序。

Answer 1

可以通过以下方式实现：

from ortools.sat.python import cp_model as cp

model = cp.CpModel()
x = [model.NewIntVar(lb=0, ub=10, name = "") for _ in range(5)]

n = len(x)

# list of bin_var corresponding to x's. 
# if bin_var[i] == 1 then x[i] > 0
# if bin_var[i] == 0 then x[i] == 0
bin_var = [model.NewBoolVar("") for i in range(n)]
for i in range(n):
    model.Add(x[i] != 0).OnlyEnforceIf(bin_var[i])
    model.Add(x[i] == 0).OnlyEnforceIf(bin_var[i].Not())


# comparing x[i]'s amongst each other
for i in range(n):
    for j in range(i):
        # we want if bin_var[i] and bin_var[j] are both true
        # then x[i] != x[j]
        bv = model.NewBoolVar("")
        model.AddBoolAnd([bin_var[i], bin_var[j]]).OnlyEnforceIf(bv)
        model.AddBoolOr([bin_var[i].Not(), bin_var[j].Not()]).OnlyEnforceIf(bv.Not())
        model.Add(x[i] != x[j]).OnlyEnforceIf(bv)  

# first 2 x's are 0
model.Add(x[0] + x[1] == 0)

model.Maximize(sum(x))
solver = cp.CpSolver()
status = solver.solve(model)

# investigate solution
print(f"Optimal value = {solver.ObjectiveValue()}") 
# optimal value = 27

print([solver.value(x[i]) for i in range(5)])
# [0, 0, 10, 9, 8]
# position of 8,9,10 are not restricted through any constraints

Answer 2

就像我们对 alldiff 进行间隔扩展一样。

from ortools.sat.python import cp_model

# Model.
model = cp_model.CpModel()

# Declare our primary variable.
x = [model.new_int_var(0, 10, f'x{i}') for i in range(5)]

# Expand the AllDifferentExcept0 constraint.
variables_per_value = collections.defaultdict(list)
all_values = set()

for var in x:
  all_encoding_literals = []
  # Domains of variables are represented by flat intervals.
  for i in range(0, len(var.proto.domain), 2):
    start = var.proto.domain[i]
    end = var.proto.domain[i + 1]
    for value in range(start, end + 1):  # Intervals are inclusive.
      # Create the literal attached to var == value.
      bool_var = model.new_bool_var(f'{var} == {value}')
      model.add(var == value).only_enforce_if(bool_var)

      # Collect all encoding literals for a given variable.
      all_encoding_literals.append(bool_var)

      # Collect all encoding literals for a given value.
      variables_per_value[value].append(bool_var)

      # Collect all different values.
      all_values.add(value)

  # One variable must have exactly one value.
  model.add_exactly_one(all_encoding_literals)

# Add the all_different constraints.
for value, literals in variables_per_value.items():
  if value == 0:
    continue
  model.add_at_most_one(literals)

model.add(x[0] == 0)
model.add(x[1] == 0)

model.maximize(sum(x))

# Create a solver and solve with a fixed search.
solver = cp_model.CpSolver()

# Search and print out all solutions.
status = solver.solve(model)
if status == cp_model.OPTIMAL:
  print(f'Optimal solution: {solver.objective_value}, expected: 27.0')