CP-SATの紹介 ― SATの技術で解く制約プログラミング

CP-SATの紹介 ― SATの技術で解く制約プログラミング#

この章で学ぶこと#

OR-Tools の CP-SAT は、Google が作った制約プログラミングのソルバーです。Z3 の章と同じく「条件を書いて解を求める」道具ですが、最適化（利益を最大にする、距離を最小にする）が得意です。

  • CP-SAT がどんな仕組みで解いているか（SAT の技術＋線形緩和）

  • 一番基本的な使い方（CpModel / new_int_var / add / solve）

  • 線形計画法の例（利益の最大化）

  • 論理クイズを assumptions で推理する

CP-SAT とは#

CP-SAT は、SAT（充足可能性問題）の技術を土台にした制約プログラミングのソルバーです。

  • SAT ソルバーの CDCL（衝突を学習して枝刈りする）や LCG（Lazy Clause Generation）といった技術で、探索を賢く進めます。

  • 線形緩和も組み合わせているので、MIP（混合整数計画）ソルバーのように「目的関数を最大・最小にする」最適化もできます。

OR-Tools には古くから constraint_solver（古典的な CP ソルバー）もありますが、そちらは深さ優先探索が中心で、最適化が苦手でした。新しく OR-Tools を使うなら CP-SAT を選ぶのが定石です。この本の OrTools の章は、すべて CP-SAT を使います。

例題：SEND + MORE = MONEY#

z3でSEND+MORE=MONEYを解く

Z3 の章でも扱った覆面算を、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() … モデル（制約の入れ物）を作る

  • model.new_int_var(下限, 上限, 名前) … 整数変数を作る

  • model.add(条件) … 制約を追加する（!=, ==, >= などの比較式がそのまま書ける）

  • model.add_all_different([...]) … すべて違う値にする

  • solver.solve(model) … 解を求める

  • solver.value(式) … 式の値を取り出す

* や + で式を作れるので、s * 1000 + e * 100 + ... のように「桁」をそのまま書けます。積和は 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])

線形計画法#

次は「利益を最大にする」問題です。線形計画法の例として、次の問題を考えます。

ある製品 A と B を作るのに、3種類の原料 a, b, c が必要です。1単位作るのに必要な量と在庫は次のとおりで、1単位売ると A は3万円、B は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 \quad \text{（最大化）} \]

制約条件

\[\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}\]

CP-SAT は整数しか扱えません。2.5 が入った式は、両辺を2倍して整数にします（2.5x1 + 2x2 <= 12.5 → 5x1 + 4x2 <= 25）。不等式を2倍しても、条件の意味は変わりません。

model.maximize(z) は「\(z = 3x_1 + 2x_2\) を最大にする \(x_1, x_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つの箱を選んで、中身をもらえることになりました。次の情報から、必ずりんごが入っている箱を選んでください。

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

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

CP-SAT では、ブール変数と論理制約でそのまま書けます。

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

model.add_bool_or([red, blue, yellow, green])                 # 少なくとも1つは入っている
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([...]) … 少なくとも1つが真（論理和）

  • add_implication(a, b) … a なら b（論理包含）

  • add_bool_and(a, b).only_enforce_if(c) … c のときだけ「a かつ b」

    • ~ は否定

    • only_enforce_if() は「この条件のときだけ有効」を指定する

このクイズの目的は、解を1つ見つけることではなく、どの箱が必ずりんご入りかを推理することです。そこで各箱について「入っていない」と仮定して解き、矛盾（INFEASIBLE）すれば、その箱には必ず入っていると判断します。

  • model.add_assumption(条件) で仮定を追加する

  • clear_assumptions() で仮定を消す（次の箱を試す前に必ず呼ぶ）

結果は green でした。緑がないとすると、黄も青もなくなり、赤→青も使えないので、りんごが1つもなくなるからです。

まとめ#

  • CP-SAT は SAT の技術＋線形緩和で動く制約ソルバー。OR-Tools ならこれ一択

  • 基本の流れは CpModel() → 変数 → add() → solve() → value()

  • 最適化は model.maximize(式) / model.minimize(式)

  • CP-SAT は整数だけ。小数がある式は、両辺を整数倍して消す

  • ブール変数と論理制約（add_bool_or, add_implication, only_enforce_if）で条件分岐も書ける

  • assumptions を使うと「この条件を足したら矛盾するか」を調べられる（推理クイズの定石）

次の章では、CP-SAT の API をもう少し詳しく見ていきます。