技術的概要：Eager エンコーディングを超えて：SMT における理論レマ列挙のための理論非依存アプローチ

1. 問題定義

Satisfiability Modulo Theories（SMT）において、ブール推論手法の持ち上げ（lifting）は、しばしば理論レマ（T-レマ）の生成を必要とする。これらは、命題論理的には充足可能だが理論的に矛盾する真理値割り当てを排除する、T-妥当な節である。

標準的な SMT 解法は、探索中にこれらのレマを「遅延的（lazy）」に必要に応じて生成するが、最小 unsat-core 抽出、MaxSMT、T-OBDD や T-SDD のコンパイルといった特定の複雑な SMT タスクでは、完全な T-レマのセットを事前に「Eager（先行的）」に計算する必要がある。

既存の「古典的」な Eager SMT エンコーディングはこの目的には不十分である。なぜなら：

1. 彼らは EUF、DL、LRA といった数少ない単純な理論に特化しているためである。
2. 理論の組み合わせ（theory combination）に準拠していないためである。
3. しばしば不要なレマを過剰に生成するためである。

現在、特に計算オーバーヘッドをオフライン段階に押しやることでオンラインクエリを多項式時間で可能にするナレッジコンパイル（KC）アプリケーションにおいて、任意の式に対する完全な T-レマのセットを効率的に列挙するための理論非依存（theory-agnostic）な手法が存在しない。

2. 手法

著者は、背後にある理論に依存しない T-レマの列挙フレームワークを提案する。このアプローチは、AllSMT（すべての T-充足可能割り当ての列挙）を用いたベースライン手法を基盤とし、スケーラビリティを向上させる 3 つの直交かつ組み合わせ可能な改善を導入する。

2.1 ベースライン：完全 AllSMT 列挙

ベースライン手法（アルゴリズム 2）は、入力式 $\phi[\alpha]$ に対して、完全かつ非射影的な AllSMT 列挙を実行する。これは、反復的に T-充足可能な完全真理値割り当てを見つけ、それらをブロックし、式が充足不能になるまでソルバによって学習された T-レマを収集する。

• 限界：このアプローチは、完全割り当ての列挙に依存している。例 2 に示されるように、単純な部分列挙は、特定の T-矛盾する完全割り当てがソルバによって探索されない場合、必要な T-レマを生成できない可能性がある。しかし、すべての完全割り当てを列挙することは、組み合わせ爆発により計算的に非現実的であることが多い。

2.2 改善 1：分割統治法（D&C）

完全列挙のコストを軽減するため、著者は分割統治法（Divide-and-Conquer）戦略（アルゴリズム 3）を提案する。

1. 部分AllSMT 列挙を実行し、ブール探索空間を、互いに素な T-充足可能な部分割り当ての集合（$M_{\alpha}^p$）に分解する。
2. 各部分割り当て $\mu \in M_{\alpha}^p$ に対して、制限された式 $\phi \land \mu$ 上で完全AllSMT 列挙を実行する。
3. 完全列挙は並列に実行される。

• 根拠：これは、1 つの大型で非現実的な完全列挙を、1 つの安価な分解ステップと、より小さく管理可能な多数の完全列挙に変換する。

2.3 改善 2：射影列挙

著者は、T-矛盾はブール原子（$\alpha_B$）ではなく、理論原子（$\alpha_T$）への割り当てによってのみ決定されると指摘する。

• 手法：$\alpha_T$ に対してのみ射影された AllSMT 列挙を実行する（アルゴリズム 4）。
• 理論的根拠：定理 1 は、列挙を T-原子に射影することで T-レマの完全なセットが得られることを証明している。
• 利点：これは探索次元を劇的に削減する。$\alpha_T$ 上の 1 つの T-充足可能な割り当ては、原子の完全な集合に対する最大 $2^k$ 個の完全割り当て（ここで $k$ はブール原子の数）を表すため、メモリ使用量とブロック節のサイズを大幅に削減する。

2.4 改善 3：理論駆動型パーティショニング

$\phi$ 内の原子の集合が、ある集合の原子と他の集合の原子が変数や未解釈記号を共有しないような互いに素な集合（$\alpha_1, \dots, \alpha_n$）に分割できる場合、問題はさらに分解可能である（アルゴリズム 5）。

• 手法：性質 1 と定理 2 に基づき、T-レマを各パーティションに対して独立して列挙できる。アルゴリズムは、原子を反復的にパーティショニングし、各パーティションの原子に対して射影されたレマを列挙し、結果を蓄積する。
• 利点：これは、単一の完全列挙を $n$ 個の独立した射影列挙に分解することを可能にし、互いに素なコンポーネントを持つ問題に対して潜在的な指数関数的な高速化をもたらす。

3. 主要な貢献

1. 理論非依存フレームワーク：理論固有の Eager エンコーディングを超えて、任意の理論に対する完全な T-レマのセットを列挙する手法を明示的に提示した最初の事例。
2. スケーラビリティ技術：3 つの直交する技術の導入。
   • 分割統治法：ブール空間を分解することで探索を並列化する。
   • 射影列挙：T-原子に焦点を当てることで探索次元を削減する。
   • パーティショニング：式内の構造的な互いに素性を活用して部分問題を独立して解決する。
3. 理論的保証：これら最適化が、すべての T-矛盾する割り当てを排除するために必要な T-レマの完全性を維持することを示す形式的証明（定理 1 と 2）。
4. ナレッジコンパイルとの統合：この作業は、OBDD や SDD などの決定図に代表されるナレッジコンパイル手法を SMT レベルに持ち上げるための基盤技術として機能し、T-レマ列挙という以前のボトルネックに対処する。

4. 実験結果

これらの手法は、2 つのベンチマークセットで評価された。

• 合成 SMT(LRA) インスタンス：[16] から生成された 450 のランダム生成問題。
• 時間的計画インスタンス：「Painter」ドメインの計画問題の 90 の SMT エンコーディング。

パフォーマンス指標：

• 時間効率：
  • 合成ベンチマークにおいて、D&Cはベースラインに対して最大 2 桁の性能向上をもたらし、タイムアウト内で 17 個追加の問題を解決した。
  • 射影を追加することでさらに結果が改善され、D&C 単独よりも 30 個多く問題を解決し、以前に解決されたインスタンスの時間を劇的に短縮した。
  • パーティショニングは合成データでは改善を示さなかった（互いに素なパーティションを持つ問題が少なかったため）が、計画問題では非常に効果的であった。
  • 計画問題において、パーティショニングは支配的な要因であり、以前は非現実的だったホライズン 5 の問題を解決可能にし、数桁の高速化を達成した。
• レマの数：
  • D&C は、並列的な冗長性により、わずかに多くのレマを生成する傾向があった。
  • 射影とパーティショニングは、一般的に冗長な探索を軽減し、より強く小型のレマを生成することで、列挙されたレマの数を削減した。
• レマのサイズ：
  • 計画問題におけるパーティショニングは、特定のパーティションのみに関与する T-矛盾する分枝の早期プルーニングに起因すると考えられる、明らかに小型（リテラル数が少ない）の T-レマをもたらした。

5. 意義と主張

本論文は、これらの手法がベースラインの AllSMT アプローチと比較して、T-レマ列挙の効率とスケーラビリティを劇的に向上させると主張している。

• 可能化の役割：主な意義は、ナレッジコンパイルの実用的な応用を可能にすることにある。著者は、以前の研究 [16] において、T-レマ列挙が決定図のコンパイルにおける「主なボトルネック」であったと指摘している。このボトルネックを解消することで、提案された手法は、これらのコンパイル手法を複雑な実世界のインスタンスに拡張する道を開く。
• 謙虚さ：著者は、改善が文脈に依存することを慎重に指摘している。例えば、射影は計画問題には役立たなかった。なぜなら、それらの特定のエンコーディングでは、T-原子の割り当てがブール割り当ての決定的な帰結であったからである。同様に、パーティショニングは、問題構造が自然に互いに素なパーティションを許容する場合にのみ利益をもたらした。

要約すると、本論文は、Eager T-レマ列挙のための堅牢で理論非依存なツールキットを提供し、以前は非現実的だったステップをスケーラブルなプロセスに変換することで、MaxSMT やナレッジコンパイルなどの高度な SMT アプリケーションを促進する。