CP-SATの基本API ― 制約を書くための道具一覧

CP-SATの基本API ― 制約を書くための道具一覧#

この章で学ぶこと#

CP-SAT で使う API の一覧と、それぞれの動く例です。

変数の作り方（整数・ブール・とびとびの範囲）
線形制約と、条件付きの制約（only_enforce_if）
最大・最小・絶対値、乗算・除算・剰余
論理制約（AND / OR / ちょうど1つ / XOR）
組み合わせの許可・禁止、配列の要素参照（add_element）、逆写像（add_inverse）

from ortools.sat.python import cp_model
from helper.ortools import get_all_solutions, is_between, is_not_between

この章で扱う関数#

CP-SAT で使う API を、動く例とセットで並べます。辞書のように引ける構成です。各例では get_all_solutions() ですべての解を取り出して、制約が何をしているかを目で確かめます。

分類	関数
変数作成	`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 \leq 10x \leq 50\) または \(70 \leq 10x \leq 80\) という制約を作ります。Domain.from_flat_intervals([30, 50, 70, 80]) は「30〜50」と「70〜80」の2つの区間を表します。

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

次のコードでは、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]

まとめ#

やりたいこと	使うもの
整数変数	`new_int_var(lb, ub, name)`
0/1 の変数	`new_bool_var(name)`
飛び飛びの値だけ	`new_int_var_from_domain(Domain.from_values([...]), name)`
区間の集まり	`Domain.from_flat_intervals([lb1, ub1, lb2, ub2])`
上限と下限をまとめて	`add_linear_constraint(式, lb, ub)`
とびとびの範囲に収める	`add_linear_expression_in_domain(式, domain)`
条件付きで制約を効かせる	`model.add(...).only_enforce_if(b)`
最大・最小・絶対値	`add_max_equality` / `add_min_equality` / `add_abs_equality`
積・商・余り	`add_multiplication_equality` / `add_division_equality` / `add_modulo_equality`
すべて違う値	`add_all_different`
組み合わせを許可・禁止	`add_allowed_assignments` / `add_forbidden_assignments`
配列の参照	`add_element(index, values, element)`
逆写像	`add_inverse(a, b)`（`b[a[i]] == i`）

制約は「解の候補を減らしていく」もの。get_all_solutions() で解の集合を見ると、制約の意味がよく分かる
論理制約はブール変数専用。整数を使いたいときは、比較式をブール変数に割り当ててから使う