Solver

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

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

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

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

from amplify import BinaryPoly, gen_symbols, 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

物理グラフへの埋め込み

ソルバークラスでは必要に応じて入力模型や論理模型を物理模型へのグラフ埋め込みを自動で行います。 具体的には solver.clientHitachiClientDWaveClientDWaveSamplerClient の場合にグラフ埋め込みは行われます。

その際、一つの論理変数は複数の物理変数 (チェイン) によって表現されます。 チェイン内の物理変数が同じ向きに揃うように、チェイン内の物理変数間に相互作用を張ります。 その相互作用の大きさをチェイン重みと呼びます。 ソルバークラスはチェイン重みも自動で調整を行います。 また、必要に応じて係数を変更することが出来ます。

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

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

solver = Solver()
solver.client = client
solver.chain_strength = 2.0

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

solve() メソッドに入力模型や論理模型を与えることでイジングマシンを実行できます。

入力模型

入力模型については次の入力が可能です。

多項式

3次以上も含めた高次多項式の入力が可能です。

行列

二次多項式の行列表現の入力が可能です。第二引数は定数項を表します。

制約条件

制約条件オブジェクトの入力が可能です。

論理模型

論理模型については次の入力が可能です。

実行例

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

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

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

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

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

    • is_feasible : 解が全ての制約条件を満たしているかを返します。

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

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

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

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

q = gen_symbols(BinaryPoly, 8)
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.000000 q_0 q_1 q_2 - q_0 q_1 + q_2 + 1.000000
>>> [f"energy = {s.energy}, q[0] = {s.values[0]}, q[1] = {s.values[1]}, q[2] = {s.values[2]}" for s in result]
['energy = 0.0, q[0] = 1, q[1] = 1, q[2] = 0']

解のフィルタリング

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

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

q = gen_symbols(BinaryPoly, 8)
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秒

model = f + c
solver = Solver(client)
result = solver.solve(model)
>>> f
2.000000 q_0 q_1 q_2 - q_0 q_1 + q_2 + 1.000000
>>> [f"energy = {s.energy}, q[0] = {s.values[0]}, q[1] = {s.values[1]}, q[2] = {s.values[2]}, is_feasible = {s.is_feasible}" for s in result]
['energy = 1.0, q[0] = 0, q[1] = 1, q[2] = 0, is_feasible = True']

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

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

q = gen_symbols(BinaryPoly, 8)
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)
>>> f
2.000000 q_0 q_1 q_2 - q_0 q_1 + q_2 + 1.000000
>>> [f"energy = {s.energy}, q[0] = {s.values[0]}, q[1] = {s.values[1]}, q[2] = {s.values[2]}, is_feasible = {s.is_feasible}" for s in result]
[]

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

solver.filter_solution = False
result = solver.solve(model)
>>> [f"energy = {s.energy}, q[0] = {s.values[0]}, q[1] = {s.values[1]}, q[2] = {s.values[2]}, is_feasible = {s.is_feasible}" for s in result]
['energy = 1.0, q[0] = 1, q[1] = 0, q[2] = 0, is_feasible = False']

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

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

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

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

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

制約条件へのラベル付け によって付けたラベルを元に制約条件をフィルタリングすることが可能です。

次の例では one-hot 制約をフィルタして制約を満たしているか確認する方法を紹介します。

from amplify import BinaryPoly, gen_symbols, sum_poly
from amplify.constraint import equal_to, less_equal, greater_equal

q = gen_symbols(BinaryPoly, 3, 3)
f = - q[0][0] - q[1][1] - q[2][2]
one_hot = sum(equal_to(sum_poly(q[i]), 1, f"one_hot_{i}") for i in range(3)) # 行方向の one-hot 制約
c1 = less_equal(q[0][0] + q[1][0], 1, "less_equal")  # 制約: q[0][0] + q[1][0] <= 1
c2 = greater_equal(q[1][2] + q[2][2], 1, "greater_equal")  # 制約: q[2][2] + q[3][2] >= 1

model = f + one_hot + c1 + c2
>>> solution = [1, 1, 0, 0, 1, 1, 0, 0, 1]
>>> model.check_constraints(solution)
[((one_hot_0: q_0 + q_1 + q_2 == 1.000000, 1), False), ((one_hot_1: q_3 + q_4 + q_5 == 1.000000, 1), False), ((one_hot_2: q_6 + q_7 + q_8 == 1.000000, 1), False), ((less_equal: q_0 + q_3 <= 1, 1), True), ((greater_equal: q_5 + q_8 >= 1, 1), True)]

この例では制約が少ないため確認が容易ですが、制約が多い場合一つ一つ確認するのは手間です。 同じ種類の制約に似たようなラベルを付けておくことでまとめてどの程度制約を満たしていないか確認できます。

今回は one-hot 制約について確認してみましょう。 one-hot 制約には上で one_hot_0, one_hot_1 , one_hot_2 というラベルを付けているのでそれを元にフィルタリングできます。 満たしていない制約と満たしている制約の中からラベルに対して正規表現を用いて one-hot 制約を抜き出し、フィルタリングしてみましょう。

>>> import re
>>> unsat_one_hot = [(c, b) for (c, b) in model.check_constraints(solution) if not b and re.match('one_hot_[0-9]+', c.label)]
>>> unsat_one_hot
[((one_hot_0: q_0 + q_1 + q_2 == 1.000000, 2), False), ((one_hot_1: q_3 + q_4 + q_5 == 1.000000, 2), False)]
>>> sat_one_hot = [(c, b) for (c, b) in model.check_constraints(solution) if b and re.match('one_hot_[0-9]+', c.label)]
>>> sat_one_hot
[((one_hot_2: q_6 + q_7 + q_8 == 1.000000, 2), True)]
>>> print(f"unsatisfied: {len(unsat_one_hot)}, satisfied: {len(sat_one_hot)}")

この結果を見ると one-hot 制約は満たしていないものが 2 つ、満たしているものが 1 つあることが分かります。 イジングマシンから得られた解が制約を満たしていない場合、一般的にその制約の強さが十分大きくないことが考えられます。 そこで、 one-hot 制約の強さを 2 倍してみます。 先と同様にラベルに対して正規表現を用いて one-hot 制約を抜き出して操作を加えます。

>>> for c in model.input_constraints:
>>>     if re.match('one_hot_[0-9]+', c.label):
>>>         c[1] *= 2
>>> model.input_constraints
[(one_hot_0: q_0 + q_1 + q_2 == 1.000000, 2), (one_hot_1: q_3 + q_4 + q_5 == 1.000000, 2), (one_hot_2: q_6 + q_7 + q_8 == 1.000000, 2), (less_equal: q_0 + q_3 <= 1, 1), (greater_equal: q_5 + q_8 >= 1, 1)]

one-hot 制約のみ重み係数が 2 倍されていることが確認できます。

解の重複排除

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

注釈

通常は重複排除機能をオフに設定する必要はありません。

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

from amplify import BinaryPoly, gen_symbols, Solver, decode_solution
from amplify.constraint import equal_to
from amplify.client import FixstarsClient

q = gen_symbols(BinaryPoly, 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 = {decode_solution(q, 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 = {decode_solution(q, 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回の実行で複数の解を出力する場合に適用されます。これはデフォルトで有効です。無効にした場合、複数の解の格納順はマシンの出力順に依存します。

from amplify import Solver
from amplify.client import FixstarsClient

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

ソルバークラスの内部

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

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

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

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

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

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

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

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

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

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

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

from amplify import BinaryPoly, gen_symbols, Solver
from amplify.constraint import equal_to
from amplify.client.ocean import DWaveSamplerClient

q = gen_symbols(BinaryPoly, 8)
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 = DWaveSamplerClient()
client.solver = "DW_2000Q_VFYC_6"
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

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