NAE-SAT (全不等充足可能性問題)¶

全不等充足可能性問題 (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{split} \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} \end{split}\]

割り当て $(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 で解き,結果を検証します.

naesat-program1.cpp¶

#include <qbpp/qbpp.hpp>
#include <qbpp/easy_solver.hpp>

int main() {
  const int n = 5;

  // 節: 各節は変数インデックスの集合
  std::vector<std::vector<int>> clauses = {
      {0, 1, 2},
      {1, 2, 3},
      {2, 3, 4},
      {0, 3, 4}
  };

  // バイナリ変数の作成
  auto x = qbpp::var("x", n);

  // NAE 制約: 全 True または全 False のときペナルティ
  auto constraint = qbpp::toExpr(0);
  for (const auto& clause : clauses) {
    auto all_true = qbpp::toExpr(1);
    auto all_false = qbpp::toExpr(1);
    for (int idx : clause) {
      all_true *= x[idx];
      all_false *= ~x[idx];
    }
    constraint += all_true + all_false;
  }

  // 目的関数: True/False の数のバランス
  auto s = qbpp::sum(x);
  auto objective = (2 * s - n) * (2 * s - n);

  // ペナルティ重み付き HUBO 式
  int penalty_weight = n * n + 1;
  auto f = (objective + penalty_weight * constraint).simplify_as_binary();

  // 求解
  auto solver = qbpp::EasySolver(f);
  // n=5 は奇数なので最良バランスで (2*s-n)^2 = 1
  auto sol = solver.search({{"target_energy", 1}});

  // 結果の出力
  std::cout << "Energy = " << sol.energy() << std::endl;
  std::cout << "Assignment: ";
  for (int i = 0; i < n; ++i) {
    std::cout << "x[" << i << "]=" << sol(x[i]) << " ";
  }
  std::cout << std::endl;

  std::cout << "constraint = " << sol(constraint) << std::endl;
  std::cout << "objective  = " << sol(objective) << std::endl;

  // 検証: 各節のチェック
  bool all_satisfied = true;
  for (size_t k = 0; k < clauses.size(); ++k) {
    int sum_val = 0;
    for (int idx : clauses[k]) {
      sum_val += sol(x[idx]);
    }
    bool satisfied = (sum_val > 0) &&
                     (sum_val < static_cast<int>(clauses[k].size()));
    std::cout << "Clause " << k << ": "
              << (satisfied ? "satisfied" : "VIOLATED") << std::endl;
    if (!satisfied) all_satisfied = false;
  }
  std::cout << "All clauses NAE-satisfied: "
            << (all_satisfied ? "Yes" : "No") << std::endl;
}

実行結果の例

Energy = 1
Assignment: x[0]=1 x[1]=0 x[2]=1 x[3]=0 x[4]=1
constraint = 0
objective  = 1
Clause 0: satisfied
Clause 1: satisfied
Clause 2: satisfied
Clause 3: satisfied
All clauses NAE-satisfied: Yes

ソルバーは 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$ により,制約違反が目的関数の最大値を必ず上回るようにします.