Quadratic Model

このセクションでは二次多項式模型 (論理模型) クラスとその周辺関数について説明します。論理模型クラスは多項式や行列で表される目的関数と、変数間に課せられる制約条件を、二次多項式の「論理模型」としてモデル化する役割を持ちます。

参考

このセクションを読む前に Tutorial にて Amplify SDK の基本的な使用方法と Polynomial にて多項式オブジェクトと Constraint にて制約条件オブジェクトの使用方法を確認してください。

論理模型クラスは多項式や行列などで表される目的関数を二次形式に変換し、制約条件オブジェクトの持つペナルティ関数と合わせて、QUBO やイジング模型として定式化する役割を持ちます。後述するソルバークラス(Solver) を用いてイジングマシンを実行する際には論理模型クラスへの変換が必要です。マシンを実行するだけであれば、論理模型オブジェクトの構築方法について把握しておけば十分です。このセクションでは、論理模型クラスの内部で行われている変換結果の取得方法や変換方法など上級者向けの機能も含めて紹介します。

論理模型オブジェクトの構築

入力模型クラスと論理模型クラスの対応関係は次の通りです。

論理模型クラス

入力模型クラス

BinaryQuadraticModel

BinaryPoly BinaryMatrix BinaryConstraint BinaryConstraints

BinaryIntPolyBinaryIntMatrix BinaryIntConstraint BinaryIntConstraints

BinaryIntQuadraticModel

BinaryIntPolyBinaryIntMatrix BinaryIntConstraint BinaryIntConstraints

IsingQuadraticModel

IsingPoly IsingMatrix IsingConstraint IsingConstraints

IsingIntPoly IsingIntMatrix IsingIntConstraint IsingIntConstraints

IsingIntQuadraticModel

IsingIntPoly IsingIntMatrix IsingIntConstraint IsingIntConstraints

論理模型クラスの構築は下記のようにして行います。

多項式による構築

バイナリ変数またはイジング変数の多項式オブジェクトを論理模型に変換します。

from amplify import BinarySymbolGenerator, BinaryQuadraticModel

gen = BinarySymbolGenerator()
q = gen.array(2)  # 長さ 2 の変数配列を生成
f = 2 * q[0] * q[1] + q[0] + q[1] - 1
model = BinaryQuadraticModel(f)

input_poly プロパティで入力模型を多項式形式で確認できます。

>>> f
2 q_0 q_1 + q_0 + q_1 - 1
>>> model.input_poly
2 q_0 q_1 + q_0 + q_1 - 1

三次以上の高次多項式についても扱うことが出来ます。この場合、次数下げアルゴリズムにより補助変数を用いて二次形式へ変換されます。

from amplify import BinarySymbolGenerator, BinaryQuadraticModel

gen = BinarySymbolGenerator()
q = gen.array(3)  # 長さ 3 の変数配列を生成
f = 3 * q[0] * q[1] * q[2] + 2 * q[0] * q[1] + q[0] - 1  # 3次多項式
model = BinaryQuadraticModel(f)
>>> f
3 q_0 q_1 q_2 + 2 q_0 q_1 + q_0 - 1
>>> model.input_poly
3 q_0 q_1 q_2 + 2 q_0 q_1 + q_0 - 1

二次多項式に変換された論理模型は次のようにして確認できます。変数のインデックスについては入力変数とは異なるマッピングになっていることに注意してください。

>>> model.logical_poly
5 q_0 q_1 + 3 q_0 q_2 - 3 q_0 q_3 + 3 q_1 q_2 - 3 q_1 q_3 - 3 q_2 q_3 + q_0 + 3 q_3 - 1

参考

Amplify SDK に実装されている次数下げアルゴリズムの詳細とその選択方法については 高次多項式の次数下げ を参照してください。

行列による構築

行列オブジェクトを論理模型に変換します。

from amplify import BinaryMatrix, BinaryQuadraticModel

m = BinaryMatrix(3)
m[0, 0] = -2
m[0, 1] = 1
m[1, 2] = -1
m[2, 2] = 1
model = BinaryQuadraticModel(m)

input_matrix プロパティで入力模型を行列形式で確認できます。行列と定数項のペアで返却されることに注意してください。

>>> m
[[-2, 1, 0],
 [0, 0, -1],
 [0, 0, 1]]
>>> model.input_matrix
([[-2, 1, 0],
 [0, 0, -1],
 [0, 0, 1]], 0.0)

制約条件による構築

単一の制約条件

制約条件オブジェクトを論理模型に変換します。

from amplify import BinarySymbolGenerator, BinaryQuadraticModel
from amplify.constraint import one_hot

gen = BinarySymbolGenerator()
q = gen.array(4)  # 長さ 4 の変数配列を生成
c1 = one_hot(q[:3])   # q_0 + q_1 + q_2 == 1
model = BinaryQuadraticModel(c1)

input_constraints プロパティで制約条件を確認できます。

>>> model.input_constraints
[(q_0 + q_1 + q_2 == 1, 1)]

複数の制約条件

複数の制約条件オブジェクトを論理模型に変換します。

from amplify import BinarySymbolGenerator, BinaryQuadraticModel
from amplify.constraint import one_hot

gen = BinarySymbolGenerator()
q = gen.array(4)  # 長さ 4 の変数配列を生成
c1 = one_hot(q[:3])   # q_0 + q_1 + q_2 == 1
c2 = one_hot(q[1:])   # q_1 + q_2 + q_3 == 1
model = BinaryQuadraticModel(c1 + c2)
>>> model.input_constraints
[(q_0 + q_1 + q_2 == 1, 1), (q_1 + q_2 + q_3 == 1, 1)]

多項式と制約条件による構築

多項式に対して制約条件を課すという形で論理模型オブジェクトを構築します。

from amplify import BinarySymbolGenerator, BinaryQuadraticModel
from amplify.constraint import one_hot

gen = BinarySymbolGenerator()
q = gen.array(4)  # 長さ 4 の変数配列を生成
f = 2 * q[0] * q[1] * q[2] + q[0] * q[1] + q[0] + q[1] + q[2] - 1
c1 = one_hot(q[:3])   # q_0 + q_1 + q_2 == 1
c2 = one_hot(q[1:])   # q_1 + q_2 + q_3 == 1
model = BinaryQuadraticModel(f, c1 + c2)
>>> model.input_poly
2 q_0 q_1 q_2 + q_0 q_1 + q_0 + q_1 + q_2 - 1
>>> model.input_constraints
[(q_0 + q_1 + q_2 == 1, 1), (q_1 + q_2 + q_3 == 1, 1)]

多項式オブジェクトに制約条件を加算することで、論理模型オブジェクトを生成することも出来ます。詳細は「制約条件クラスの加算演算子」を参照してください。

from amplify import BinarySymbolGenerator, BinaryQuadraticModel
from amplify.constraint import one_hot

gen = BinarySymbolGenerator()
q = gen.array(4)  # 長さ 4 の変数配列を生成
f = 2 * q[0] * q[1] * q[2] + q[0] * q[1] + q[0] + q[1] + q[2] - 1
c1 = one_hot(q[:3])   # q_0 + q_1 + q_2 == 1
c2 = one_hot(q[1:])   # q_1 + q_2 + q_3 == 1
model = f + c1 + c2
>>> model.input_poly
2 q_0 q_1 q_2 + q_0 q_1 + q_0 + q_1 + q_2 - 1
>>> model.input_constraints
[(q_0 + q_1 + q_2 == 1, 1), (q_1 + q_2 + q_3 == 1, 1)]

行列と制約条件による構築

行列に対して制約条件を課す形で論理模型オブジェクトを構築します。

from amplify import BinarySymbolGenerator, BinaryMatrix, BinaryQuadraticModel
from amplify.constraint import one_hot

gen = BinarySymbolGenerator()
q = gen.array(4)  # 長さ 4 の変数配列を生成
m = BinaryMatrix(3)
m[0, 0] = -2
m[0, 1] = 1
m[1, 2] = -1
m[2, 2] = 1
c1 = one_hot(q[:3])   # q_0 + q_1 + q_2 == 1
c2 = one_hot(q[1:])   # q_1 + q_2 + q_3 == 1
model = BinaryQuadraticModel(m, c1 + c2)
>>> model.input_matrix
([[-2, 1, 0],
 [0, 0, -1],
 [0, 0, 1]], 0.0)
>>> model.input_constraints
[(q_0 + q_1 + q_2 == 1, 1), (q_1 + q_2 + q_3 == 1, 1)]

高次多項式の次数下げ

Amplify SDK には高次多項式を二次多項式に次数下げするため次の方法が実装されています。論理模型の構築時に手法とパラメータを指定することが出来ます。

NTR-KZFD 1 2

係数が負であるようなバイナリ変数多項式の項について、バイナリ補助変数 \(x\) を用いて下記の変換を行います。どのような次数 \(n\) の項でも必要な補助変数は一つで済みますが、係数 \(p\) が負の場合にしか使用できません。

\[p \prod_{i =1}^{n}{q_i} \rightarrow x p \left( S + 1 - n \right) \ \left( p < 0 \right)\]
\[S = \sum_{i =1}^{n}{q_i}\]

PTR-Ishikawa 3

バイナリ変数の次数 \(n\) の項について、バイナリ補助変数 \(x_i\) を用いて下記の変換を行います。係数 \(p\) が正の場合にも使用できますが、必要な補助変数の数は \(\mathrm{floor} \left( \left(n - 1\right) / 2 \right)\) です。

\[p \prod_{i =1}^{n}{q_i} \rightarrow \left| p \right| \frac{1}{2} S \left( S - 1 \right) - \left| p \right| \sum_{k = 1}^{\mathrm{floor} \left( \left(n - 1\right) / 2 \right)}{x_k \left( c_{n,k} \left( S - 2 k \right) + 1 \right) }\]
\[\begin{split}c_{n,k} = \begin{cases} 1, & \text{if $n$ is odd and $k = \mathrm{floor} \left( \left(n - 1\right) / 2 \right)$} \\ 2, & \text{else} \end{cases}\end{split}\]
\[S = \sum_{i =1}^{n}{q_i}\]

PTR-Ishikawa (Ising)

Amplify SDK は PTR-Ishikawa のイジング変数版を独自に実装しています。バイナリ変数の次数 \(n\) の項について、イジング補助変数 \(y_i\) を用いて下記の変換を行います。係数 \(p\) の正負と \(n\) の偶奇で下記の2通りに場合分けされます。

  • \(p > 0 \text{ and $n$ is odd}\), \(p < 0 \text{ and $n$ is even}\)

    \[p \prod_{i =1}^{n}{s_i} \rightarrow 2 \left| p \right| S^2 - 8 \left| p \right| \sum_{k = 1}^{\mathrm{floor} \left( n / 2 \right)}{x_k \left( S - 2 k + 1 \right) } - \left| p \right|\]
    \[S = \sum_{i =1}^{n}{\frac{s_i + 1}{2}} \quad x_k = \frac{y_k + 1}{2}\]
  • \(p > 0 \text{ and $n$ is even}\), \(p < 0 \text{ and $n$ is odd}\)

    \[p \prod_{i =1}^{n}{q_i} \rightarrow 2 \left| p \right| \left( S - 1 \right)^2 - 8 \left| p \right| \sum_{k = 1}^{\mathrm{floor} \left( \left(n - 1\right) / 2 \right)}{x_k \left( S - 2 k \right) } - \left| p \right|\]
    \[S = \sum_{i =1}^{n}{\frac{s_i + 1}{2}} \quad x_k = \frac{y_k + 1}{2}\]

Substitution 4

2つのバイナリ変数の積について、バイナリ補助変数 \(x\) を用いて下記の置換を行い、これを制約条件と見なしペナルティ関数 \(g\) を付与します。4次以上の項についてはこの置換を再帰的に行います。必要な補助変数の数は次数 \(n\) の項について \(n-2\) ですが、置換を全ての項について同時に行うことで、補助変数を共有出来ることがあります。ただし、適切なペナルティ関数の強さは一般に非自明なので調整が必要です。

\[q_1 q_2 \rightarrow x\]
\[g \left(q_1, q_2, x \right) = q_1 q_2 − 2 q_1 x − 2 q_2 x + 3 x\]

アルゴリズムの指定

多項式オブジェクトから論理模型を構築する際に、method キーワード引数として QuadratizationMethod クラスを与えると次数下げアルゴリズムを選択できます。

from amplify import (
    BinarySymbolGenerator,
    BinaryQuadraticModel,
    QuadratizationMethod,
    pair_sum,
)

gen = BinarySymbolGenerator()
q = gen.array(8)  # 長さ 8 の変数配列を生成
f = pair_sum(q) ** 4  # 高次多項式の作成例

# Substitution 法を用いて次数下げを行う
BinaryQuadraticModel.substituion_multiplier = 2.0  # Substitution のペナルティ関数の強さを指定
model = BinaryQuadraticModel(f, method=QuadratizationMethod.SUBSTITUTION)
>>> model.num_input_vars   # 次数下げ前の変数の数
8
>>> model.num_logical_vars # 次数下げ後の変数の数
69

指定可能な値として下記が選択可能です。

QuadratizationMethod.ISHIKAWA

Ishikawa の方法を用いて次数下げを行います。バイナリ変数・イジング変数多項式の両方で指定が可能です。

QuadratizationMethod.ISHIKAWA_KZFD [デフォルト]

Ishikawa の方法と KZFD を組み合わせます。係数が負の項については KZFD を使用し、係数が正の項については Ishikawa を用います。イジング変数の多項式では KZFD 法が適用出来ないため、全ての項について Ishikawa の方法が使用されます。

QuadratizationMethod.SUBSTITUTION

Substitution の方法を用いて次数下げを行います。イジング変数の多項式に対しては未実装なため Ishikawa の方法が使用されます。

QuadratizationMethod.SUBSTITUTION_KZFD

Substitution の方法と KZFD を組み合わせます。係数が負の項については KZFD を使用し、係数が正の項については Substitution を用います。イジング変数の多項式に対しては未実装なため Ishikawa の方法が使用されます。

それぞれの方法には長所と短所があります。Ishikawa や KZFD の方法は単一の項に対しては補助変数の使用を少なく出来ますが、複数の項に渡って何度も同じ変数に対して次数下げを行うような場合には Substitution の方法の方が効率が良いこともあります。一方で、Substitution の方法は置換に対する制約条件としてペナルティ関数を設定するため、ペナルティ関数の強さの設定が必要になります。Ishikawa や KZFD の方法にはこれが必要ありません。Substitution のペナルティ関数の強さは Amplify SDK が置換時に推定しこれを初期値としますが、精度の良い解を得るためには調整が必要かもしれません。また、Substitution 対象を貪欲法で決めるので、必ずしも置換変数の決定について最適化されているわけではありません。

from amplify import BinaryQuadraticModel

# Substitution のペナルティ関数の強さを指定
# 自動推定値からの比を与える (1.01 がデフォルト)
BinaryQuadraticModel.substituion_multiplier = 2.0

小規模な問題についてはデフォルトの ISHIKAWA_KZFD を用い、もし次数下げによって問題サイズが爆発的に増加してしまった場合には、SUBSTITUTION, SUBSTITUTION_KZFD を試してみるという方針を推奨します。ただし、Substitution の方法はペナルティ関数の強さの調整が必要かもしれないことに注意してください。

参考

様々な次数下げの方法に関するレビューが "Quadratization in discrete optimization and quantum mechanics" 5 にまとめられています。

1

V. Kolmogorov and R. Zabih, “What energy functions can be minimized via graph cuts?” IEEE Transactions on Pattern Analysis and Machine Intelligence 26, 147–159 (2004).

2

D. Freedman and P. Drineas, “Energy Minimization via Graph Cuts: Settling What is Possible,” in 2005 IEEE Computer Society Conference on Computer Vision and Pattern Recognition (CVPR’05), Vol. 2 (IEEE, 2005) pp. 939–946.

3

H Ishikawa, “Transformation of General Binary MRF Minimization to the First-Order Case,” IEEE Transactions on Pattern Analysis and Machine Intelligence 33, 1234–1249 (2011).

4

I. G. Rosenberg, “Reduction of Bivalent Maximization to the Quadratic Case,” Cahiers du Centre d’Etudes de Recherche Operationnelle 17, 71–74 (1975).

5

Nike Dattani, "Quadratization in discrete optimization and quantum mechanics" http://arxiv.org/abs/1901.04405

論理模型クラスの内部

論理模型クラスは入力模型オブジェクトに対して、イジングマシンが扱える二次多項式への変換と論理変数インデックスへのマッピングを行います。論理模型の内部情報として、入力模型からの変換情報と変換結果の取得方法について説明します。

注釈

内部情報の取得に関するインタフェースは今後変更される可能性があります。

次の表は論理模型クラスの内部表現を返却する読み込み専用プロパティの一覧です。

入力レイヤ

論理レイヤ

論理模型

多項式オブジェクト

input_poly

logical_poly

logical_model_poly

行列オブジェクト

input_matrix

logical_matrix

logical_model_matrix

制約条件オブジェクト

input_constraints

input_constraints/penalty

N/A

入力されたオブジェクトは二次多項式への次数下げとインデックスの再割り当てが行われます。変換前後のオブジェクトは上記のプロパティにて取得が可能です。入力インデックスと論理インデックスの関係は logical_mapping プロパティで辞書として取得出来ます。この辞書はキーを入力インデックス、値を論理インデックスとします。

from amplify import BinarySymbolGenerator, BinaryQuadraticModel

gen = BinarySymbolGenerator()
q = gen.array(4)  # 長さ 4 の変数配列を生成
f = 2 * q[0] * q[1] * q[2] + q[0] * q[1] + q[0] + q[1] + q[2] - 1
model = BinaryQuadraticModel(f)
>>> model.input_poly
2 q_0 q_1 q_2 + q_0 q_1 + q_0 + q_1 + q_2 - 1
>>> model.logical_poly
3 q_0 q_1 + 2 q_0 q_2 - 2 q_0 q_3 + 2 q_1 q_2 - 2 q_1 q_3 - 2 q_2 q_3 + q_0 + q_1 + q_2 + 2 q_3 - 1
>>> model.logical_mapping
{0: 0, 1: 1, 2: 2}

論理模型オブジェクトには制約条件オブジェクトを後から追加することも出来ます。

from amplify.constraint import one_hot

c1 = one_hot(q[:3])
c2 = one_hot(q[1:])
model += c1 + c2
>>> model.input_constraints
[(q_0 + q_1 + q_2 == 1, 1), (q_1 + q_2 + q_3 == 1, 1)]

最終的に論理模型として目的関数と制約条件のペナルティ関数が足されます。

>>> model.logical_model_poly
5 q_0 q_1 + 4 q_0 q_2 - 2 q_0 q_3 + 6 q_1 q_2 - 2 q_1 q_3 + 2 q_1 q_4 - 2 q_2 q_3 + 2 q_2 q_4 - q_1 - q_2 + 2 q_3 - q_4 + 1

上記は多項式として取得していますが、行列形式でも同様に取得が可能です。

論理模型クラスのメソッド

入力変数の数の取得

入力模型に含まれる変数の数を取得します。

from amplify import BinarySymbolGenerator, BinaryQuadraticModel
from amplify.constraint import one_hot

gen = BinarySymbolGenerator()
q = gen.array(4)  # 長さ 4 の変数配列を生成
f = 2 * q[0] * q[1] * q[2] + q[0] * q[1] + q[0] + q[1] + q[2] - 1
c = one_hot(q)   # q_0 + q_1 + q_2 + q_3 == 1
model = BinaryQuadraticModel(f, c)

多項式 f と制約条件 c に現れる変数の数が返却されます。

>>> model.num_input_vars
4

論理変数の数の取得

論理模型の内部表現である二次多項式に含まれる変数の数を取得します。

from amplify import BinarySymbolGenerator, BinaryQuadraticModel
from amplify.constraint import one_hot

gen = BinarySymbolGenerator()
q = gen.array(4)  # 長さ 4 の変数配列を生成
f = 2 * q[0] * q[1] * q[2] + q[0] * q[1] + q[0] + q[1] + q[2] - 1
c = one_hot(q)   # q_0 + q_1 + q_2 + q_3 == 1
model = BinaryQuadraticModel(f, c)

必ずしも入力模型の変数の数に一致しないことに注意して下さい。上記の例では、多項式 f は高次多項式なので、補助変数を用いて二次多項式に変換されます。そのため、論理模型の変数の数は、入力模型の変数に加えて必要に応じて補助変数を合わせた数となります。次のようにして論理模型とその変数の数が確認できます。

>>> model.logical_model_poly
5 q_0 q_1 + 4 q_0 q_2 - 2 q_0 q_3 + 2 q_0 q_4 + 4 q_1 q_2 - 2 q_1 q_3 + 2 q_1 q_4 - 2 q_2 q_3 + 2 q_2 q_4 + 2 q_3 - q_4
>>> model.num_logical_vars
5

制約条件オブジェクトの取得

制約条件オブジェクトのコンテナを取得します。

from amplify import BinarySymbolGenerator, BinaryQuadraticModel
from amplify.constraint import one_hot

gen = BinarySymbolGenerator()
q = gen.array(4)  # 長さ 4 の変数配列を生成
f = 2 * q[0] * q[1] * q[2] + q[0] * q[1] + q[0] + q[1] + q[2] - 1
c = one_hot(q)   # q_0 + q_1 + q_2 + q_3 == 1
model = BinaryQuadraticModel(f, c)
>>> model.input_constraints
[(q_0 + q_1 + q_2 + q_3 == 1, 1)]
>>> model.logical_model_poly
5 q_0 q_1 + 4 q_0 q_2 - 2 q_0 q_3 + 2 q_0 q_4 + 4 q_1 q_2 - 2 q_1 q_3 + 2 q_1 q_4 - 2 q_2 q_3 + 2 q_2 q_4 + 2 q_3 - q_4

強さの係数値については論理模型の構築後にも変更が可能です。変更後は論理模型が変化します。

>>> model.input_constraints[0][1] = 2
>>> model.input_constraints
[(q_0 + q_1 + q_2 + q_3 == 1, 2)]
>>> model.logical_model_poly
7 q_0 q_1 + 6 q_0 q_2 - 2 q_0 q_3 + 4 q_0 q_4 + 6 q_1 q_2 - 2 q_1 q_3 + 4 q_1 q_4 - 2 q_2 q_3 + 4 q_2 q_4 - q_0 - q_1 - q_2 + 2 q_3 - 2 q_4 + 1

制約条件の充足検査

論理模型に含まれる制約条件オブジェクトについて check_constraints() を使用すると一括で制約充足検査が行われます。与えることの出来る引数の形式は is_satisfied() と同様です。詳しくは こちら を参照してください。

この関数は得られた出力解について、どの制約条件を満たしているか、またはどの制約条件を満たさなかったのかを調査するために用いられます。またその時の論理模型における制約条件の強さの係数値についても、制約条件オブジェクトの取得 と同様に取得・変更が可能です。

from amplify import BinarySymbolGenerator
from amplify.constraint import one_hot, less_equal

gen = BinarySymbolGenerator()
q = gen.array(3)  # 長さ 3 の変数配列を生成
f = 2 * q[0] * q[1] * q[2] + q[0] * q[1] + q[0] + q[1] + q[2] - 1
c1 = one_hot(q[0] + q[2])  # q_0 + q_2 == 1
c2 = less_equal(q[0] + q[1], 1)  # q_0 + q_1 <= 1
model = f + c1 + c2
checked = model.check_constraints({0: 1, 1: 1, 2: 0})  # q[0] = q[1] = 1, q[2] = 0
>>> checked
[((q_0 + q_2 == 1, 1), True), ((q_0 + q_1 <= 1, 1), False)]

出力は制約条件オブジェクトと結果のペアのコンテナで返されます。上記では q = [1, 1, 0] が制約条件を満たすかをチェックし、その結果として q_0 + q_2 == 1 は満たすが q_0 + q_1 <= 1 は充たさないことを意味します。ここでは解を Solver クラスの出力を与えることを想定して辞書で作成していますが、配列を渡すことも可能です。

check_constraints() 関数を利用する例として、制約条件を満たさなかった場合に、その制約条件オブジェクトに対して制約条件オブジェクトの重みを変更するという操作が可能です。

for c, r in checked:
    if r is False:
        c[1] *= 2
>>> model.input_constraints
[(q_0 + q_2 == 1, 1), (q_0 + q_1 <= 1, 2)]

論理模型クラスの演算子

論理模型オブジェクトに対し制約条件オブジェクトや制約条件コンテナを加算すると制約条件が追加されます。詳細は 制約条件クラスの加算演算子 を参照してください。

from amplify import BinarySymbolGenerator, BinaryQuadraticModel

gen = BinarySymbolGenerator()
q = gen.array(4)  # 長さ 4 の変数配列を生成
f = 2 * q[0] * q[1] * q[2] + q[0] * q[1] + q[0] + q[1] + q[2] - 1
model = BinaryQuadraticModel(f)
>>> model.input_poly
2 q_0 q_1 q_2 + q_0 q_1 + q_0 + q_1 + q_2 - 1
>>> len(model.input_constraints)
0
from amplify.constraint import one_hot

c1 = one_hot(q[:3])
c2 = one_hot(q[1:])
model += c1 + c2
>>> model.input_constraints
[(q_0 + q_1 + q_2 == 1, 1), (q_1 + q_2 + q_3 == 1, 1)]