制約充足問題

制約充足問題#

制約充足問題（Constraint Satisfaction Problem, CSP）とは、変数に対して制約を満たすように値を割り当てる問題のことです。例えば、次のような問題があります。

5人の子供（A, B, C, D, E）が順番にお弁当を食べ終わります。
以下の制約を満たすように、食べ終わる順番を決めてください。

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

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

この条件を整理すると、以下の関係が得られます。

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

ここで、\( X \prec Y \) は「XがYよりも前に食べ終わった」ことを意味します。

permutationsでの全数調査#

まず、Pythonのitertools.permutationsを使って、すべての順列（5! = 120通り）を生成し、条件を満たすものを探してみます。

from itertools import permutations

# 5人の子供
kids = ["A", "B", "C", "D", "E"]

# 条件を満たす順列を探す
for order in permutations(range(len(kids))):
    a, b, c, d, e = order
    if b < a < c and c < d < e:
        print([kids[index] for index in order])

['B', 'A', 'C', 'D', 'E']

この方法では、全ての120通りを試し、条件を満たすものを探すことになります。5人なら問題なく動作しますが、人数が増えると計算量が急増（階乗の増加）するため、全列挙は現実的ではなくなります。

permutationsについて#

itertools.permutations は Python の itertools モジュールに含まれる関数で、与えられた要素のすべての順列（並び替えの組み合わせ）を生成するのに使用されます。

itertools.permutations(iterable, r=None)

iterable : 順列を生成するための要素のリストやタプル。
r : 取り出す要素数（デフォルトは None で、すべての要素を使った順列を生成）。

例えば、リスト ['A', 'B', 'C'] のすべての並び順を生成してみます。3つの要素の順列は 3! = 6通り です。

data = ['A', 'B', 'C']
for p in permutations(data):
    print(p)

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

4つの要素から 2つだけを選んで順列を作る場合は、\(4 \times 3 = 12\)通りになります。

for p in permutations(['A', 'B', 'C', 'D'], 2):
    print(p)

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

permutations()を使うとき注意すべき点は：

順序が異なる組み合わせをすべて列挙する（組み合わせとは異なり、順序を考慮）。
要素が重複していない場合のみ使用可能（重複を考慮したい場合は itertools.product などを使う）。
計算量が爆発的に増加（n! の計算量なので、大きな n では非現実的）。

したがって、itertools.permutations は小規模な問題の確認やテストには便利ですが、大規模な制約問題には専用のソルバーを活用する方が現実的です。

Z3ソルバーを使った解法#

Z3のようなソルバーを使うと、制約を直接モデル化し、効率的に解を求めることができます。

from z3 import IntVector, Solver, Distinct, sat

# 5人の子供を整数値（順位）で表現
kids = ["A", "B", "C", "D", "E"]
a, b, c, d, e = pos = IntVector("pos", 5)  # 各子供の食べ終わる順位 (0~4)
solver = Solver()

for p in pos:
    solver.add(p >= 0, p < len(kids))

# 順位は0～4の異なる整数
solver.add(Distinct(pos))

# 制約を追加
solver.add(b < a, a < c)  # B < A < C
solver.add(c < d, d < e)  # C < D < E

# 解を求める
if solver.check() == sat:
    model = solver.model()
    solution = [model[p].as_long() for p in pos]
    print([kids[index] for index in solution])

['B', 'A', 'C', 'D', 'E']

上のプログラムでは、次のように制約を追加しています。

IntVector("pos", 5) で5つの整数変数（各子供の順位）を作成します。この時、解空間は無限です。
solver.add(p >= 0, p < len(kids)) で各順位が0から4の範囲にあることを制約します。解空間は\(5^5\)になります。
solver.add(Distinct(pos)) ですべての順位が異なることを制約します。解空間は\(5!\)になります。この段階でpermutationsと同じになります。
solver.add(b < a, a < c) などで条件をモデル化します。制約条件によって解空間がさらに小さくなります。
solver.check() で解の有無を確認し、 model() で解を取得します。
ソリューションを順位順に並べて出力します。

纏め#

次のテーブルで全数調査と制約ソルバーZ3を比較します。

手法	計算量	実装のしやすさ	解釈
`itertools.permutations`	\( O(n!) \)	簡単だが大規模には不向き	全候補を試し、条件を満たすものを探す
Z3ソルバー	効率的に探索	制約を記述すれば良い	制約を満たす解を直接求める

制約ソルバーの利点:

itertools.permutationsは小規模な問題なら使えるが、大規模な問題では現実的でない。
Z3のようなソルバーは、制約を直接扱うため、大きな問題にも対応できる。
例えば、10人や20人に拡張しても、Z3なら効率的に解を求められる。

制約充足問題

Contents

制約充足問題#

permutationsでの全数調査#

permutationsについて#

Z3ソルバーを使った解法#

纏め#