技術的概要：CDCL の排他的論理和（Parity）方程式の論理和への拡張

問題定義

衝突駆動節学習（CDCL）は SAT 解決における支配的な手法であるが、Resolution 証明システムによって本質的に制限されている。Resolution において指数関数的な証明サイズを必要とする問題（Tseitin 式や双射鳩の巣原理など）は、CDCL に対して証明的に困難である。一部のソルバーは、擬似ブールソルバーによる Cutting Planes や、排他的論理和（XOR）方程式を処理する CNF-XOR ソルバーなど、より強力な証明システムの断片を取り入れているが、これらのアプローチはしばしば排他的論理和の推論を独立したモジュールとして扱うか、特定の正規形（例：CNF-XOR）に限定されている。

本研究が扱う具体的なギャップは、XNF（XOR-OR-AND 正規形）式をネイティブに処理する CDCL スタイルのアルゴリズムの欠如である。XNF 式は、排他的論理和方程式の論理和である線形節の論理積で構成される（例：$(x \oplus y) \lor \neg(y \oplus z)$）。XNF への一般化である**Res(⊕)**証明システムは、特定の問題において Resolution よりも指数関数的に強力であることが知られているが、既存のソルバーは Res(⊕) 推論を CDCL ループに完全に統合しておらず、また CDCL スタイルのアルゴリズムが Res(⊕) を多項式時間でシミュレートできるという理論的証明も提供していない。

手法

著者は、XNF 式を直接操作するように設計された CDCL アルゴリズムの一般化である**CDCL(⊕)**を提案する。この手法は以下の 3 つの中核コンポーネントに依存している：

1. Res(⊕) の新しい推論規則：
   著者は、標準的なResolutionと弱め（weakening）の規則を加算と基底変換に置き換える Res(⊕) 証明システムの新しい特徴付けを導入する。

   • 加算： $C \lor f$ と $D \lor g$ から、$C \lor D \lor (f + g)$ を導く。
   • 基底変換： $C$ から、$C \equiv D$（意味的に等価）である任意の $D$ を導く。
     重要なのは、方程式を（基底変換を通じて）「分離」し、加算による打ち消しを可能にする**アフィン・レジリューション（affine resolution）**規則を定義している点である。これにより、弱め規則に関連する指数関数的な探索空間の必要性が排除され、多項式シミュレーションが可能となる。

2. 線形代数を用いた単一伝播（Unit Propagation）：
   文字の割り当てに基づいて伝播を行う古典的な CDCL と異なり、CDCL(⊕) は $\mathbb{F}_2$ 上の線形代数を用いて単一伝播を行う。

   • ソルバーは既知の単位（方程式）の集合 $U$ を維持する。
   • 伝播は、線形節 $C$ が $U$ に基づいて新しい方程式 $f$ または矛盾（$1$）を意味するかどうかをチェックする。
   • これは、節の「線形否定」（節を偽にする割り当ての部分空間）を $U$ の張る空間に対して簡約化することで実装される。節の否定が $U$ の張る空間に単一の方程式 $f$ を加えたものに含まれる場合、$f$ が導かれる。

3. 衝突分析による節学習：
   本論文は、1-UIP（最初の一意な帰結点）節学習戦略を XNF 設定に適応させる。帰結グラフは線形方程式に直接変換されないため、学習アルゴリズムは意味論的に動作する：

   • 衝突節（矛盾の原因）から開始する。
   • 反復的に基底変換を適用して、最新の決定に責任がある方程式を分離する。
   • 加算規則を適用して、分離された節と衝突の原因を組み合わせ、決定変数を効果的に打ち消す。
   • このプロセスを、現在の決定レベルで伝播を強制する**主張節（asserting clause）**が見つかるまで繰り返す。

主要な貢献

理論的貢献

• 双方向的な接続： 本論文は、CDCL(⊕) が Res(⊕) 証明を生成するだけでなく、非決定的な決定とリスタートが与えられれば、Res(⊕) 証明システムを多項式時間でシミュレートすることを証明する。これは、古典的な CDCL と Resolution の関係を反映している。
• 新しい証明システムの特徴付け： 著者は、Res(⊕) と多項式的に等価であるが弱め規則を持たない新しい推論規則のセット（加算と基底変換）を提供し、これらをアルゴリズム的実装に適したものにしている。
• 入力 Res(⊕) 同等性： 本論文は、CDCL(⊕) における単一伝播が、古典的 CDCL に関する既知の結果を一般化する、*入力 Res(⊕)*として知られる Res(⊕) の断片と同等であることを証明する。
• 改善されたシミュレーション係数： シミュレーションの証明は、節の分解の吸収方法を最適化することで、古典的 CDCL/Resolution 関係における多項式係数を改善し、[7] の結果をより単純な議論で一致させている。

実用的貢献

• Xorcle の実装： 著者は、CDCL(⊕) の概念実証ソルバーであるXorcleを提示する。
  • ビットパックを使用して $\mathbb{F}_2$ 上の効率的な線形代数を実装している。
  • VSIDS や CMTF を XNF 文脈に一般化した新しい節選択ヒューリスティックであるCSIDS（Clause State Independent Decaying Sum）を導入している。
  • 排他的論理和式をサポートするように LRUP 証明ログ形式を拡張した**LRUP(⊕)**を導入している。
• XNF 向けのヒューリスティック： 本論文は、監視構造（複雑なウォッチリストの維持ではなく、線形依存関係により節を循環させる）、決定手続き（節の否定からランダムな方程式に基づいて分岐）、および位相選択（節を偽にすることを優先）の適応について詳述している。

実験結果

著者は、Xorcle を以下のベンチマークスイートで評価した：

• Ascon-128： 暗号学に関連する 2-XNF ファミリー。
• ランダムおよび制限付き k-XNF： 変数と方程式の数が異なる合成式。
• Tseitin 式： Resolution に対して困難であることが知られている CNF 符号化された排他的論理和問題。

主要な発見：

• XNF における性能： Xorcle は、ネイティブな XNF ベンチマークにおいて既存のソルバー（Kissat、CryptoMiniSAT、2-Xornado）を上回った。特に、一般的な XNF 推論を使用しているにもかかわらず、Ascon-128 インスタンスにおいて専用 2-XNF ソルバーである 2-Xornado を上回った。
• Tseitin 式における性能： CNF で符号化された Tseitin 式において、Xorcle は実行時間においてほぼ多項式的なスケーリングを示した。一方、Resolution ベースのソルバーは指数関数的な時間を必要することが知られている。これは前処理なしで、コアとなる CDCL(⊕) 推論のみに依存して達成された。
• 決定の質： Xorcle は競合するソルバーよりも著しく少ない決定を必要とした。これは、排他的論理和に基づく分岐と推論メカニズムが、これらの問題クラスに対してより効果的であることを示唆している。

意義と主張

本論文は、CDCL(⊕) が、排他的論理和推論を CDCL パラダイムに完全に統合する最初の厳密な理論的枠組みと実用的な実装を提供すると主張している。

• 理論的意義： CDCL の限界はアルゴリズム構造に固有のものではなく、基盤となる証明システム（Resolution）にあることを確立する。Res(⊕) に移行することで、CDCL は理論的に標準的な CDCL に対して指数関数的に困難な問題を解決できる。
• 実用的意義： 結果は、ネイティブな XNF 解決が実現可能であり、XNF を CNF や CNF-XOR に変換することよりも優れている可能性を示唆している。前処理なしで Tseitin 式をほぼ多項式時間で解決できる能力は、SAT 解決における既知の困難さの障壁を克服する排他的論理和推論の可能性を浮き彫りにしている。
• 将来の方向性： 著者は控えめに、Xorcle は概念実証であると指摘している。現在、節削除、高度なリスタート、動的ヒューリスティックなど、いくつかの標準的な CDCL 最適化が欠落しており、「1-UIP」や「節最小化」といった概念を意味論的 XNF 設定に完全に一般化していない。この研究は、暗黙的に排他的論理和推論を必要とする CNF 式をターゲットとしたヒューリスティックに関するさらなる研究への扉を開く。