Solver

このセクションでは論理模型のソルバーについて説明します。

参考

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

また説明に現れるクライアントオブジェクトの詳細については、Client を参照してください。

ソルバークラスはイジングマシンのクライアントを内包することでハードウェアを抽象化し、入力模型・論理模型を解くためのインタフェースを提供します。ソルバークラスを用いることで、様々なイジングマシンに対して仕様の差異を意識する必要がなくなり、統一的なインタフェースでイジングマシンを実行し解を求めることが可能になります。

ソルバーオブジェクトの構築

ソルバーはクライアントオブジェクトを用いて次のように構築されます。

from amplify import BinaryPoly, Solver
from amplify.client import FixstarsClient

client = FixstarsClient()
client.token = "xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx"
client.parameters.timeout = 1000  # タイムアウト1秒

solver = Solver(client)

後からクライアントを設定することも出来ます。

from amplify import Solver
from amplify.client import FixstarsClient

client = FixstarsClient()
client.token = "xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx"
client.parameters.timeout = 1000  # タイムアウト1秒

solver = Solver()
solver.client = client

参考

各マシンに対応するクライアントクラスの詳細や用意されているパラメータについては Client を参照してください。

ソルバーの実行と解の取得

solve() メソッドには論理模型オブジェクトを与えることでイジングマシンを実行できます。

次の論理模型クラスの入力が可能です。

簡便のため、solve() メソッドには多項式、行列、制約条件オブジェクトを直接与えることも可能です。この場合は与えたオブジェクトの種類に応じて、自動的に論理模型オブジェクトが一時的に作成されます。この呼び出し方法は簡易的なものなので、目的関数と制約条件の組み合わせなどは与えられません。明示的に論理模型オブジェクトを構築するか、または 制約条件クラスの加算演算子 を用いてください。

多項式を用いる場合は次のように引数を与えます。

行列を用いる場合は次のように引数を与えます。第二引数は定数項を表します。

制約条件オブジェクトを用いる場合は次のように引数を与えます。

実行結果の取得

solve() メソッドを実行すると実行結果が返却されます。以下は Amplify AE のクライアントを使用する例です。

from amplify import BinarySymbolGenerator, Solver
from amplify.client import FixstarsClient

gen = BinarySymbolGenerator()
q = gen.array(3)
f = 2 * q[0] * q[1] * q[2] - q[0] * q[1] + q[2] + 1

client = FixstarsClient()
client.token = "xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx"
client.parameters.timeout = 1000  # タイムアウト1秒

solver = Solver(client)
result = solver.solve(f)

>>> f
2 q_0 q_1 q_2 - q_0 q_1 + q_2 + 1
>>> [f"energy = {s.energy}, q = {q.decode(s.values)}" for s in result]
['energy = 0.0, q = [1. 1. 0.]']

solve() メソッドの実行結果は下記のアトリビュートを持つオブジェクトです。

  • solutions : 実行結果が格納されたリストを取得します。各要素は以下のアトリビュートを持ちます。

    • energy : エネルギー値 (入力模型の評価値) を取得します。

    • values : 入力変数の値をリストで取得します。

    • frequency : 同一の解の個数を取得します。

    • is_feasible : 解が全ての制約条件を満たしているかを返します。解のフィルタリング によりデフォルトでは True の解だけが格納されます。

下記の特殊メソッドが定義されているので、返却値に対して for ループや要素アクセスで solutions の要素を取得できます。

  • __getitem__ : 透過的に solutions の要素アクセス solutions[n] を返却します。

  • __len__ : 透過的に solutions の要素数 len(solutions) を返却します。

  • __iter__ : 透過的に solutions のイテレータを返却します。

通常は、最初の要素 (result[0]) から次のように解を取り出せば実行結果のうち最も良い解が取得できます。

>>> result[0].energy
0.0
>>> result[0].values
{2: 0, 1: 1, 0: 1}

ただし次で説明するように、制約条件が与えられた場合には実行可能解だけが格納されるようにフィルタされます。もし result の長さが 0 の場合、制約条件を満たす解が得られなかったことを意味します。

解のフィルタリング

solve() メソッドに制約条件を与えた場合に、デフォルトでは自動的に制約条件を満たさない入力模型の解をフィルタします。次の例は q[0] + q[1] == 1 となる制約を課しています。

from amplify import BinarySymbolGenerator, Solver
from amplify.constraint import one_hot
from amplify.client import FixstarsClient

gen = BinarySymbolGenerator()
q = gen.array(3)
f = 2 * q[0] * q[1] * q[2] - q[0] * q[1] + q[2] + 1
c = one_hot(q[0] + q[1])  # 制約: q[0] + q[1] == 1

client = FixstarsClient()
client.token = "xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx"
client.parameters.timeout = 1000  # タイムアウト1秒

model = f + c
solver = Solver(client)
result = solver.solve(model)

>>> f
2 q_0 q_1 q_2 - q_0 q_1 + q_2 + 1
>>> result[0].energy
1.0
>>> result[0].values
{2: 0, 1: 1, 0: 0}
>>> result[0].is_feasible
True

制約を満たす解が得られなかった場合は、実行結果の SolverResult の長さは 0 になります。次の例では矛盾する制約を課すことでこの様子を確認しています。

from amplify import BinarySymbolGenerator, Solver
from amplify.constraint import equal_to
from amplify.client import FixstarsClient

gen = BinarySymbolGenerator()
q = gen.array(3)
f = 2 * q[0] * q[1] * q[2] - q[0] * q[1] + q[2] + 1
c1 = equal_to(q[0] + q[1], 1)  # 制約: q[0] + q[1] == 1
c2 = equal_to(q[0] + q[1], 2)  # 制約: q[0] + q[1] == 2 (c1と矛盾)

client = FixstarsClient()
client.token = "xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx"
client.parameters.timeout = 1000  # タイムアウト1秒

model = f + c1 + c2
solver = Solver(client)
result = solver.solve(model)

>>> result[0]
Traceback (most recent call last):
File "<stdin>", line 1, in <module>
IndexError
>>> len(result)
0

上記の実行可能解以外をフィルタする機能は、ソルバークラスの filter_solution を設定することで無効化することが出来ます。

solver.filter_solution = False
result = solver.solve(model)

>>> len(result)
1
>>> result[0].energy
0.0
>>> result[0].values
{2: 0, 1: 1, 0: 1}
>>> result[0].is_feasible
False

得られた解のアトリビュート is_feasible は False となっており、これは実行可能解ではない (少なくとも一つの制約条件が満たされない) ことを意味します。

どの制約条件を満たさなかったのかについては check_constraints() に変数配列を与えることで確認できます。

>>> model.check_constraints(result[0].values)
[((q_0 + q_1 == 1, 1), False), ((q_0 + q_1 == 2, 1), True)]

これは、得られた最初の解の配列が q_0 + q_1 == 1.000000 については制約条件を満たしていること、q_0 + q_1 == 2.000000 については制約条件を満たしていないことを意味します。

制約条件のフィルタリング

上記のように、制約条件を満たす解が得られなかった場合に、 filter_solution と check_constraints() メソッドを用いることで、どの制約条件を満たせなかったのかを確認できました。しかし、その制約条件がどのような意味を持つのかは print するだけでは判別が困難です。

そこで、制約条件へのラベル付け を用いてラベル付けすることで、どの制約条件が満たせたのか、満たせなかったのかを判別する方法を紹介します。

次の例では one-hot 制約であることが解るように制約条件にラベルを付けた場合の実行例です。

from amplify import BinarySymbolGenerator, Solver
from amplify.constraint import one_hot, less_equal, greater_equal
from amplify.client import FixstarsClient

gen = BinarySymbolGenerator()
q = gen.array(3, 3)  # 3x3 の変数配列を作成
f = 5 * q.sum() # 目的関数
c0 = sum(one_hot(q[i], label=f"one_hot_r{i}") for i in range(3))  # 全ての行に対する one-hot 制約
c1 = sum(one_hot(q[:, i], label=f"one_hot_c{i}") for i in range(3))  # 全ての列に対する one-hot 制約
c2 = one_hot(q.diagonal(), label=f"one_hot_d")  # 対角方向の one-hot 制約

model = f + c0 + c1 + c2

client = FixstarsClient()
client.token = "xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx"
client.parameters.timeout = 1000  # タイムアウト1秒

solver = Solver(client)
solver.filter_solution = False  # 制約条件フィルタを無効化
result = solver.solve(model)

一部の制約条件が満たせなかったことがわかります。

>>> model.check_constraints(result[0].values)
[((one_hot_r0: q_0 + q_1 + q_2 == 1, 1), False),
 ((one_hot_r1: q_3 + q_4 + q_5 == 1, 1), False),
 ((one_hot_r2: q_6 + q_7 + q_8 == 1, 1), True),
 ((one_hot_c0: q_0 + q_3 + q_6 == 1, 1), False),
 ((one_hot_c1: q_1 + q_4 + q_7 == 1, 1), False),
 ((one_hot_c2: q_2 + q_5 + q_8 == 1, 1), True),
 ((one_hot_d: q_0 + q_4 + q_8 == 1, 1), True)]

満たせなかった制約条件から label を用いて判別することで、行に対する One-hot 制約だけを抽出することが出来ます。

>>> [c for c, r in model.check_constraints(result[0].values) if r is False and "one_hot_r" in c.label]
[(one_hot_r0: q_0 + q_1 + q_2 == 1, 1), (one_hot_r1: q_3 + q_4 + q_5 == 1, 1)]

このように、制約条件を満たせなかった場合にどの制約条件なのかを特定したり、重みを変更して再実行する等、柔軟な処理が可能になります。上記の例では抽出した制約条件の重みを大きくして再実行することで、制約が全て充足される可能性があります。

解のソート

論理模型と入力模型の解をエネルギー値の昇順でソートします。この機能はクライアントが複数の解を出力する場合に適用されます。これはデフォルトで有効です。ソートされている場合には solve() メソッドの実行結果において先頭の要素が最も良い解ですが、無効にすると解の格納順はマシンの出力順に依存します。

from amplify import Solver
from amplify.client import FixstarsClient

client = FixstarsClient()
solver = Solver(client)
# 複数の解をソートしない (マシンの出力順で処理する)
solver.sort_solution = False

解の重複排除

ソルバークラスの出力する解の配列に重複が発生した場合、通常は重複を排除する処理が行われます。これはデフォルトで有効です。この機能がソルバークラスに実装されている背景を以下で説明します。

注釈

通常は重複排除機能を無効に設定する必要はありません。イジングマシンの出力とソルバークラスが行う解の解釈処理をデバッグする場合を想定して用意しています。

例えば、不等式制約 less_equal() を設定した場合に deduplicate を無効に設定すると、次のように出力解に重複が発生する場合があります。

from amplify import BinarySymbolGenerator, BinaryQuadraticModel, Solver
from amplify.constraint import less_equal
from amplify.client import FixstarsClient

gen = BinarySymbolGenerator()
q = gen.array(4)
f = 4 * q[0] + 3 * q[1] + 2 * q[2] + q[3]
g = less_equal(f, 3)

client = FixstarsClient()
client.token = "xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx"
client.parameters.timeout = 1000  # タイムアウト1秒
client.parameters.outputs.duplicate = True  # エネルギー値が同一の解を異なる解とみなす

model = BinaryQuadraticModel(g)
solver = Solver(client)
solver.deduplicate = False  # 重複解を区別する
result = solver.solve(model)

>>> [f"energy = {s.energy}, q = {q.decode(s.values)}, frequency = {s.frequency}" for s in result]
['energy = 0.0, q = [0., 0., 0., 0.], frequency = 1',
 'energy = 0.0, q = [0., 0., 0., 1.], frequency = 1',
 'energy = 0.0, q = [0., 0., 0., 1.], frequency = 1',
 'energy = 0.0, q = [0., 0., 0., 1.], frequency = 1',
 'energy = 0.0, q = [0., 0., 1., 0.], frequency = 1',
 'energy = 0.0, q = [0., 0., 1., 0.], frequency = 1',
 'energy = 0.0, q = [0., 0., 1., 0.], frequency = 1',
 'energy = 0.0, q = [0., 0., 1., 1.], frequency = 1',
 'energy = 0.0, q = [0., 1., 0., 0.], frequency = 1']

注釈

Amplify Annealing Engine はデフォルトではエネルギー値が同一の解を区別せずに一つだけ出力します。client.parameters.outputs.duplicate = True を設定することで、エネルギー値は同一であっても解の配列が異なる場合に、それらを区別して複数出力するような動作に変更されます。

ソルバークラスはイジングマシンの出力を元に問題の実行時と逆のステップを踏んで、物理模型、論理模型、入力模型の各レイヤで解を解釈します。この時、解が重複してしまう可能性があるため、精査し重複をまとめる処理がソルバークラスには実装されています。同一の解が複数回出力される理由として以下が挙げられます。

  • イジングマシンの出力解 (物理模型の解) に重複がある

  • 物理模型の解を論理模型でデコードした解 (論理模型の解) に重複がある

  • 論理模型の解を入力模型でデコードした解 (ソルバーの出力) に重複がある

一つ目はイジングマシンの設定や動作仕様に基づきます。マシンによっては重複する解をまとめず異なる解として出力する場合があります。後者二つについては、物理模型における「グラフ埋め込み」が行われた場合や、論理模型における「補助変数を用いた定式化」を用いた場合において重複が発生してしまう可能性があります。

例えば上記の不等式制約について Amplify Annealing Engine を用いた場合には三つ目が該当しました。不等式制約の定式化に補助変数を用います。論理模型において補助変数を含めて解の解釈をした際には重複が無かったものの、出力解には補助変数は含まれないため、補助変数を除いた結果では重複していたと考えられます。

ソルバークラスの重複排除機能が働くと以下のように出力されます。

solver.deduplicate = True  # 重複する解をまとめる (デフォルト動作)
result = solver.solve(model)

>>> [f"energy = {s.energy}, q = {q.decode(s.values)}, frequency = {s.frequency}" for s in result]
['energy = 0.0, q = [0, 0, 0, 0], frequency = 1',
 'energy = 0.0, q = [0, 0, 0, 1], frequency = 3',
 'energy = 0.0, q = [0, 0, 1, 0], frequency = 3',
 'energy = 0.0, q = [0, 0, 1, 1], frequency = 1',
 'energy = 0.0, q = [0, 1, 0, 0], frequency = 1']

得られた解の配列の重複がまとめられ、そのような解について frequency が加算されたことが確認されます。

ソルバークラスの内部

ソルバークラスの内部では次の手順でイジングマシンを実行し解を出力します。

  1. ソルバークラスにイジングマシンのクライアントオブジェクトを与える

  2. 入力模型または論理模型を受けとる

  3. ハードウェア仕様に基づき論理模型を物理模型に変換

    • 疎結合グラフを持つイジングマシンに対してはグラフ埋め込み

  4. 物理模型をクライアントに与えて実行

  5. 実行結果である物理模型の解を論理模型の解に変換

    • グラフ埋め込みによる物理変数制約を解決

  6. 論理模型の解から制約条件をチェックしフィルタ

  7. フィルタされた論理模型の解を入力模型の解に変換

このうち、クライアントが返却する「物理模型の解」と、制約条件をフィルタする前の「論理模型の解」については、次のようにして solve() メソッドの実行後に取得が可能です。

from amplify import BinaryPoly, BinarySymbolGenerator, Solver
from amplify.constraint import one_hot
from amplify.client.ocean import DWaveSamplerClient

gen = BinarySymbolGenerator()
q = gen.array(3)
f = 2 * q[0] * q[1] * q[2] - q[0] * q[1] + q[2] + 1
c = one_hot(q[0] + q[1])  # 制約: q[0] + q[1] == 1

client = DWaveSamplerClient()
client.solver = "Advantage_system6.3"
client.token = "XXXX-xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx"
client.parameters.num_reads = 100  # 実行回数

solver = Solver(client)
solver_result = solver.solve(f + c)

# 論理模型の解を取得
logical_result = solver.logical_result
# 物理模型の解を取得
client_result = solver.client_result

>>> [f"energy = {s.energy}, client_result  = {s.values}" for s in client_result[:1]]
['energy = 1.0, client_result  = [0, 0, 1, 0, 0, 0, 1, 0, 3, 3, 3, ...]']
>>> [f"energy = {s.energy}, logical_result = {s.values}" for s in logical_result[:1]]
['energy = 1.0, logical_result = [0, 0, 1, 0]']
>>> [f"energy = {s.energy}, solver_result  = {s.values}" for s in solver_result[:1]]
['energy = 1.0, solver_result  = [0, 1, 0]']

WIP

出力解の途中経過を取得するインタフェースは今後変更される可能性があります。

logical_result には論理模型 (logical_model_poly) に対してデコードされた解が LogicalResult オブジェクトとして格納されています。

client_result にはイジングマシンの出力結果が格納されています。マシンの出力をそのまま持つため、クライアントによってオブジェクトのクラスは異なります。詳細は Client に記載されている各クライアントの 「実行結果クラス」 を参照してください。

実行時間情報の取得

solve() メソッドの実行後に、マシンの実行時間情報を execution_time で取得できます。このプロパティは、マシンが求解に用いた時間をミリ秒単位に変換して返却します。

下記は FixstarsClient を用いて実行時間を取得する例です。

from amplify import BinaryPoly, BinarySymbolGenerator, Solver
from amplify.constraint import equal_to
from amplify.client import FixstarsClient

gen = BinarySymbolGenerator()
q = gen.array(3)
f = 2 * q[0] * q[1] * q[2] - q[0] * q[1] + q[2] + 1
c = equal_to(q[0] + q[1], 1)  # 制約: q[0] + q[1] == 1

client = FixstarsClient()
client.token = "xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx"
client.parameters.timeout = 1000  # タイムアウト1秒

solver = Solver(client)
solver.solve(f + c)

>>> solver.execution_time
969

指定したタイムアウト値に近い実行時間だったことが確認できます。

マシン固有の実行情報の取得

solve() メソッドの実行後にはマシン固有の実行情報を client_result で取得できます。返却されるオブジェクトは各クライアントの「実行結果クラス」 (Client に記載) で確認できます。

各クライアントで共通して client_result から取得可能な情報にマシンの実行時間情報があり、 timing で取得できます。返却されるオブジェクトは各クライアントの「実行時間クラス」 (Client に記載) で確認できます。実行時間クラスに含まれる情報や時間の単位は各マシンのAPI仕様に従います。例えば Fixstars AE ではミリ秒単位、D-Wave はマイクロ秒単位、Fujitsu は秒単位です。

下記は FixstarsClient の実行情報の取得例です。

from amplify import BinaryPoly, BinarySymbolGenerator, Solver
from amplify.constraint import equal_to
from amplify.client import FixstarsClient

gen = BinarySymbolGenerator()
q = gen.array(3)
f = 2 * q[0] * q[1] * q[2] - q[0] * q[1] + q[2] + 1
c = equal_to(q[0] + q[1], 1)  # 制約: q[0] + q[1] == 1

client = FixstarsClient()
client.token = "xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx"
client.parameters.timeout = 1000  # タイムアウト1秒

solver = Solver(client)
solver_result = solver.solve(f + c)
client_result = solver.client_result

>>> client_result.timing.cpu_time
107.565479
>>> client_result.timing.queue_time
83.35885699999992
>>> client_result.timing.time_stamps
[38.904337]
>>> client_result.execution_parameters.num_iterations
28

注釈

[Deprecated] annealing_time_ms は v0.7.0 から非推奨となりました。実行時間の取得には、execution_time をお使いください。

物理グラフへの埋め込み

ソルバークラスでは必要に応じて自動で入力模型や論理模型の物理模型へのグラフ埋め込みを行います。 具体的には Solver.client が HitachiClient 、DWaveClient や DWaveSamplerClient の場合にグラフ埋め込みが行われます。グラフ埋め込みについては こちらの解説 を参考にしてください。

グラフ埋め込みにより一つの論理変数を複数の物理変数 (チェイン) によって表すことで、論理変数間の相互作用を実現します。この時、チェイン内の物理変数が同じ値に揃うように、チェイン内の物理変数間に相互作用を張ります。この相互作用の大きさをチェイン重みと呼びます。 ソルバークラスではチェイン重みをある程度は自動で調整しますが、必要に応じて自動設定値からの比をプロパティ chain_strength に与えることが出来ます。また、論理変数の数が完全グラフ埋め込みが行えるサイズを超えた場合には、動的にグラフ埋め込みを探索します。この時の探索時間上限はプロパティ embedding_time_limit で変更が可能です。これらのプロパティは solve() メソッドの呼び出しより前に設定してください。

from amplify import Solver
from amplify.client.ocean import DWaveSamplerClient

client = DWaveSamplerClient()
client.token = "xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx"
client.solver = "Advantage_system4.1"
client.num_reads = 100

solver = Solver()
solver.client = client
solver.chain_strength = 2.0          # デフォルト: 1.0
solver.embedding_time_limit = 2000   # デフォルト: 1000ms