線形実数算術における充足可能性（SMT）のための連続最適化

要旨: 決定可能性（充足可能性）問題に対する理論（SMT: Satisfiability Modulo Theories）向けの効率的な解法は、ハードウェア検証や設計自動化といった産業用途において不可欠です。既存のアプローチは主として、競合駆動型節学習（conflict-driven clause learning）に基づいていますが、これは構造的に並列化しにくいため、スケールが伸びにくいという問題があります。本研究では、SMTのための、スケーラブルで高度に並列化可能な連続変数最適化フレームワークとしてFourierSMTを提案します。われわれは、ブール領域から混合ブール-実数領域へ拡張された、拡張WFE（xWFE）と呼ばれる、Walsh-Fourier展開（WFE）を一般化し、SMTに対して勾配法を用いることを可能にします。これにより、離散変数の局所更新によって、高アリティ制約に対する充足可能な変数割当てを見つけるという課題に対処します。xWFEの評価複雑性を低減するために、拡張バイナリ決定図（xBDD）を提示し、xWFEからxBDDへ制約を写像します。さらに、ランダム化丸めによりxBDDの回路出力確率（COP）をサンプリングすることが、xWFEの期待値に等しいことを示します。これにより制約の効率的な計算が可能になります。減らした問題は収束が保証され、充足可能性を保つことを示し、解の健全性（サウンドネス）を確実にします。このフレームワークは、大規模なスケジューリングおよび配置問題に対してベンチマークされており、最大10,000変数および700,000制約を扱い、最先端のSMTソルバに比べて8倍の高速化を達成しています。これらの結果は、連続システムを扱うSMTのGPUベース最適化への道を切り拓きます。