制約充足問題（CSP）― お弁当を食べ終わる順番を決めよう

制約充足問題（CSP）― お弁当を食べ終わる順番を決めよう#

この章で学ぶこと#

この章では、制約充足問題（Constraint Satisfaction Problem、略して CSP）を扱います。

制約充足問題とはどんな問題か
総当たり（全数探索）だと、なぜすぐ手に負えなくなるのか
Z3 を使うと、なぜ楽に解けるのか

出てくるキーワードは「変数」と「制約」の2つだけです。肩の力を抜いて読んでください。

制約充足問題とは#

制約充足問題とは、いくつかの変数に、条件（制約）を満たすように値を決める問題です。

小さな例で考えてみましょう。

5人の子供（A, B, C, D, E）が、順番にお弁当を食べ終わりました。次の話から、食べ終わった順番を決めてください。

A は B より遅く食べ終わったが、C よりは早かった。

D は E より早く食べ終わったが、C よりは遅かった。

この問題では、

変数：5人それぞれが「何番目に食べ終わったか」
制約：「A は B より後」「A は C より前」などの条件

になります。5人の順番を決めて、どの条件も破っていなければ、それが答えです。

条件を整理する#

日本語のままでは考えにくいので、記号で書き直します。

\(X \prec Y\) を「X が Y より先に食べ終わった」とします。

A は B より遅く、C より早い → \(B \prec A \prec C\)
D は E より早く、C より遅い → \(C \prec D \prec E\)

2つをつなげると、\(B \prec A \prec C \prec D \prec E\) という1本の鎖になります。

つまり、求めるものは「この順番を満たす並べ方」です。

まずは総当たりで解いてみる#

一番素直な方法は、ありうる順番を全部作って、条件に合うものだけを残すことです。

5人の並び順は \(5! = 120\) 通りしかありません。全部試しても一瞬で終わります。

from itertools import permutations

kids = ["A", "B", "C", "D", "E"]

# order は「食べ終わった順に並んだ子供の番号」
for order in permutations(range(len(kids))):
    rank = {kids[i]: pos for pos, i in enumerate(order)}   # 各子供の順位
    if rank["B"] < rank["A"] < rank["C"] and rank["C"] < rank["D"] < rank["E"]:
        print(" → ".join(kids[i] for i in order))

B → A → C → D → E

条件を満たす順番は B → A → C → D → E の1通りだけでした。

5人なら一瞬です。では、人数が増えたらどうなるでしょうか。並び順の数は \(n!\) で増えていきます。

import math

for n in [5, 8, 10, 12]:
    print(f"{n:2d}人: {math.factorial(n):,}通り")

 5人: 120通り
 8人: 40,320通り
10人: 3,628,800通り
12人: 479,001,600通り

12人で約4億8千万通りです。1秒に100万通り試せたとしても8分かかります。20人（約2.4×10¹⁸通り）になると、そもそも終わりません。

「全部試す」は、人数が少し増えるだけで使えなくなる方法です。この章の後半で、Z3 がこの壁をどう越えるかを見ます。

補足：`itertools.permutations` について#

総当たりに使った permutations() は、与えた要素のすべての並び順を作る関数です。

itertools.permutations(iterable, r=None)

iterable：並べたい要素
r：何個取り出すか（省略すると全部）

3つの要素なら \(3! = 6\) 通りです。

for p in permutations(["A", "B", "C"]):
    print(p)

('A', 'B', 'C')
('A', 'C', 'B')
('B', 'A', 'C')
('B', 'C', 'A')
('C', 'A', 'B')
('C', 'B', 'A')

permutations() を使うときに気をつけることは3つです。

順序を区別する：(A, B) と (B, A) は別のものとして扱われます。
重複は考えない：同じ要素が入っていると、同じ並びが何度も出てきます。
計算量が \(n!\)：要素が増えると爆発的に増えます。

小さな問題を目で確かめるには便利ですが、大きな問題には向きません。そこでソルバーの出番です。

Z3 で解く#

Z3 は制約ソルバーの1つです。条件をそのまま書くと、条件を満たす値の組み合わせを探してくれます。

総当たりとの違いはこうです。

	やること
総当たり	候補を全部作って、1つずつ確かめる
Z3	条件を書いて、探すのは Z3 に任せる

Z3 で解く手順はいつも同じです。

変数を作る
制約を追加する
解を取り出す

from z3 import IntVector, Solver, Distinct, sat

kids = ["A", "B", "C", "D", "E"]

# 各子供の「食べ終わった順位」を表す5つの整数変数（pos[0] が A、pos[1] が B …）
pos = IntVector("pos", 5)
eat_a, eat_b, eat_c, eat_d, eat_e = pos

solver = Solver()

# 1. 順位は 0〜4 のどれか
for p in pos:
    solver.add(p >= 0, p < len(kids))

# 2. 同じ順位の子供はいない
solver.add(Distinct(pos))

# 3. 問題の条件  B ≺ A ≺ C ≺ D ≺ E
solver.add(eat_b < eat_a, eat_a < eat_c)
solver.add(eat_c < eat_d, eat_d < eat_e)

# 4. 解を取り出して、順位の小さい順に並べる
if solver.check() == sat:
    model = solver.model()
    rank = {kid: model[pos[i]].as_long() for i, kid in enumerate(kids)}
    print(" → ".join(sorted(kids, key=lambda kid: rank[kid])))

B → A → C → D → E

総当たりと同じ答えが出ました。ここで、探索する範囲が少しずつ狭くなっていく様子に注目してください。

IntVector("pos", 5) を作っただけでは、値は何でもよい → 無限
0 <= p < 5 を加える → \(5^5 = 3125\) 通り
Distinct(pos) を加える → \(5! = 120\) 通り（総当たりと同じ範囲）
条件 \(B \prec A \prec C \prec D \prec E\) を加える → 1通り

総当たりは手順3の範囲から始めて、最後まで自分で全部試します。Z3 は条件を先に受け取るので、条件に合わない候補を最初から作らずに済みます。人数が増えても仕組みは同じです。

まとめ#

手法	計算量	向いている場面
`itertools.permutations`	\(O(n!)\)	小さな問題を目で確かめる
Z3	条件から効率よく探索	条件が複雑な問題、人数が多い問題

制約充足問題は「変数」と「制約」でできている
総当たりの計算量は \(n!\) なので、少し大きくなるだけで使えなくなる
Z3 は制約をそのまま書けるので、問題が変わっても対応しやすい