# 充足可能性問題 (SAT)
:::{container} prog-cpp
**充足可能性問題 (SAT)** は,**連言標準形 (CNF)** で与えられたブール式を真にするような変数への真偽値の割り当てが存在するかを判定する問題です.
CNF 式は**節** (clause) の連言 (AND) であり,各節は**リテラル**の選言 (OR) です.
リテラルは変数 $x_i$（正リテラル）またはその否定 $\lnot x_i$（負リテラル）です.
例えば,以下は 5 変数 $x_0,x_1,x_2,x_3,x_4$,6 節の 3-SAT インスタンスです：
$$
(x_0 \lor x_1 \lor x_2) \land (\lnot x_0 \lor x_3 \lor x_4) \land (x_1 \lor \lnot x_2 \lor \lnot x_3) \land (\lnot x_1 \lor \lnot x_3 \lor x_4) \land (\lnot x_0 \lor \lnot x_1 \lor \lnot x_2) \land (x_0 \lor x_1 \lor \lnot x_4)
$$
充足する割り当てはすべての節を真にする,つまり各節で少なくとも 1 つのリテラルが真でなければなりません.
## HUBO 定式化
バイナリ変数の規約として **True = 0**,**False = 1** を用います.
この規約の下で：
- 正リテラル $x_i$ は $x_i = 1$ のとき**偽 (False)** です.
- 負リテラル $$\lnot x_i$$ は $$x_i = 0$$ のとき**偽 (False)** です.すなわち $$\tilde{x}_i = 1$$ のとき（$$\tilde{x}_i$$ は Hi-QUBO における否定リテラル）です.
節が違反される（すべてのリテラルが偽）のは,各リテラルの「偽指標」の積が 1 に等しいときです.
節 $C_k$ に対して,ペナルティを以下のように定義します：
$$
p_k = \prod_{\ell \in C_k} f(\ell)
$$
ここで,$\ell$ が正リテラル $x_i$ の場合 $f(\ell) = x_i$,$\ell$ が負リテラル $\lnot x_i$ の場合 $f(\ell) = \tilde{x}_i$ です.
この積は節が違反されたときのみ 1 になります.
制約式の合計は以下の通りです：
$$
\text{constraint} = \sum_{k} p_k
$$
この式はすべての節が充足されたときのみ最小値 0 を達成します.
制約は自然に **HUBO**（高次無制約バイナリ最適化）式となります.$m$ リテラルの節は次数 $m$ の項を生成するためです.
## Hi-QUBO による定式化
以下の Hi-QUBO プログラムは,上記の 3-SAT インスタンスを解きます：
```{literalinclude} /../programFiles/cppPrograms/example/math/sat-program1.cpp
:language: cpp
:caption: sat-program1.cpp
```
このプログラムでは,5 つのバイナリ変数を定義し,各節のペナルティ式を構築します.
正リテラル $x_i$ には `x[i]` を使用し,これはリテラルが偽のとき 1 になります.
負リテラル $\lnot x_i$ には `~x[i]` を使用し,これはリテラルが偽のとき（すなわち $x_i$ が真,つまり $x_i = 0$ のとき）1 になります.
Hi-QUBO は否定リテラル `~x[i]` をネイティブにサポートするため,`1 - x[i]` に手動で置き換える必要はありません.
節内のこれらの項の積は,節のすべてのリテラルが偽のとき,つまり節が違反されたときのみ 1 になります.
制約の合計はすべての節ペナルティの和であり,すべての節が充足されたときのみ 0 を達成します.
`simplify_as_binary()` を呼び出して冪等律 $x_i^2 = x_i$ を適用し式を簡約化した後,目標エネルギー 0 で EasySolver を用いて解きます.
### 出力結果
```{include} /../programFiles/markDown/example/math/sat.md
:start-after:
:end-before:
```
ソルバーはエネルギー 0 の充足割り当てを見つけます.これはすべての節が充足されていることを意味します.
ソルバーは確率的であるため,実際の割り当ては実行ごとに異なる場合があります.
:::
:::{container} prog-python
**充足可能性問題 (SAT)** は,**連言標準形 (CNF)** で与えられたブール式を真にするような変数への真偽値の割り当てが存在するかを判定する問題です.
CNF 式は**節** (clause) の連言 (AND) であり,各節は**リテラル**の選言 (OR) です.
リテラルは変数 $x_i$（正リテラル）またはその否定 $\lnot x_i$（負リテラル）です.
例えば,以下は 5 変数 $x_0,x_1,x_2,x_3,x_4$,6 節の 3-SAT インスタンスです：
$$
(x_0 \lor x_1 \lor x_2) \land (\lnot x_0 \lor x_3 \lor x_4) \land (x_1 \lor \lnot x_2 \lor \lnot x_3) \land (\lnot x_1 \lor \lnot x_3 \lor x_4) \land (\lnot x_0 \lor \lnot x_1 \lor \lnot x_2) \land (x_0 \lor x_1 \lor \lnot x_4)
$$
充足する割り当てはすべての節を真にする,つまり各節で少なくとも 1 つのリテラルが真でなければなりません.
## HUBO 定式化
バイナリ変数の規約として **True = 0**,**False = 1** を用います.
この規約の下で：
- 正リテラル $x_i$ は $x_i = 1$ のとき**偽 (False)** です.
- 負リテラル $\lnot x_i$ は $x_i = 0$ のとき**偽 (False)** です.すなわち $\tilde{x}_i = 1$ のとき（$\tilde{x}_i$ は PyQBPP における否定リテラル）です.
節が違反される（すべてのリテラルが偽）のは,各リテラルの「偽指標」の積が 1 に等しいときです.
節 $C_k$ に対して,ペナルティを以下のように定義します：
$$
p_k = \prod_{\ell \in C_k} f(\ell)
$$
ここで,$\ell$ が正リテラル $x_i$ の場合 $f(\ell) = x_i$,$\ell$ が負リテラル $\lnot x_i$ の場合 $f(\ell) = \tilde{x}_i$ です.
この積は節が違反されたときのみ 1 になります.
制約式の合計は以下の通りです：
$$
\text{constraint} = \sum_{k} p_k
$$
この式はすべての節が充足されたときのみ最小値 0 を達成します.
制約は自然に **HUBO**（高次無制約バイナリ最適化）式となります.$m$ リテラルの節は次数 $m$ の項を生成するためです.
## PyQBPP による定式化
以下の PyQBPP プログラムは,上記の 3-SAT インスタンスを解きます：
```{literalinclude} /../programFiles/pythonPrograms/example/math/sat-program1.py
:language: python
:caption: sat-program1.py
```
このプログラムでは,5 つのバイナリ変数を定義し,各節のペナルティ式を構築します.
正リテラル $x_i$ には `x[i]` を使用し,これはリテラルが偽のとき 1 になります.
負リテラル $\lnot x_i$ には `~x[i]` を使用し,これはリテラルが偽のとき（すなわち $x_i$ が真,つまり $x_i = 0$ のとき）1 になります.
PyQBPP は否定リテラル `~x[i]` をネイティブにサポートするため,`1 - x[i]` に手動で置き換える必要はありません.
節内のこれらの項の積は,節のすべてのリテラルが偽のとき,つまり節が違反されたときのみ 1 になります.
制約の合計はすべての節ペナルティの和であり,すべての節が充足されたときのみ 0 を達成します.
`simplify_as_binary()` を呼び出して冪等律 $x_i^2 = x_i$ を適用し式を簡約化した後,目標エネルギー 0 で EasySolver を用いて解きます.
### 出力結果
```{include} /../programFiles/markDown/example/math/sat.md
:start-after:
:end-before:
```
ソルバーはエネルギー 0 の充足割り当てを見つけます.これはすべての節が充足されていることを意味します.
ソルバーは確率的であるため,実際の割り当ては実行ごとに異なる場合があります.
:::