Core Concepts
本論文は、重要な単調理論の部分集合であるSAT Modulo Monotonic Theories (SMMT)に対して、効率的に不可能性証明を生成する初めての手法を提供する。提案手法は、理論述語の命題的定義を利用し、効率的なHorn近似を生成することで、DRATプルーフを生成する。実験では、提案手法が実用的なSMMT問題に対して最小限のオーバーヘッドで動作し、従来は不可能だった多くの問題に対して証明を生成・検証できることを示す。
Abstract
本論文は、SAT Modulo Monotonic Theories (SMMT)に対する不可能性証明を効率的に生成・検証する手法を提案している。
主な内容は以下の通り:
不可能性証明は信頼性向上や抽象化のために重要であるが、一般的なSMTソルバーでは効率的な証明生成が困難である。一方、DRATプルーフは効率的な検証が可能だが、理論推論を扱うことが難しい。
SMMTは有限単調理論を効率的にサポートする重要な部分集合であり、実用的な問題に広く適用されている。
提案手法は、理論述語の命題的定義を利用し、効率的なHorn近似を生成することで、DRATプルーフを生成する。これにより、DRATプルーフチェッカーを用いて理論レンマを効率的に検証できる。
実験では、提案手法が実用的なSMMT問題に対して最小限のオーバーヘッドで動作し、従来は不可能だった多くの問題に対して証明を生成・検証できることを示している。
Stats
提案手法の解決時間のオーバーヘッドは、ネットワーク到達可能性ベンチマークで幾何平均14.10%、最悪ケース28.8%、エスケープルーティングベンチマークで幾何平均1.11%、最悪ケース5.71%であった。
全ベンチマークの幾何平均オーバーヘッドは7.41%であった。