CP-SATの紹介

CP-SATの紹介#

OR-ToolsのCP-SAT（Constraint Programming SAT Solver）は、Googleが開発した最新の制約プログラミングソルバーであり、SAT（Boolean Satisfiability）技術を基盤にしています。これは従来のCPソルバーであるconstraint_solverモジュールと比較して、はるかに高いパフォーマンスを発揮し、より大規模で複雑な問題に対応できるよう設計されています。SAT技術とは、もともとブール変数の充足可能性を判断するアルゴリズムですが、CP-SATでは整数最適化や線形制約の処理にも応用されています。このSATベースのアプローチにより、従来の制約プログラミングの手法では扱いにくかった大規模な組合せ最適化問題にも対応できるようになっています。

CP-SATの特徴のひとつは、探索アルゴリズムの大幅な改善です。SATソルバー特有のConflict-Driven Clause Learning（CDCL）やLazy Clause Generation（LCG）といった技術を活用し、探索木のサイズを小さく抑えることで効率的に解を求めます。また、線形緩和（Linear Relaxation）を併用することで、MIP（Mixed Integer Programming）ソルバーと同様の最適化が可能になっており、整数計画法的なアプローチと制約プログラミングの長所を兼ね備えています。このため、純粋な制約プログラミングだけでは難しい最適化問題にも対応しやすくなっています。

一方、従来のconstraint_solverモジュールは、古典的な制約プログラミング（Constraint Programming, CP）に基づいており、主に深さ優先探索（DFS）や大域近傍探索（Large Neighborhood Search, LNS）を利用した解探索を行います。この方法は、特定の種類の組合せ問題には有効ですが、最適化が求められる問題や、より大きな探索空間を持つ問題では、探索時間が指数関数的に増加してしまうという課題がありました。また、最適化の際に、MIPソルバーのような線形緩和の技術が使えないため、特に大規模なスケジューリングやナップザック問題などでは、解の品質が劣ることもありました。

このように、CP-SATはSATソルバーの技術を活かしながら、線形計画法や制約プログラミングの良い部分を統合した強力なソルバーであり、従来のCP-Solverよりも多くの問題に適用しやすくなっています。そのため、新たにOR-Toolsを使って制約プログラミングを行う場合は、CP-SATを第一に選択すべきでしょう。

「SEND + MORE = MONEY」を解く#

z3でSEND+MORE=MONEYを解く

本節では、「SEND + MORE = MONEY」を例に、CP-SAT の使い方を説明します。以下に、フルソースコードを示します。

from ortools.sat.python import cp_model

model = cp_model.CpModel()
s, e, n, d, m, o, r, y = [model.new_int_var(0, 10, name) for name in "sendmory"]
model.add(s != 0)
model.add(m != 0)
model.add_all_different([s, e, n, d, m, o, r, y])
send = s * 1000 + e * 100 + n * 10 + d
more = m * 1000 + o * 100 + r * 10 + e
money = m * 10000 + o * 1000 + n * 100 + e * 10 + y

model.add(send + more == money)
solver = cp_model.CpSolver()
solver.Solve(model)
print(f"{solver.value(send)} + {solver.value(more)} = {solver.value(money)}")

9567 + 1085 = 10652

  • CpModel(): 制約プログラミングのためのモデルを作成します。

  • CpModel.new_int_var(): 指定した範囲の整数変数を作成します。

  • * や + などを用いて演算式を作成できます。

  • != や == などを用いて制約条件を記述できます。

  • CpModel.add(): モデルに制約条件を追加します。

また、積和演算は LinearExpr.weighted_sum() を用いて次のように表現することもできます。

send = cp_model.LinearExpr.weighted_sum([s, e, n, d], [1000, 100, 10, 1])
more = cp_model.LinearExpr.weighted_sum([m, o, r, e], [1000, 100, 10, 1])
money = cp_model.LinearExpr.weighted_sum([m, o, n, e, y], [10000, 1000, 100, 10, 1])

CpSolver().solve(model) を用いて解を求め、CpSolver.value(expr) で演算式 expr の値を取得できます。

以下のように修正すると、より自然で明確な日本語になります。

線形計画法#

線形計画法の例として、以下の問題を考えます。

ある製品 A および B を生産するためには、3 種類の原料 a、b、c が必要です。各製品を 1 単位生産するために必要な原料の量と、各原料の現在の在庫量は、以下の表の通りとします。また、各製品を 1 単位売却すると、それぞれ 3 万円および 2 万円の利益が得られるものとします。利益を最大化するために、各製品の生産量を決定してください。

原料

製品 A に対する必要量

製品 B に対する必要量

在庫量

a

3

1

9

b

2.5

2

12.5

c

1

2

8

各製品の生産量を、それぞれ (x_1) および (x_2) とすると、この問題は以下のように定式化できます。

目的関数:

\[ z = 3x_1 + 2x_2 \]

制約条件:

\[\begin{split} \begin{aligned} 3x_1 + x_2 &\leq 9 \\ 2.5x_1 + 2x_2 &\leq 12.5 \\ x_1 + 2x_2 &\leq 8 \\ x_1, x_2 &\geq 0 \end{aligned} \end{split}\]

このように、線形計画問題は目的関数と制約条件を明確に定式化することで、最適な解を求めることができます。

次のコードでは、maximize(z) は目的関数 \( z = 3x_1 + 2x_2 \) を最大化するように、\( x_1 \) と \( x_2 \) の値を決定することを意味します。また、CP-SAT は整数しか扱えないため、2.5 を含む式のすべての数値を整数にするために、両辺を 2 倍にして調整します。

model = cp_model.CpModel()
x1, x2 = [model.new_int_var(0, 10000, f"x{i}") for i in range(1, 3)]
model.add(3 * x1 + x2 <= 9)
model.add(5 * x1 + 4 * x2 <= 25)
model.add(x1 + 2 * x2 <= 8)
z = 3 * x1 + 2 * x2
model.maximize(z)
solver = cp_model.CpSolver()
solver.Solve(model)
print(f"x1 = {solver.value(x1)}, x2 = {solver.value(x2)}, z = {solver.value(z)}")

x1 = 2, x2 = 3, z = 12

論理クイズ#

赤、青、黄、緑の4つの箱があります。この中のどれかにりんごが入っています。りんごが入っている箱の数は分かりませんが、少なくとも1つはリンゴの入った箱があります。もちろん、2つ以上あることもあります。あなたは、どれか1つだけ箱を選んで中身をもらえることになりました。次の情報をもとに、どの箱を選べばりんごが入っているか当ててください。

  • 赤の箱にりんごが入っている場合、青の箱にもりんごが入っている。

  • 緑の箱にりんごが入っていない場合、黄色の箱と青の箱にはりんごは入っていない。

次のコードを使って、このクイズを解くことができます。

model = cp_model.CpModel()
red, blue, yellow, green = [model.new_bool_var(name) for name in ['red', 'blue', 'yello', 'green']]

model.add_bool_or([red, blue, yellow, green])
model.add_implication(red, blue)
model.add_bool_and(~yellow, ~blue).only_enforce_if(~green)

solver = cp_model.CpSolver()
for box in [red, blue, yellow, green]:
    model.add_assumption(~box)
    res = solver.solve(model)
    if res == cp_model.INFEASIBLE:
        print(box)
    model.clear_assumptions()

green

  • new_bool_var(): ブール変数を作成します（ブール値は 0 または 1 の整数変数として表現されます）。

  • add_bool_or([red, blue, yellow, green]): 「少なくとも 1 つの箱にはりんごが入っている」という制約を追加します（論理和）。

  • add_implication(red, blue): 「赤の箱にりんごがあるなら、青の箱にもりんごがある」という制約を追加します（論理包含）。

  • add_bool_and(~yellow, ~blue).only_enforce_if(~green): 「緑の箱にりんごが入っていない場合、黄色と青の箱にもりんごは入っていない」という制約を追加します。

    • ~ は not を意味します。

    • only_enforce_if() を使用して制約の前提条件を設定します。

    • 「黄色と青の箱にもりんごは入っていない」は常に適用されるわけではなく、「緑の箱にりんごが入っていない」場合にのみ有効になることを指定します。

この問題では、単に解を見つけるのではなく、どの箱に必ずりんごが入っているかを推理する ことが目的です。そのため、add_assumption(~box) を使用して各箱について「りんごが入っていない」と仮定し、それが矛盾を引き起こすかどうかを確認します。

  • もし solver.solve(model) の結果が INFEASIBLE（解が存在しない）となった場合、その仮定は誤りであり、その箱には必ずりんごが入っていることになります。

  • 次の仮定を試す前に、clear_assumptions() を呼び出して前の仮定をリセットする必要があります。

Contents