Logical Expression

このセクションでは論理式クラスとその周辺関数について説明します。

論理式の構築

論理式クラス LogicPoly は論理式を表現します。イジングマシンへの入力を前提としているため、内部表現としてバイナリ多変数多項式を持ち、多項式オブジェクトへの変換が可能です。

論理式オブジェクトは、次のようにブール変数のインデックスを与えて構築されます。

from amplify import LogicPoly

x0 = LogicPoly(0)

>>> x0
x_0

ブール値を与えて構築することも出来ます。

t = LogicPoly(True)
f = LogicPoly(False)

>>> t
1
>>> f
0

このように、論理式オブジェクトは True の場合に 1 を、False の場合に 0 で表示されます。これは内部表現がバイナリ多変数多項式であることに由来します。そのため文字列として表示した場合には、バイナリ変数による多変数多項式 BinaryPoly を同様の形式で表されます。

Note

LogicPoly の内部表現はバイナリ多変数多項式 BinaryPoly ですが、取り得る値は必ず 1 (True) か 0 (False) になるように制限されています。ユーザは直接この多項式オブジェクトを操作することは出来ません。

コンストラクタ引数に同じ論理式オブジェクトを与えるとコピーされます。

from amplify import LogicPoly

x0 = LogicPoly(0)
x_copy = LogicPoly(x0)

>>> x0
x_0
>>> x_copy
x_0

論理式の演算子

多項式クラスには、多項式オブジェクト同士やブール変数との間に、等価・論理和・論理積・排他的論理和・論理否定とその複合代入演算子が定義されます。

>>> LogicPoly(0) | LogicPoly(1)
- x_0 x_1 + x_0 + x_1

>>> LogicPoly(0) & LogicPoly(1)
x_0 x_1

>>> LogicPoly(0) ^ LogicPoly(1)
- 2 x_0 x_1 + x_0 + x_1

>>> ~(LogicPoly(0) & LogicPoly(1))
- x_0 x_1 + 1

>>> ~(LogicPoly(0) | LogicPoly(1)) == ~LogicPoly(0) & ~LogicPoly(1)
True

変数配列を用いた構築と評価

多項式クラスと同様に、gen_symbols() 関数と decode_solution() 関数を用いてブール変数配列を生成と解の評価ができます。詳細は多項式クラスの 変数配列を用いた構築、 変数配列への値の代入 変数配列を用いた解の取得 を参照してください。

from amplify import LogicPoly, gen_symbols

x = gen_symbols(LogicPoly, 10)

>>> x
[x_0, x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9]

定式化補助関数

多項式クラスにおける sum_poly() 関数等と同様に、論理式に対する定式化補助関数として、

• 全ての論理積 \(\land_i\) に相当する intersection() 関数

• 全ての論理和 \(\lor_i\) に相当する union() 関数

• 全ての排他的論理和 \(\oplus_i\) に相当する symmetric_difference() 関数

が提供されています。

これらの関数には下記の3つの機能があります。

リストに対する演算

リスト x に対して次の演算を行います。

\[ \begin{align}\begin{aligned}l &= \bigwedge_{i = 0}^{n - 1} x_\left[ i \right]\\l &= \bigvee_{i = 0}^{n - 1} x_\left[ i \right]\\l &= \bigoplus_{i = 0}^{n - 1} x_\left[ i \right]\end{aligned}\end{align} \]

from amplify import LogicPoly, gen_symbols, intersection, union, symmetric_difference

x = gen_symbols(LogicPoly, 3)

>>> intersection(x)
x_0 x_1 x_2

>>> union(x)
x_0 x_1 x_2 - x_0 x_1 - x_0 x_2 - x_1 x_2 + x_0 + x_1 + x_2

>>> symmetric_difference(x)
4 x_0 x_1 x_2 - 2 x_0 x_1 - 2 x_0 x_2 - 2 x_1 x_2 + x_0 + x_1 + x_2

インデックスに対する演算

変数 x_i に対して次の演算を行います。

\[ \begin{align}\begin{aligned}l &= \bigwedge_{i = 0}^{n - 1} x_i\\l &= \bigvee_{i = 0}^{n - 1} x_i\\l &= \bigoplus_{i = 0}^{n - 1} x_i\end{aligned}\end{align} \]

第一引数から第三引数には組み込みクラス range と同一の引数を与えるか、第一引数に列挙型を与えることも可能です。

>>> intersection(3)
x_0 x_1 x_2
>>> intersection(1, 4)
x_1 x_2 x_3
>>> intersection(1, 6, 2)
x_1 x_3 x_5
>>> intersection(range(2, 7, 2))
x_2 x_4 x_6

>>> union(3)
x_0 x_1 x_2 - x_0 x_1 - x_0 x_2 - x_1 x_2 + x_0 + x_1 + x_2
>>> union(1, 4)
x_1 x_2 x_3 - x_1 x_2 - x_1 x_3 - x_2 x_3 + x_1 + x_2 + x_3
>>> union(1, 6, 2)
x_1 x_3 x_5 - x_1 x_3 - x_1 x_5 - x_3 x_5 + x_1 + x_3 + x_5
>>> union(range(2, 7, 2))
x_2 x_4 x_6 - x_2 x_4 - x_2 x_6 - x_4 x_6 + x_2 + x_4 + x_6

>>> symmetric_difference(3)
4 x_0 x_1 x_2 - 2 x_0 x_1 - 2 x_0 x_2 - 2 x_1 x_2 + x_0 + x_1 + x_2
>>> symmetric_difference(1, 4)
4 x_1 x_2 x_3 - 2 x_1 x_2 - 2 x_1 x_3 - 2 x_2 x_3 + x_1 + x_2 + x_3
>>> symmetric_difference(1, 6, 2)
4 x_1 x_3 x_5 - 2 x_1 x_3 - 2 x_1 x_5 - 2 x_3 x_5 + x_1 + x_3 + x_5
>>> symmetric_difference(range(2, 7, 2))
4 x_2 x_4 x_6 - 2 x_2 x_4 - 2 x_2 x_6 - 2 x_4 x_6 + x_2 + x_4 + x_6

Note

多項式クラスと同様に最終引数に論理式クラスを与えても良いですが、省略できます。

関数に対する演算

関数 g(i) に対して次の演算を行います。

\[ \begin{align}\begin{aligned}l &= \bigwedge_{i = 0}^{n - 1} g\left( i \right)\\l &= \bigvee_{i = 0}^{n - 1} g\left( i \right)\\l &= \bigoplus_{i = 0}^{n - 1} g\left( i \right)\end{aligned}\end{align} \]

式に対する演算

\[l = \bigwedge_{i = 0}^{n - 1} \lnot x_{2 i}\]

from amplify import LogicPoly, intersection

>>> intersection(3, lambda i: ~LogicPoly(2 * i))
- x_0 x_2 x_4 + x_0 x_2 + x_0 x_4 + x_2 x_4 - x_0 - x_2 - x_4 + 1

ネストした演算

k-SAT

\[l = \bigwedge_{i} \bigvee_{j \in C_i} l_j\]

from amplify import LogicPoly, intersection, union

x = gen_symbols(LogicPoly, 5)
l = intersection(3, lambda i: union(3, lambda j: x[i + j] if j == 1 else ~x[i + j]))

>>> l
x_0 x_1 x_2 x_3 x_4 - x_0 x_1 x_2 x_4 - x_0 x_2 x_3 x_4 + x_0 x_1 x_2 + x_0 x_2 x_4 + x_1 x_2 x_3 + x_2 x_3 x_4 - x_0 x_2 - x_1 x_3 - x_2 x_4 + 1

論理式クラスのメソッド

ほとんどのメソッドについて、多項式クラスと同様のインタフェースを持ちます。多項式クラスのメソッド を参照してください。

変数変換

change_variables()

項の数

count()

ブール値への変換可能性

論理式オブジェクトがブール値のみで構成されているかを返します。これが True の場合、ブール値への暗黙変換が可能です。

from amplify import LogicPoly

p = LogicPoly(0) | ~LogicPoly(0)

>>> p.is_bool()
True
>>> "TRUE" if p else "FALSE"
TRUE

インデックスの最大値

max_index()

多項式への値の代入

replace()

多項式の値の評価

replace_all()

バイナリ多項式への変換

論理式からバイナリ多項式へ変換します。

from amplify import LogicPoly

p = LogicPoly(0) | LogicPoly(1)
f = (~p).to_Poly()

>>> p
- x_0 x_1 + x_0 + x_1
>>> f
q_0 q_1 - q_0 - q_1 + 1

Note

論理式クラスでは True を 1 とし False を 0 とします。バイナリ多項式を最適化(最小化)問題として扱う場合には大小関係が逆になっているため、 NOT 演算を行った上で to_Poly() 関数を呼び出すと整合します。