充足可能性問題 (SAT)¶

充足可能性問題 (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 インスタンスを解きます：

sat-program1.cpp¶

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

int main() {
  // 5つのブール変数
  auto x = qbpp::var("x", 5);

  // 規約: True=0, False=1
  // 正リテラル x_i: x_i=1 のとき偽 -> x[i] を使用
  // 負リテラル ~x_j: x_j=0 のとき偽 -> ~x[j] を使用
  // 積 = 1 は節のすべてのリテラルが偽のとき（違反）

  // 節 0: (x0 OR x1 OR x2)
  //   x0=偽 AND x1=偽 AND x2=偽 のとき違反
  //   ペナルティ = x[0] * x[1] * x[2]
  auto c0 = x[0] * x[1] * x[2];

  // 節 1: (~x0 OR x3 OR x4)
  //   x0=真 AND x3=偽 AND x4=偽 のとき違反
  //   ペナルティ = ~x[0] * x[3] * x[4]
  auto c1 = ~x[0] * x[3] * x[4];

  // 節 2: (x1 OR ~x2 OR ~x3)
  //   x1=偽 AND x2=真 AND x3=真 のとき違反
  //   ペナルティ = x[1] * ~x[2] * ~x[3]
  auto c2 = x[1] * ~x[2] * ~x[3];

  // 節 3: (~x1 OR ~x3 OR x4)
  //   x1=真 AND x3=真 AND x4=偽 のとき違反
  //   ペナルティ = ~x[1] * ~x[3] * x[4]
  auto c3 = ~x[1] * ~x[3] * x[4];

  // 節 4: (~x0 OR ~x1 OR ~x2)
  //   x0=真 AND x1=真 AND x2=真 のとき違反
  //   ペナルティ = ~x[0] * ~x[1] * ~x[2]
  auto c4 = ~x[0] * ~x[1] * ~x[2];

  // 節 5: (x0 OR x1 OR ~x4)
  //   x0=偽 AND x1=偽 AND x4=真 のとき違反
  //   ペナルティ = x[0] * x[1] * ~x[4]
  auto c5 = x[0] * x[1] * ~x[4];

  // 制約の合計: 節ペナルティの和
  auto constraint = c0 + c1 + c2 + c3 + c4 + c5;

  constraint.simplify_as_binary();
  auto solver = qbpp::EasySolver(constraint);
  auto sol = solver.search({{"target_energy", 0}});

  // 結果の出力
  std::cout << "Energy = " << sol.energy() << std::endl;
  std::cout << "Assignment (True=0, False=1):" << std::endl;
  for (size_t i = 0; i < 5; ++i) {
    std::cout << "  x[" << i << "] = " << sol(x[i])
              << " (" << (sol(x[i]) == 0 ? "True" : "False") << ")"
              << std::endl;
  }

  // 各節の検証
  std::cout << "Clause penalties:" << std::endl;
  std::cout << "  c0 = " << sol(c0) << std::endl;
  std::cout << "  c1 = " << sol(c1) << std::endl;
  std::cout << "  c2 = " << sol(c2) << std::endl;
  std::cout << "  c3 = " << sol(c3) << std::endl;
  std::cout << "  c4 = " << sol(c4) << std::endl;
  std::cout << "  c5 = " << sol(c5) << std::endl;
  std::cout << "Violated clauses = " << sol(constraint) << std::endl;
}

このプログラムでは,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 を用いて解きます.

出力結果

Energy = 0
Assignment (True=0, False=1):
  x[0] = 0 (True)
  x[1] = 1 (False)
  x[2] = 0 (True)
  x[3] = 1 (False)
  x[4] = 0 (True)
Clause penalties:
  c0 = 0
  c1 = 0
  c2 = 0
  c3 = 0
  c4 = 0
  c5 = 0
Violated clauses = 0

ソルバーはエネルギー 0 の充足割り当てを見つけます.これはすべての節が充足されていることを意味します. ソルバーは確率的であるため,実際の割り当ては実行ごとに異なる場合があります.

例えば,以下は 5 変数 $x_0,x_1,x_2,x_3,x_4$,6 節の 3-SAT インスタンスです：

充足する割り当てはすべての節を真にする,つまり各節で少なくとも 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 における否定リテラル）です.

\[ p_k = \prod_{\ell \in C_k} f(\ell) \]

制約式の合計は以下の通りです：

\[ \text{constraint} = \sum_{k} p_k \]

PyQBPP による定式化

以下の PyQBPP プログラムは,上記の 3-SAT インスタンスを解きます：

sat-program1.py¶

import pyqbpp as qbpp

# 5つのブール変数
x = qbpp.var("x", shape=5)

# 規約: True=0, False=1
# 正リテラル x_i: x_i=1 のとき偽 -> x[i] を使用
# 負リテラル ~x_j: x_j=0 のとき偽 -> ~x[j] を使用
# 積 = 1 は節のすべてのリテラルが偽のとき（違反）

# 節 0: (x0 OR x1 OR x2)
#   x0=偽 AND x1=偽 AND x2=偽 のとき違反
#   ペナルティ = x[0] * x[1] * x[2]
c0 = x[0] * x[1] * x[2]

# 節 1: (~x0 OR x3 OR x4)
#   x0=真 AND x3=偽 AND x4=偽 のとき違反
#   ペナルティ = ~x[0] * x[3] * x[4]
c1 = ~x[0] * x[3] * x[4]

# 節 2: (x1 OR ~x2 OR ~x3)
#   x1=偽 AND x2=真 AND x3=真 のとき違反
#   ペナルティ = x[1] * ~x[2] * ~x[3]
c2 = x[1] * ~x[2] * ~x[3]

# 節 3: (~x1 OR ~x3 OR x4)
#   x1=真 AND x3=真 AND x4=偽 のとき違反
#   ペナルティ = ~x[1] * ~x[3] * x[4]
c3 = ~x[1] * ~x[3] * x[4]

# 節 4: (~x0 OR ~x1 OR ~x2)
#   x0=真 AND x1=真 AND x2=真 のとき違反
#   ペナルティ = ~x[0] * ~x[1] * ~x[2]
c4 = ~x[0] * ~x[1] * ~x[2]

# 節 5: (x0 OR x1 OR ~x4)
#   x0=偽 AND x1=偽 AND x4=真 のとき違反
#   ペナルティ = x[0] * x[1] * ~x[4]
c5 = x[0] * x[1] * ~x[4]

# 制約の合計: 節ペナルティの和
constraint = c0 + c1 + c2 + c3 + c4 + c5

constraint.simplify_as_binary()
solver = qbpp.EasySolver(constraint)
sol = solver.search(target_energy=0)

# 結果の出力
print(f"Energy = {sol.energy}")
print("Assignment (True=0, False=1):")
for i in range(5):
    val = sol(x[i])
    print(f"  x[{i}] = {val} ({'True' if val == 0 else 'False'})")

# 各節の検証
print("Clause penalties:")
for i, c in enumerate([c0, c1, c2, c3, c4, c5]):
    print(f"  c{i} = {sol(c)}")
print(f"Violated clauses = {sol(constraint)}")

このプログラムでは,5 つのバイナリ変数を定義し,各節のペナルティ式を構築します. 正リテラル $x_i$ には x[i] を使用し,これはリテラルが偽のとき 1 になります. 負リテラル $\lnot x_i$ には ~x[i] を使用し,これはリテラルが偽のとき（すなわち $x_i$ が真,つまり $x_i = 0$ のとき）1 になります. PyQBPP は否定リテラル ~x[i] をネイティブにサポートするため,1 - x[i] に手動で置き換える必要はありません.

simplify_as_binary() を呼び出して冪等律 $x_i^2 = x_i$ を適用し式を簡約化した後,目標エネルギー 0 で EasySolver を用いて解きます.

出力結果

Energy = 0
Assignment (True=0, False=1):
  x[0] = 0 (True)
  x[1] = 1 (False)
  x[2] = 0 (True)
  x[3] = 1 (False)
  x[4] = 0 (True)
Clause penalties:
  c0 = 0
  c1 = 0
  c2 = 0
  c3 = 0
  c4 = 0
  c5 = 0
Violated clauses = 0