求解器："simple" 逻辑问题的 OR-Tools 或 clingo(ASP) 模型

Question

我尝试使用 OR-Tools 或 clingo(ASP) 解决“简单”的逻辑问题。它是这样的：我有一组人，比如 Person(Tony, Bob, Ann, Carl, Amber, Peter) 我还有像 Group1(Bob, Ann, Carl, Amber, Peter)、Group2(Bob, Amber) 和 [=22= 这样的组]组 3（琥珀色）。现在我想 select Group1 中的两个人，Group2 中的一个人和 Group3 中的一个人 - 所以总共有四个人满足所有限制条件。可能的解决方案是 Carl、Ann、Bob、Amber 或 Peter、Ann、Bob、Amber 或 Carl、Peter、Bob , 琥珀色。我怎样才能做到这一点？

编辑：我在 ASP clingo:

中尝试过这个

person(tony; bob; ann; carl; amber; peter).
group1(bob; ann; carl; amber; peter).
group2(bob; amber).
group3(amber).

% rules
{select(X): person(X), group1(X)} = 2.
{select(X): person(X), group2(X)} = 1.
{select(X): person(X), group3(X)} = 1.

#show select/1.

但我只得到：

clingo version 5.5.0
Reading from stdin
Solving...
Answer: 1
select(amber) select(carl)
Answer: 2
select(amber) select(peter)
Answer: 3
select(amber) select(ann)
SATISFIABLE

Models       : 3
Calls        : 1
Time         : 0.004s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time     : 0.000s

感谢和问候

Answer 1

快速破解：

代码

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

# DATA
# ----
names = ['Tony', 'Bob', 'Ann', 'Carl', 'Amber', 'Peter']
matrix = np.array([
  [0, 1, 1, 1, 1, 1],     # group 0 "members": NOT Tony, Bob, Ann, ...
  [0, 1, 0, 0, 1, 0],     # group 1 "members": Bob, Amber      
  [0, 0, 0, 0, 1, 0]      # group 2 "members": Amber
])
cardinalities = [2, 1, 1] # group 0, group 1, group 2

# MODEL
# -----
model = cp_model.CpModel()
# 2d boolean assignment-matrix: person X group picked?
var_assign = np.empty(matrix.shape, dtype=object)
for a in range(matrix.shape[0]):
  for b in range(matrix.shape[1]):
    var_assign[a, b] = model.NewBoolVar('')

# forbid to pick a person from a group without being a "member"
forbidden_picks = np.where(matrix == 0)
for ind, group in enumerate(forbidden_picks[0]):
  model.Add(var_assign[group, forbidden_picks[1][ind]] == 0)

# a person is picked from at most one group
for person in range(matrix.shape[1]):
  model.Add(var_assign[:, person].sum() <= 1)

# a group is picked exactly n times 
for group, group_card in enumerate(cardinalities):
  model.Add(var_assign[group, :].sum() == group_card)

# SOLVE
# -----
class VarArraySolutionPrinter(cp_model.CpSolverSolutionCallback):
    def __init__(self, variables):
        cp_model.CpSolverSolutionCallback.__init__(self)
        self.__variables = variables

    def on_solution_callback(self):
        selected = []
        for g in range(len(cardinalities)):
          for p_ind, p in enumerate(names):
            if self.Value(self.__variables[g][p_ind]) == 1:
              selected.append(p)
        print('Solution: ', selected)

solver = cp_model.CpSolver()
solution_printer = VarArraySolutionPrinter(var_assign.tolist())
status = solver.SearchForAllSolutions(model, solution_printer)

出来

Solution:  ['Ann', 'Carl', 'Bob', 'Amber']
Solution:  ['Ann', 'Peter', 'Bob', 'Amber']
Solution:  ['Carl', 'Peter', 'Bob', 'Amber']

方法

想想一些赋值矩阵：

Tony  Bob  Ann  Carl  Amber  Peter
 -     1    1    1      1      1   = group 0 = 2
 -     1    -    -      1      -   = group 1 = 1
 -     -    -    -      1      -   = group 2 = 1 

 <=1  <=1  <=1  <=1    <=1    <=1

Answer 2

您在 ASP 中完美地阐述了您描述的问题，并且显示了正确的结果。您忘记说明的是，您不想 select 来自两个不同组的同一个人。

我将您的 ASP 程序修改为以下内容：

person(tony; bob; ann; carl; amber; peter).
group1(bob; ann; carl; amber; peter).
group2(bob; amber).
group3(amber).

% select the amount for each group individually
{select(1,X): group1(X)} = 2.
{select(2,X): group2(X)} = 1.
{select(3,X): group3(X)} = 1.

% you are not allowed to select a person in two groups
:- select(G,X), select(G',X), G < G'.

#show .
#show select(X) : select(G,X).

这给出了您预期的答案。

求解器："simple" 逻辑问题的 OR-Tools 或 clingo(ASP) 模型

Solver: OR-Tools or clingo(ASP) model for "simple" logical problem

prolog

solver

answer-set-programming

clingo

or-tools

代码

出来

方法