制約プログラミングで勉強会のグループ分けを最適化した

はじめに

駅奪取チームの id:konakawa です。

モバイルファクトリーでは、前年度と今年度の新卒で行う新卒同期勉強会というものがあります。 この会は参加者を何人かずつのグループに分けて行うのですが、その組み合わせについて

• 毎回同じ人と一緒になっている気がする
• 職種が偏ってしまうことがある
• 社会人年数も偏らないようにしたい

といった偏りの問題を抱えていました。

これまでは人力で頑張って組み合わせを作っていましたが、上記条件を可能な限り満たす組み合わせを考えようとすると非常に手間がかかります。 去年は AI に組み合わせの作成をお願いしましたが、偏りの問題をうまく解決することは難しそうでした。

今回はこの会の組み合わせを CP-SAT ソルバー の力を借りて作成した話になります。

問題について

この問題は Social Golfer Problem (SGP) と呼ばれる問題に非常に似ています。

SGP とは、簡単には以下のような問題です。

何人かのゴルファーが、複数週にわたって定期的にゴルフをプレイする。各週、全員がいくつかの同じ人数のグループに分かれてプレイする。このとき、同じペアのゴルファーが 2 回以上同じグループでプレイしないようなスケジュールを組みたい。

SGP は SAT (satisfiability problem, 充足可能性問題) と呼ばれる問題に帰着できることが知られており、SAT は NP 完全であることが示されています。 すなわち、SGP は

• 解を見つけることは多項式時間でできるかわからない
• 解の候補が実際に解かどうか検証することは多項式時間でできる

ような問題です。

「解の候補が実際に解かどうか検証することは多項式時間でできる」ため、この「解の候補」の探し方を上手くやれば、現実的な時間で解の 1 つが見つかるかもしれません。

一方、新卒同期勉強会の組み合わせを考える問題は、これに制約を加えて拡張したものと捉えられそうです。

今年度は、満たしたい制約を以下のように定めました。

• 任意のペアが同じグループになる回数を均等にする
• グループの全員が同じ職種にならない
• 25 卒が 3 人以上同じグループにならない
• 任意の 3 人組が 2 回連続で同じグループにならない
• 任意の 2 人組が 3 回連続で同じグループにならない

「開催回」「参加者」「グループ」をそれぞれインデックスにもち、ある開催回である参加者があるグループに属するかどうか表す真偽値型配列 assignments[times_meeting][member][group] を用意してやれば、上記の制約は全て assignments を用いた線形な不等式で書くことができます。

例えば、任意の 3 人組が 2 連続で同じグループにならないことは

# 参加者1・参加者2・参加者3が1回目と2回目の勉強会でグループ1にならない
  assignments[1][1][1] + assignments[1][2][1] + assignments[1][3][1]
+ assignments[2][1][1] + assignments[2][2][1] + assignments[2][3][1] < 6
,
# 参加者1・参加者2・参加者3が1回目と2回目の勉強会でグループ2にならない
  assignments[1][1][2] + assignments[1][2][2] + assignments[1][3][2]
+ assignments[2][1][2] + assignments[2][2][2] + assignments[2][3][2] < 6
,
...

のような線形不等式で表すことができます。

真偽値の変数のみからなる不等式制約を充足する解が存在するか という問題を 0-1 ILP (Integer Linear Programming) と呼びます。 任意の SAT の問題は 0-1 ILP に帰着できることが知られており、 SGP を真偽値の線形不等式制約で拡張した今回の問題は 0-1 ILP に属すると言えそうです。

0-1 ILP も NP 完全であることが知られており、すなわち上手く解の候補を探すことができれば現実的な時間で解が見つかるかもしれません。

制約プログラミング

このような問題を解決するプログラミングパラダイムとして、制約プログラミング (CP, Constraint Programming) が存在します。 制約プログラミングは、問題を変数とその変数の制約という形で記述し、その制約を満たす解を見つける手法です。

記述した制約を専用のソルバーに渡すと、「上手く解の候補を探す」部分をやってくれます。 今回は Google が提供している CP-SAT ソルバー を使用しました。

CP-SAT ソルバー は C++, C#, Java, Python に提供されていて、今回は Python で制約プログラミングを行いました。

CP-SAT ソルバーを用いた制約プログラミングでは、比較的直観的に制約を記述していけます。

先ほど線形不等式の例で取り上げた、任意の 3 人組が 2 連続で同じグループにならない制約を用いて、コード例を記載します。

from ortools.sat.python import cp_model

model = cp_model.CpModel()

TOTAL_MEETINGS = 10
TOTAL_GROUPS   = 3
GROUP_SIZE     = 4

# name は仮名
MEMBERS = [
  {'name': 'ito',       'role': 'planner'},
  {'name': 'kato',      'role': 'developer'},
  {'name': 'kobayashi', 'role': 'designer'},
  {'name': 'nakamura',  'role': 'planner'},
  {'name': 'saito',     'role': 'developer'},
  {'name': 'sato',      'role': 'designer'},
  {'name': 'suzuki',    'role': 'planner'},
  {'name': 'takahashi', 'role': 'developer'},
  {'name': 'tanaka',    'role': 'designer'},
  {'name': 'watanabe',  'role': 'planner'},
  {'name': 'yamada',    'role': 'developer'},
  {'name': 'yoshida',   'role': 'designer'},
]

TOTAL_MEMBERS = len(MEMBERS)

# 論理変数: assignments[meeting_idx][member_idx][group_idx] = その回でそのメンバーがそのグループにいるかどうか
assignments = [[[None for _ in range(TOTAL_GROUPS)] for _ in range(TOTAL_MEMBERS)] for _ in range(TOTAL_MEETINGS)]
for meeting_idx in range(TOTAL_MEETINGS):
  for member_idx in range(TOTAL_MEMBERS):
    for group_idx in range(TOTAL_GROUPS):
      assignments[meeting_idx][member_idx][group_idx] = model.NewBoolVar(f'a_{meeting_idx}_{member_idx}_{group_idx}')

# 任意の3人組が2連続で同じグループにならない
for member_i in range(TOTAL_MEMBERS):
  for member_j in range(member_i + 1, TOTAL_MEMBERS):
    for member_k in range(member_j + 1, TOTAL_MEMBERS):
      # 連続するミーティングをチェック
      for meeting_idx in range(TOTAL_MEETINGS - 1):
        for group_idx in range(TOTAL_GROUPS):
          # 今回のミーティングで3人が同じグループにいる
          current_meeting_trio = model.NewBoolVar(f'trio_m{meeting_idx}_g{group_idx}_{member_i}_{member_j}_{member_k}')
          model.AddBoolAnd([
            assignments[meeting_idx][member_i][group_idx],
            assignments[meeting_idx][member_j][group_idx],
            assignments[meeting_idx][member_k][group_idx]
          ]).OnlyEnforceIf(current_meeting_trio)
          model.AddBoolOr([
            assignments[meeting_idx][member_i][group_idx].Not(),
            assignments[meeting_idx][member_j][group_idx].Not(),
            assignments[meeting_idx][member_k][group_idx].Not()
          ]).OnlyEnforceIf(current_meeting_trio.Not())

          # 次回のミーティングで3人が同じグループにいる
          next_meeting_trio = model.NewBoolVar(f'trio_m{meeting_idx+1}_g{group_idx}_{member_i}_{member_j}_{member_k}')
          model.AddBoolAnd([
            assignments[meeting_idx + 1][member_i][group_idx],
            assignments[meeting_idx + 1][member_j][group_idx],
            assignments[meeting_idx + 1][member_k][group_idx]
          ]).OnlyEnforceIf(next_meeting_trio)
          model.AddBoolOr([
            assignments[meeting_idx + 1][member_i][group_idx].Not(),
            assignments[meeting_idx + 1][member_j][group_idx].Not(),
            assignments[meeting_idx + 1][member_k][group_idx].Not()
          ]).OnlyEnforceIf(next_meeting_trio.Not())

          # 両方が同時にTrueになることを禁止
          model.AddBoolOr([
            current_meeting_trio.Not(),
            next_meeting_trio.Not()
          ])

このような形で一通り制約を記述して、ソルバーに解を探してもらうと、数秒から 1 分程度の現実的な時間で上記制約を全て満たす組み合わせを見つけることができました！

=== 第1回 ===
- グループ1: yamada (developer), yoshida (designer), watanabe (planner), kato (developer)
- グループ2: tanaka (designer), ito (planner), saito (developer), kobayashi (designer)
- グループ3: suzuki (planner), takahashi (developer), sato (designer), nakamura (planner)

=== 第2回 ===
（以下省略）

制約の追加

この方法であれば途中で条件が変わっても、制約を追加して再度問題を解くことで解決することができます。

例えば、初回の勉強会を実施した後に、トータルの開催回数が増えたとします。 この場合、「初回の組み合わせが特定のものである」という制約を追加した上で、開催数を増やして再度プログラムを実行することで、既に開催されたものを考慮した上で全体の偏りをなくした組み合わせを見つけることができます。

また、司会やタイムキーパーの回数を均等にするなど、更に制約を追加して拡張することもできそうです。

まとめ

毎年組み合わせの作成が課題になっていた勉強会について、制約プログラミングで問題を解決し、最適な組み合わせを見つけることができました。 制約プログラミングの手法であれば、将来的な拡張も行える上、機械に組み合わせ作成を任せるので時間もかかりません。

似たような問題に遭遇したら、ぜひ制約プログラミングのことを思い出してみてください！