CP-SATの基本API

from ortools.sat.python import cp_model
from helper.ortools import get_all_solutions

本章では、CP-SATの基本的なAPI関数について説明します。主に以下の関数が含まれます。

• 変数作成: new_int_var, new_bool_var, new_int_var_from_domain

• 目的関数: minimize, maximize

• 線形制約: add, add_linear_constraint, add_linear_expression_in_domain

• 絶対値と最大・最小制約: add_min_equality, add_max_equality, add_abs_equality

• 乗算・除算・剰余制約: add_modulo_equality, add_multiplication_equality, add_division_equality

• 異なる値: add_all_different

• 論理制約: add_implication, add_bool_or, add_at_least_one, add_at_most_one, add_exactly_one, add_bool_and, add_bool_xor

• ドメインと組み合わせ: add_allowed_assignments, add_forbidden_assignments

• 配列/要素制約: add_element, add_inverse

変数の作成

• new_int_var: 最小値、最大値、変数名を指定して整数変数を作成

• new_bool_var: 最小値0、最大値1の整数変数を作成。引数には変数名のみ指定

• new_int_var_from_domain: 不連続な範囲を指定して整数変数を作成

以下では、これらの関数を使った例を説明します。ヘルプ関数get_all_solutions()を使ってすべての解を取得し、変数の候補値を観測します。

次に、\(0 \le x \le 3\) の整数変数を作成します。

model = cp_model.CpModel()
x = model.new_int_var(0, 3, 'x')
get_all_solutions(model)

[{'x': 0}, {'x': 1}, {'x': 2}, {'x': 3}]

次に、\(0 \le b \le 1\) の整数変数（ブール変数）を作成します。

model = cp_model.CpModel()
x = model.new_bool_var('b')
get_all_solutions(model)

[{'b': 0}, {'b': 1}]

次に、Domain.from_values() を使って候補値を直接指定します。

model = cp_model.CpModel()
domain = cp_model.Domain.from_values([1, 3, 5, 7])
x = model.new_int_var_from_domain(domain, 'x')
get_all_solutions(model)

[{'x': 1}, {'x': 3}, {'x': 5}, {'x': 7}]

次に、Domain.from_flat_intervals() を使って複数の範囲を指定します。各範囲は連続した二つの値のペアで指定します。下限や上限がない場合は、INT_MIN と INT_MAX を使用します。

model = cp_model.CpModel()
domain = cp_model.Domain.from_flat_intervals([1, 3, 7, 9, 10, 12])
x = model.new_int_var_from_domain(domain, 'x')
get_all_solutions(model)

[{'x': 1},
 {'x': 2},
 {'x': 3},
 {'x': 7},
 {'x': 8},
 {'x': 9},
 {'x': 10},
 {'x': 11},
 {'x': 12}]

線形制約

• add(): 線形演算式の比較式を制約条件として追加します。

• add_linear_constraint(): 線形演算式とその下限・上限を指定して制約条件を追加します。

• add_linear_expression_in_domain(): 線形演算式の不連続な範囲を制約します。

次の二つの例では、すべて \(30 \le 10 x \le 50\) という線形制約を作成しますが、例1では二つの add() を使って式の下限と上限を指定します。例2では、add_linear_constraint() を使って下限と上限を同時に設定します。

model = cp_model.CpModel()
x = model.new_int_var(0, 100, 'x')
model.add(10 * x <= 50)
model.add(10 * x >= 30)
get_all_solutions(model)

[{'x': 3}, {'x': 4}, {'x': 5}]

model = cp_model.CpModel()
x = model.new_int_var(0, 100, 'x')
model.add_linear_constraint(10 * x, 30, 50)
get_all_solutions(model)

[{'x': 3}, {'x': 4}, {'x': 5}]

次に、add_linear_expression_in_domain() を使って、\(30 \le 10 x \le 50 \lor 30 \le 10 x \le 80\) という線形制約を作成します。

model = cp_model.CpModel()
x = model.new_int_var(0, 100, 'x')
domain = cp_model.Domain.from_flat_intervals([30, 50, 70, 80])
model.add_linear_expression_in_domain(10 * x, domain)
get_all_solutions(model)

[{'x': 3}, {'x': 4}, {'x': 5}, {'x': 7}, {'x': 8}]

本書では、次の二つのヘルプ関数を提供します。これらの関数は比較式を作成し、add() で制約条件として追加できます。

• \(l \le x \le u\): is_between(x, l, u)

• \(x < l \lor x > u\): is_not_between(x, l, u)

model = cp_model.CpModel()
x = model.new_int_var(1, 6, 'x')
y = model.new_int_var(1, 6, 'y')
model.add(is_between(x + y, 9, 10))
get_all_solutions(model)

[{'x': 3, 'y': 6},
 {'x': 4, 'y': 5},
 {'x': 4, 'y': 6},
 {'x': 5, 'y': 4},
 {'x': 5, 'y': 5},
 {'x': 6, 'y': 3},
 {'x': 6, 'y': 4}]

model = cp_model.CpModel()
x = model.new_int_var(1, 6, 'x')
y = model.new_int_var(1, 6, 'y')
model.add(is_not_between(x + y, 4, 11))
get_all_solutions(model)

[{'x': 1, 'y': 1}, {'x': 2, 'y': 1}, {'x': 1, 'y': 2}, {'x': 6, 'y': 6}]

条件分岐

作成した制約条件に対して、only_enforce_if() メソッドを使用すると、その条件が有効になる前提条件を指定できます。前提条件には、一つまたは複数のブール変数、あるいはその否定のみを使用できます。たとえば、次のような条件を実装する場合、中間のブール変数を用いることで、二つの比較式をリンクできます。

\[ 1 \leq x \leq 3, \quad 1 \leq y \leq 3 \]

\[\begin{split} z = \begin{cases} 50, & \text{if } x + y \geq 4 \\ -50, & \text{otherwise} \end{cases} \end{split}\]

以下のコードでは、only_enforce_if(cond) と only_enforce_if(~cond) を使用し、cond を x + y >= 4 にリンクさせています。次に、この条件を利用して z の値を制約します。

model = cp_model.CpModel()
x, y = [model.new_int_var(1, 3, name) for name in 'xy']
z= model.new_int_var(-100, 100, 'z')

cond = model.new_bool_var('cond')
model.add(x + y >= 4).only_enforce_if(cond)
model.add(x + y < 4).only_enforce_if(~cond)

model.add(z == 50).only_enforce_if(cond)
model.add(z == -50).only_enforce_if(~cond)
get_all_solutions(model)

[{'x': 1, 'y': 1, 'z': -50, 'cond': 0},
 {'x': 2, 'y': 1, 'z': -50, 'cond': 0},
 {'x': 1, 'y': 2, 'z': -50, 'cond': 0},
 {'x': 1, 'y': 3, 'z': 50, 'cond': 1},
 {'x': 2, 'y': 2, 'z': 50, 'cond': 1},
 {'x': 3, 'y': 2, 'z': 50, 'cond': 1},
 {'x': 3, 'y': 3, 'z': 50, 'cond': 1},
 {'x': 2, 'y': 3, 'z': 50, 'cond': 1},
 {'x': 3, 'y': 1, 'z': 50, 'cond': 1}]

上記の方法では、比較式の否定を手動で作成する必要があり、手間がかかります。本書では、ヘルパー関数 equals(cond, expr, model) を用いることで、expr の否定を自動生成し、次の二つの制約を model に追加できます。

model.add(expr).only_enforce_if(cond)
model.add(inverse_expr).only_enforce_if(~cond)

以下のコードでは、equals() を用いて x + y >= 4 の条件を cond に関連付けています。

from helper.ortools import equals
model = cp_model.CpModel()
x, y = [model.new_int_var(1, 3, name) for name in 'xy']
z= model.new_int_var(-100, 100, 'z')

cond = model.new_bool_var('cond')
equals(cond, x + y >= 4, model)

model.add(z == 50).only_enforce_if(cond)
model.add(z == -50).only_enforce_if(~cond)
get_all_solutions(model)

[{'x': 1, 'y': 1, 'z': -50, 'cond': 0},
 {'x': 2, 'y': 1, 'z': -50, 'cond': 0},
 {'x': 1, 'y': 2, 'z': -50, 'cond': 0},
 {'x': 1, 'y': 3, 'z': 50, 'cond': 1},
 {'x': 2, 'y': 2, 'z': 50, 'cond': 1},
 {'x': 3, 'y': 2, 'z': 50, 'cond': 1},
 {'x': 3, 'y': 3, 'z': 50, 'cond': 1},
 {'x': 2, 'y': 3, 'z': 50, 'cond': 1},
 {'x': 3, 'y': 1, 'z': 50, 'cond': 1}]

最大値、最小値、絶対値

次には、最小値・最大値・絶対値に関する制約を簡単に追加できるメソッドを紹介します。

1. add_min_equality(target, expressions): target = min(expressions) となる制約を追加します。

2. add_max_equality(target, expressions): target = max(expressions) となる制約を追加します。

3. add_abs_equality(target, expression): target = abs(expression) となる制約を追加します。

次のコードでは、2 * x と y のうち小さい方が 2 になるように制約*課されます。例えば、x=1, y=3 の場合 min(2, 3) = 2 なので、このような組み合わせが解となります。

model = cp_model.CpModel()
x, y = [model.new_int_var(0, 4, n) for n in 'xy']
model.add_min_equality(2, [2 * x,  y])
get_all_solutions(model)

[{'x': 1, 'y': 2},
 {'x': 1, 'y': 3},
 {'x': 1, 'y': 4},
 {'x': 2, 'y': 2},
 {'x': 3, 'y': 2},
 {'x': 4, 'y': 2}]

次のコードでは、2 * x と y のうち大きい方が 4 になるように制約が課されます。例えば、x=2, y=3 の場合 max(4, 3) = 4 なので、このような組み合わせが解となります。

model = cp_model.CpModel()
x, y = [model.new_int_var(1, 4, n) for n in 'xy']
model.add_max_equality(4, [2 * x, y])
get_all_solutions(model)

[{'x': 1, 'y': 4},
 {'x': 2, 'y': 1},
 {'x': 2, 'y': 2},
 {'x': 2, 'y': 3},
 {'x': 2, 'y': 4}]

次のコードでは、x - y の絶対値が 2 になるように制約が課されます。例えば、x=3, y=1 の場合 |3 - 1| = 2 なので、このような組み合わせが解となります。

model = cp_model.CpModel()
x, y = [model.new_int_var(1, 4, n) for n in 'xy']
model.add_abs_equality(2, x - y)
get_all_solutions(model)

[{'x': 1, 'y': 3}, {'x': 2, 'y': 4}, {'x': 3, 'y': 1}, {'x': 4, 'y': 2}]

変数同士の乗算・除算

次は、整数変数同士の乗算・除算を簡単にモデル化するための便利なメソッドを紹介します。

• add_modulo_equality(target, dividend, divisor): dividend % divisor == target という制約を追加します。

• add_multiplication_equality(target, *expressions): product(expressions) == target という制約を追加します。

• add_division_equality(target, numerator, denominator): numerator // denominator == target という制約を追加します（整数除算）。

以下のコードは、add_multiplication_equality()で三辺の長さが整数である直角三角形（ピタゴラス数）を求めます。

model = cp_model.CpModel()
max_n = 20
x, y, z = [model.new_int_var(1, max_n, n) for n in 'xyz']
x2, y2, z2 = [model.new_int_var(1, 2 * max_n**2, n) for n in ['x2', 'y2', 'z2']]
model.add_multiplication_equality(x2, x, x)
model.add_multiplication_equality(y2, y, y)
model.add_multiplication_equality(z2, z, z)
model.add(x2 + y2 == z2)
model.add(y >= x)
get_all_solutions(model)

[{'x': 3, 'y': 4, 'z': 5, 'x2': 9, 'y2': 16, 'z2': 25},
 {'x': 5, 'y': 12, 'z': 13, 'x2': 25, 'y2': 144, 'z2': 169},
 {'x': 6, 'y': 8, 'z': 10, 'x2': 36, 'y2': 64, 'z2': 100},
 {'x': 8, 'y': 15, 'z': 17, 'x2': 64, 'y2': 225, 'z2': 289},
 {'x': 9, 'y': 12, 'z': 15, 'x2': 81, 'y2': 144, 'z2': 225},
 {'x': 12, 'y': 16, 'z': 20, 'x2': 144, 'y2': 256, 'z2': 400}]

異なる値

複数の変数がすべて異なる値を取るようにするための便利なメソッドadd_all_different(*expressions)が用意されています。指定したすべての演算式が異なる値を取るように制約を追加します。これは数独や割り当て問題など、異なる値を必要とする問題でよく使われます。次のコードは, 1, 2, 3の順列を求めます。

model = cp_model.CpModel()
x, y, z = [model.new_int_var(1, 3, n) for n in 'xyz']
model.add_all_different(x, y, z)
get_all_solutions(model)

[{'x': 3, 'y': 2, 'z': 1},
 {'x': 3, 'y': 1, 'z': 2},
 {'x': 2, 'y': 3, 'z': 1},
 {'x': 2, 'y': 1, 'z': 3},
 {'x': 1, 'y': 3, 'z': 2},
 {'x': 1, 'y': 2, 'z': 3}]

論理制約

本節で紹介する制約条件はブール変数あるその否定しか使えません。

メソッド	内容
add_implication(a, b)	a ⇒ b （a が真なら b も真）
add_bool_or([a, b, c])	a OR b OR c（少なくとも 1 つ真）
add_at_least_one([a, b, c])	少なくとも 1 つ真
add_at_most_one([a, b, c])	高々 1 つだけ真
add_exactly_one([a, b, c])	ちょうど 1 つだけ真
add_bool_and([a, b, c])	a AND b AND c（すべて真）
add_bool_xor([a, b, c])	奇数個の変数が真

add_implication(a, b) は論理包含の制約条件を追加します。これは「a が真ならば b も真である」という意味です。この制約は、次のテーブルで表現できます。

入力 a	入力 b	出力 a → b
0	0	1
0	1	1
1	0	0
1	1	1

a が真のときに b も真である場合にのみ、「出力 a → b」は 1 になります。次のコードは、「出力 a → b」が 1 になる解を求め、3つの解を出力します。

model = cp_model.CpModel()
a, b = [model.new_bool_var(n) for n in 'ab']
model.add_implication(a, b)
get_all_solutions(model)

[{'a': 0, 'b': 0}, {'a': 0, 'b': 1}, {'a': 1, 'b': 1}]

add_bool_or() と add_at_least_one() は同じ意味で、ブール変数リストに対して少なくとも1つが真であることを制約します。つまり、全てが偽の組み合わせを除外します。

model = cp_model.CpModel()
x, y, z = [model.new_bool_var(n) for n in 'xyz']
model.add_bool_or(x, y, z)
get_all_solutions(model)

[{'x': 0, 'y': 1, 'z': 0},
 {'x': 0, 'y': 1, 'z': 1},
 {'x': 0, 'y': 0, 'z': 1},
 {'x': 1, 'y': 0, 'z': 1},
 {'x': 1, 'y': 0, 'z': 0},
 {'x': 1, 'y': 1, 'z': 0},
 {'x': 1, 'y': 1, 'z': 1}]

add_at_most_one() は、ブール変数リストの中で最大1つだけが真であることを制約します。つまり、2つ以上が真であることはありません。

model = cp_model.CpModel()
x, y, z = [model.new_bool_var(n) for n in 'xyz']
model.add_at_most_one(x, y, z)
get_all_solutions(model)

[{'x': 0, 'y': 0, 'z': 0},
 {'x': 0, 'y': 1, 'z': 0},
 {'x': 0, 'y': 0, 'z': 1},
 {'x': 1, 'y': 0, 'z': 0}]

add_exactly_one() は、ブール変数リストの中で ちょうど1つだけが真であることを制約します。

model = cp_model.CpModel()
x, y, z = [model.new_bool_var(n) for n in 'xyz']
model.add_exactly_one(x, y, z)
get_all_solutions(model)

[{'x': 0, 'y': 1, 'z': 0}, {'x': 0, 'y': 0, 'z': 1}, {'x': 1, 'y': 0, 'z': 0}]

add_bool_and() は、ブール変数リストのすべてが真であることを制約します。

model = cp_model.CpModel()
x, y, z = [model.new_bool_var(n) for n in 'xyz']
model.add_bool_and(x, y, z)
get_all_solutions(model)

[{'x': 1, 'y': 1, 'z': 1}]

この制約は強すぎることが多いため、一般的には only_enforce_if() と併用して使用します。

model = cp_model.CpModel()
x, y, z = [model.new_bool_var(n) for n in 'xyz']
model.add_bool_and(x, y).only_enforce_if(~z)
get_all_solutions(model)

[{'x': 1, 'y': 1, 'z': 0},
 {'x': 1, 'y': 1, 'z': 1},
 {'x': 1, 'y': 0, 'z': 1},
 {'x': 0, 'y': 0, 'z': 1},
 {'x': 0, 'y': 1, 'z': 1}]

add_bool_xor() は、ブール変数リストの中で奇数個の真があることを制約します。

model = cp_model.CpModel()
x, y, z = [model.new_bool_var(n) for n in 'xyz']
model.add_bool_xor(x, y, z)
get_all_solutions(model)

[{'x': 0, 'y': 1, 'z': 0},
 {'x': 0, 'y': 0, 'z': 1},
 {'x': 1, 'y': 0, 'z': 0},
 {'x': 1, 'y': 1, 'z': 1}]

組み合わせの解

add_allowed_assignments() は、指定した変数に対して許可される値の組み合わせを制約として追加します。この制約は、リスト内の各変数が特定の組み合わせの値のみを取ることを強制します。

次のコードでは、変数 x と y について特定の値の組み合わせ（[5, 6] と [6, 7]）を、変数 y と z についても別の組み合わせ（[6, 8] と [7, 9]）を設定し、許可された解を求めています。

model = cp_model.CpModel()
x, y, z = [model.new_int_var(1, 10, n) for n in 'xyz']
model.add_allowed_assignments([x, y], [[5, 6], [6, 7]])
model.add_allowed_assignments([y, z], [[6, 8], [7, 9]])
get_all_solutions(model)

[{'x': 5, 'y': 6, 'z': 8}, {'x': 6, 'y': 7, 'z': 9}]

複数の計算式に対して候補の解を設定する場合は、中間変数を使います。次のコードでは、x_plus_y と y_plus_z は中間変数として定義され、各々 x + y と y + z の計算式を保持します。さらに、add_allowed_assignments()でx_plus_y は 5 または 6 になり、y_plus_z は 6 または 7 になる組み合わせが許可されます。この方法で中間変数を利用することで、複雑な計算式に対する解の候補を簡単に設定することができます。

model = cp_model.CpModel()
x, y, z = [model.new_int_var(1, 10, n) for n in 'xyz']
x_plus_y = model.new_int_var(-100, 100, 'x + y')
y_plus_z = model.new_int_var(-100, 100, 'y + z')
model.add(x_plus_y == x + y)
model.add(y_plus_z == y + z)
model.add_allowed_assignments([x_plus_y, y_plus_z], [[5, 6], [6, 7]])
get_all_solutions(model)

[{'x': 1, 'y': 4, 'z': 2, 'x + y': 5, 'y + z': 6},
 {'x': 2, 'y': 3, 'z': 3, 'x + y': 5, 'y + z': 6},
 {'x': 3, 'y': 2, 'z': 4, 'x + y': 5, 'y + z': 6},
 {'x': 4, 'y': 1, 'z': 5, 'x + y': 5, 'y + z': 6},
 {'x': 4, 'y': 2, 'z': 5, 'x + y': 6, 'y + z': 7},
 {'x': 3, 'y': 3, 'z': 4, 'x + y': 6, 'y + z': 7},
 {'x': 2, 'y': 4, 'z': 3, 'x + y': 6, 'y + z': 7},
 {'x': 5, 'y': 1, 'z': 6, 'x + y': 6, 'y + z': 7},
 {'x': 1, 'y': 5, 'z': 2, 'x + y': 6, 'y + z': 7}]

add_forbidden_assignments() は、指定した変数に対して許可しない値の組み合わせを制約として追加します。この制約を使うことで、特定の変数の組み合わせが解に現れないようにすることができます。次のコードでは、x と y、または y と z の組み合わせにおいて、1, 2、1, 3、2, 2 の組み合わせを禁止します。

model = cp_model.CpModel()
x, y, z = [model.new_int_var(1, 3, n) for n in 'xyz']
model.add_forbidden_assignments([x, y], [[1, 2], [1, 3], [2, 2]])
model.add_forbidden_assignments([y, z], [[1, 2], [1, 3], [2, 2]])
get_all_solutions(model)

[{'x': 3, 'y': 3, 'z': 1},
 {'x': 3, 'y': 2, 'z': 1},
 {'x': 3, 'y': 1, 'z': 1},
 {'x': 2, 'y': 1, 'z': 1},
 {'x': 2, 'y': 3, 'z': 1},
 {'x': 2, 'y': 3, 'z': 2},
 {'x': 2, 'y': 3, 'z': 3},
 {'x': 3, 'y': 3, 'z': 3},
 {'x': 3, 'y': 2, 'z': 3},
 {'x': 3, 'y': 3, 'z': 2},
 {'x': 1, 'y': 1, 'z': 1}]

配列要素

add_element(index, values, element) は、配列 values の index 番目の要素が element に等しいことを制約として追加します。この制約を使用すると、配列内の指定した位置にある要素が特定の値に一致するように条件を設定できます。

model = cp_model.CpModel()
index = model.new_int_var(0, 4, 'index')
element = model.new_int_var(-100, 100, 'element')
model.add_element(index, [1, 3, 5, 7], element)
get_all_solutions(model)

[{'index': 0, 'element': 1},
 {'index': 1, 'element': 3},
 {'index': 2, 'element': 5},
 {'index': 3, 'element': 7}]

values は定数のリストだけでなく、変数のリストを使うこともできます。

model = cp_model.CpModel()
x, y, z =  [model.new_bool_var(n) for n in 'xyz']
index = model.new_int_var(0, 3, 'index')
element = model.new_int_var(-100, 100, 'element')
model.add_at_most_one([x, y, z])
model.add_element(index, [x, y, z], element)
get_all_solutions(model)

[{'x': 0, 'y': 0, 'z': 0, 'index': 0, 'element': 0},
 {'x': 0, 'y': 1, 'z': 0, 'index': 0, 'element': 0},
 {'x': 0, 'y': 0, 'z': 1, 'index': 0, 'element': 0},
 {'x': 0, 'y': 0, 'z': 1, 'index': 1, 'element': 0},
 {'x': 0, 'y': 0, 'z': 0, 'index': 1, 'element': 0},
 {'x': 0, 'y': 1, 'z': 0, 'index': 1, 'element': 1},
 {'x': 0, 'y': 0, 'z': 1, 'index': 2, 'element': 1},
 {'x': 0, 'y': 0, 'z': 0, 'index': 2, 'element': 0},
 {'x': 0, 'y': 1, 'z': 0, 'index': 2, 'element': 0},
 {'x': 1, 'y': 0, 'z': 0, 'index': 2, 'element': 0},
 {'x': 1, 'y': 0, 'z': 0, 'index': 1, 'element': 0},
 {'x': 1, 'y': 0, 'z': 0, 'index': 0, 'element': 1}]

add_inverse(a, b) は、配列 a のインデックスを使って配列 b の要素を決定する制約を追加します。具体的には、b[a[i]] == i となるように制約します。これにより、b は a の arg_sort() と一致することが保証されます。

例えば、a の要素 [1, 2, 0] が与えられた場合、b は [2, 0, 1] の順番に基づいてインデックスが配置され、b[1] == 0, b[2] == 1, b[0] == 2 となります。

import numpy as np

model = cp_model.CpModel()
a = [model.new_int_var(0, 2, n) for n in ['a0', 'a1', 'a2']]
b = [model.new_int_var(0, 2, n) for n in ['b0', 'b1', 'b2']]
model.add_inverse(a, b)
for sol in get_all_solutions(model):
    a_sol = [sol[f'a{i}'] for i in range(3)]
    b_sol = [sol[f'b{i}'] for i in range(3)]
    print(f'a = {a_sol}, b = {b_sol}, arg_sort = {np.argsort(a_sol).tolist()}')

a = [2, 1, 0], b = [2, 1, 0], arg_sort = [2, 1, 0]
a = [1, 2, 0], b = [2, 0, 1], arg_sort = [2, 0, 1]
a = [2, 0, 1], b = [1, 2, 0], arg_sort = [1, 2, 0]
a = [1, 0, 2], b = [1, 0, 2], arg_sort = [1, 0, 2]
a = [0, 2, 1], b = [0, 2, 1], arg_sort = [0, 2, 1]
a = [0, 1, 2], b = [0, 1, 2], arg_sort = [0, 1, 2]