# NAE-SAT (全不等充足可能性問題)
:::{container} prog-cpp
**全不等充足可能性問題 (NAE-SAT: Not-All-Equal Satisfiability)** はブール充足可能性問題 (SAT) の変種です.
ブール変数 $x_0, x_1, \ldots, x_{n-1}$ と節の集合が与えられたとき,各節は少なくとも1つの変数が True であり,**かつ**少なくとも1つが False である場合にのみ**充足**されます.
つまり,節内のすべての変数が同じ値（すべて True またはすべて False）のとき,その節は違反となります.
例えば,ブール変数 $x_0, x_1, x_2, x_3$ に対して,以下の節を考えます：
$$
\begin{aligned}
C_0 &= \lbrace x_0,x_1,x_2 \rbrace,\\
C_1 &= \lbrace x_1,x_2,x_3 \rbrace,\\
C_2 &= \lbrace x_1,x_3 \rbrace
\end{aligned}
$$
割り当て $(x_0, x_1, x_2, x_3) = (\text{True}, \text{True}, \text{False}, \text{False})$ は解です.各節に少なくとも1つの True と少なくとも1つの False の変数が含まれています.
NAE-SAT は NP 完全であり,ハイパーグラフ彩色や制約充足問題などの応用があります.
## HUBO による定式化
$n$ 個のバイナリ変数 $x_0, x_1, \ldots, x_{n-1}$ と $m$ 個の節 $C_0, C_1, \ldots, C_{m-1}$ に対して,NAE-SAT 制約は HUBO（高次制約なしバイナリ最適化）式として定式化できます.
### NAE 制約
各節 $C_k = \lbrace x_{i_1}, x_{i_2}, \ldots, x_{i_s} \rbrace$ に対して以下を定義します：
- **全 True ペナルティ**: 積 $$x_{i_1} \cdot x_{i_2} \cdots x_{i_s}$$ は節内のすべての変数が True のときにのみ 1 になります.
- **全 False ペナルティ**: 積 $$\overline{x}_{i_1} \cdot \overline{x}_{i_2} \cdots \overline{x}_{i_s}$$ はすべての変数が False のときにのみ 1 になります.ここで $$\overline{x}_i$$ は否定リテラル（$$\overline{x}_i = 1 - x_i$$）を表します.
インスタンス全体の制約は以下の通りです：
$$
\text{constraint} = \sum_{k=0}^{m-1} \Bigl( \prod_{j \in C_k} x_j + \prod_{j \in C_k} \overline{x}_j \Bigr)
$$
この式はすべての節が NAE 充足されている場合にのみ 0 になります.
### 目的関数（オプション）
副次的な目的として,True と False の変数数のバランスを取ることができます：
$$
\text{objective} = \Bigl(2\sum_{i=0}^{n-1} x_i - n\Bigr)^2
$$
これは True/False の数がなるべく均等なとき最小化されます（$n$ が偶数のとき 0,$n$ が奇数のとき 1）.
### HUBO 式
最終的な HUBO 式は,制約と目的関数をペナルティ重み $P$ で組み合わせます：
$$
f = \text{objective} + P \times \text{constraint}
$$
ここで $P$ は十分大きく（例えば $P = n^2 + 1$）,制約の充足が目的関数の最小化よりも優先されるようにします.
## Hi-QUBO による定式化
Hi-QUBO は否定リテラル $$\overline{x}_i$$（`~x[i]` と記述）をネイティブに扱えるため,NAE-SAT の定式化が自然かつ効率的に行えます.
以下のプログラムは,5 変数・4 節（各節サイズ 3）の簡単な NAE-SAT インスタンスを定義し,EasySolver で解き,結果を検証します.
```{literalinclude} /../programFiles/cppPrograms/example/math/naesat-program1.cpp
:language: cpp
:caption: naesat-program1.cpp
```
### 実行結果の例
```{include} /../programFiles/markDown/example/math/naesat.md
:start-after:
:end-before:
```
ソルバーは `constraint = 0` となる割り当てを見つけ,4 つの節すべてが NAE 充足されています.
目的関数の値は 1 です.これは $n = 5$ が奇数であるため,最良の True/False バランス（例えば True が 3,False が 2）で $(2 \times 3 - 5)^2 = 1$ となるためです.
### 要点
- **否定リテラル**: Hi-QUBO では `~x[i]` を直接使用して $$\overline{x}_i$$ を表現でき,$$1 - x_i$$ に展開する必要がありません.これにより HUBO 式がコンパクトに保たれます.
- **高次項**: サイズ $s$ の節は次数 $s$ の項を生成します（例えば,3 リテラルの節では $x_0 x_1 x_2$）.Hi-QUBO は HUBO 式をネイティブに扱えるため,二次化（quadratization）は不要です.
- **ペナルティ重み**: $P = n^2 + 1$ により,制約違反が目的関数の最大値を必ず上回るようにします.
:::
:::{container} prog-python
**全不等充足可能性問題 (NAE-SAT: Not-All-Equal Satisfiability)** はブール充足可能性問題 (SAT) の変種です.
ブール変数 $x_0, x_1, \ldots, x_{n-1}$ と節の集合が与えられたとき,各節は少なくとも1つの変数が True であり,**かつ**少なくとも1つが False である場合にのみ**充足**されます.
つまり,節内のすべての変数が同じ値（すべて True またはすべて False）のとき,その節は違反となります.
例えば,ブール変数 $x_0, x_1, x_2, x_3$ に対して,以下の節を考えます：
$$
\begin{aligned}
C_0 &= \lbrace x_0,x_1,x_2 \rbrace,\\
C_1 &= \lbrace x_1,x_2,x_3 \rbrace,\\
C_2 &= \lbrace x_1,x_3 \rbrace
\end{aligned}
$$
割り当て $(x_0, x_1, x_2, x_3) = (\text{True}, \text{True}, \text{False}, \text{False})$ は解です.各節に少なくとも1つの True と少なくとも1つの False の変数が含まれています.
NAE-SAT は NP 完全であり,ハイパーグラフ彩色や制約充足問題などの応用があります.
## HUBO による定式化
$n$ 個のバイナリ変数 $x_0, x_1, \ldots, x_{n-1}$ と $m$ 個の節 $C_0, C_1, \ldots, C_{m-1}$ に対して,NAE-SAT 制約は HUBO（高次制約なしバイナリ最適化）式として定式化できます.
### NAE 制約
各節 $C_k = \lbrace x_{i_1}, x_{i_2}, \ldots, x_{i_s} \rbrace$ に対して以下を定義します：
- **全 True ペナルティ**: 積 $$x_{i_1} \cdot x_{i_2} \cdots x_{i_s}$$ は節内のすべての変数が True のときにのみ 1 になります.
- **全 False ペナルティ**: 積 $$\overline{x}_{i_1} \cdot \overline{x}_{i_2} \cdots \overline{x}_{i_s}$$ はすべての変数が False のときにのみ 1 になります.ここで $$\overline{x}_i$$ は否定リテラル（$$\overline{x}_i = 1 - x_i$$）を表します.
インスタンス全体の制約は以下の通りです：
$$
\text{constraint} = \sum_{k=0}^{m-1} \Bigl( \prod_{j \in C_k} x_j + \prod_{j \in C_k} \overline{x}_j \Bigr)
$$
この式はすべての節が NAE 充足されている場合にのみ 0 になります.
### 目的関数（オプション）
副次的な目的として,True と False の変数数のバランスを取ることができます：
$$
\text{objective} = \Bigl(2\sum_{i=0}^{n-1} x_i - n\Bigr)^2
$$
これは True/False の数がなるべく均等なとき最小化されます（$n$ が偶数のとき 0,$n$ が奇数のとき 1）.
### HUBO 式
最終的な HUBO 式は,制約と目的関数をペナルティ重み $P$ で組み合わせます：
$$
f = \text{objective} + P \times \text{constraint}
$$
ここで $P$ は十分大きく（例えば $P = n^2 + 1$）,制約の充足が目的関数の最小化よりも優先されるようにします.
## PyQBPP による定式化
PyQBPP は否定リテラル $$\overline{x}_i$$（`~x[i]` と記述）をネイティブに扱えるため,NAE-SAT の定式化が自然かつ効率的に行えます.
以下のプログラムは,5 変数・4 節（各節サイズ 3）の簡単な NAE-SAT インスタンスを定義し,EasySolver で解き,結果を検証します.
```{literalinclude} /../programFiles/pythonPrograms/example/math/naesat-program1.py
:language: python
:caption: naesat-program1.py
```
### 実行結果の例
```{include} /../programFiles/markDown/example/math/naesat.md
:start-after:
:end-before:
```
ソルバーは `constraint = 0` となる割り当てを見つけ,4 つの節すべてが NAE 充足されています.
目的関数の値は 1 です.これは $n = 5$ が奇数であるため,最良の True/False バランス（例えば True が 3,False が 2）で $(2 \times 3 - 5)^2 = 1$ となるためです.
### 要点
- **否定リテラル**: PyQBPP では `~x[i]` を直接使用して $$\overline{x}_i$$ を表現でき,$$1 - x_i$$ に展開する必要がありません.これにより HUBO 式がコンパクトに保たれます.
- **高次項**: サイズ $s$ の節は次数 $s$ の項を生成します（例えば,3 リテラルの節では $x_0 x_1 x_2$）.PyQBPP は HUBO 式をネイティブに扱えるため,二次化（quadratization）は不要です.
- **ペナルティ重み**: $P = n^2 + 1$ により,制約違反が目的関数の最大値を必ず上回るようにします.
:::