技術的概要：イジング/QUBO エンコーディングによる短 SAT 含意項の計算

1. 問題定義

説明、診断、モデル圧縮を含む多くの推論タスクでは、完全な割り当てではなく、短い部分充足割り当て（含意項）を必要とする。これらの文脈において、未割当変数は真の「無関係（don't-care）」として機能し、多くの場合、変数の一部（可視変数）のみが意味的に重要であり、他の変数は隠れたサポートとして機能する。

現代の SAT ソルバーは完全な充足割り当てを効率的に計算するが、短い含意項を導出するには、通常、繰り返し SAT 呼び出しまたは専用の後処理が必要となる。同様に、標準的なSAT からイジング/QUBO への定式化は本質的に制限されている：これらは CNF 式を、基底状態が完全な割り当てに対応する二次エネルギー関数にマッピングする。イジング/QUBO モデルはすべてのスピンに値を割り当てるため、「未割当」変数のネイティブな表現を持たない。その結果、短い含意項の計算は、二次最適化モデル自体に組み込まれるのではなく、歴史的に外部アルゴリズムに委ねられてきた。

2. 手法

著者らは、二次イジング/QUBO モデル内でネイティブに 3 値部分割り当て（真、偽、未割当）をサポートする統合最適化フレームワークを提案する。

2.1 二重極性表現

未割当変数を表現するために、このフレームワークは二重極性エンコーディングを導入する。各命題変数 $A_i$ に対して、2 つの二値スピン $(p_i, n_i)$ が使用される：

• $(1, 0) \implies A_i = \top$
• $(0, 1) \implies A_i = \bot$
• $(0, 0) \implies A_i$ は未割当（無関係）
• $(1, 1) \implies$ 矛盾（禁止）

矛盾状態を禁止するため、意味的整合性ペナルティ $M \cdot p_i n_i$ が追加される。

2.2 節のエンコーディング

節は標準的な二次ペナルティ関数を用いてエンコードされる。節 $C_k = (\ell_1 \lor \ell_2 \lor \ell_3)$ について、リテラルは対応する極性スピンにマッピングされる。二次形式を維持するために、最初の 2 つのリテラルが偽である条件を捉える補助変数 $c_k$ が導入される。エネルギー関数は、すべてのリテラルが偽である（すなわち、対応するすべてのスピンが 0 である）構成にペナルティを課す。

2.3 疎性と目的関数

エネルギー関数に疎性項が追加される：$E_{sparse} = \gamma \sum (p_i + n_i)$。この項はアクティブなスピンにペナルティを課し、最適化器を割り当てられた変数の少ない構成（より短い含意項）へバイアスする。
総エネルギー関数は以下の通りである：
$$E_F = \sum M p_i n_i + \sum E_{clause}(k) + \gamma \sum (p_i + n_i)$$

2.4 重み領域

論文は、正確性を保証するための重み（節ペナルティに対する $\lambda$、整合性に対する $M$、疎性に対する $\gamma$）に関する理論的条件を確立する。具体的には、$\lambda > n\gamma$ かつ $M > n\gamma$（ここで $n$ は変数の数）であれば、エネルギー関数の基底状態は正確に最小基数の含意項に対応する。

2.5 縮小と射影

• 含意項の縮小： 完全な充足割り当てが与えられた場合、フレームワークは「反対」の極性スピンを 0 に固定することで探索空間を制限する。これにより、最適化器は既存の割り当てからリテラルを削除することのみを行い、有効な含意項として残る最短の部分割り当てを見つけることができる。
• 射影： 可視変数の部分集合 $P$ に焦点を当てるために、疎性ペナルティは $P$ 内の変数のみに対して適用される。隠れ変数 $H$ は疎性によって制約されず、自由な補助サポートとして機能する。これにより、モデルは $H$ 経由で式を満たしつつ、$P$ 上の短い割り当てを見つけることができる。

3. 主要な貢献

1. ネイティブな 3 値エンコーディング： 二重極性意味論を通じて部分割り当て（真/偽/未割当）をネイティブに表現する SAT からイジング/QUBO へのエンコーディング。「未割当」状態を解釈するための外部後処理の必要性を排除する。
2. 柔軟な目的関数バリエーション： 含意項の縮小が極性制限によって達成され、射影が可視変数への疎性ペナルティの制限によって達成される QUBO 定式化。これらはすべて単一の固定二次モデル構造内で実現される。
3. 理論的保証： 基底状態が最小基数の含意項に対応することを保証する特定の重み領域（$\lambda > n\gamma, M > n\gamma$）の特定。最終エネルギー値から直接有効な含意項を認識するための基準を提供する。
4. 実証的検証： ランダム 3-SAT および非 CNF 式に対するシミュレーテッド・アニーリングを用いた評価。エンコーディングが短い部分割り当てを生成し、反復的改善を通じて最小性を達成する能力を実証する。

4. 実験結果

著者らは、2 つのベンチマークセットに対して**シミュレーテッド・アニーリング（SA）**を用いてエンコーディングを評価した：

• ランダム 3-SAT： 節数と変数数の比率が低い（$m/n = 1.5$）充足可能なインスタンス。
• 非 CNF 式： Tseitin/Plaisted-Greenbaum 変換を通じて CNF に変換されたブール式。隠れた補助変数を持つ射影設定を生成する。

主要な知見：

• コンパクト性： ランダム 3-SAT において、エンコーディングは平均して変数の約3 分の 1 を未割当のままにしつつ、充足可能性を維持する。
• 最小性： ベースライン SA は小〜中規模のインスタンスではしばしば最小基数の割り当てを見つけるが、問題規模が大きくなるにつれて局所最適解により成功率が低下する。しかし、反復的改善（最良の解を固定し、さらに縮小するために SA を再実行する）は結果を大幅に改善する。
• 最小性対最小基数： 反復的改善は、高い確率で包含最小性（素含意項）を達成する。最小基数（大域的最小サイズ）の達成はより困難だが、特に隠れた完全化を均一に可能にする構造を持つ非 CNF ベンチマークでは頻繁に観察される。
• 射影設定： 射影モードにおいて、この手法は隠れた補助変数の割合が高い場合（全変数の 65〜70%）でも、可視変数に対する最小基数の割り当てを正常に回復する。

5. 意義と主張

この論文は、このフレームワークが、AllSAT や説明パイプラインにおける外部縮小子ループの必要性を代替する、短部分割り当ての計算のための統合最適化アプローチを提供すると主張する。

• 理論的意義： 二重極性表現と最小性を保証する証明可能な重み領域を導入することで、イジングモデルの「完全割り当て」の性質と、多くの推論タスクが要求する「部分割り当て」の要件との間のギャップを埋める。
• 実用的意義： このエンコーディングは、既存のワークフローにおける縮小ステップの「ドロップイン代替」として機能する。著者らは、このアプローチが（シミュレーテッド・アニーリングのような）汎用最適化バックエンド下で堅牢であり、意味的妥当性を示すために専用ハードウェアを必要としないと強調している。ただし、量子アニーラーや専用イジングマシンがより良い結果をもたらす可能性があるとも指摘している。
• 限界： 著者らは控えめに、エンコーディングが理論的には最小基数の基底状態を保証するものの、ヒューリスティック最適化器は局所最適解に陥る可能性があることを認めている。さらに、射影設定において、このエンコーディングは「一貫した証人」（すべての可視完全化に対する単一の隠れ割り当て）を強制する。これは標準的な射影含意項の意味論よりも厳しい要件であるが、著者らは多くの実用的な非 CNF 変換においてこれが成り立つと主張する。

この研究は、部分推論のための二次エンコーディングの意味的検証として位置づけられており、適切なパラメータ調整と反復的改善により、イジング/QUBO モデルが効率的に最小かつ最小基数の含意項を計算できることを実証している。