単調理論に対するSAT不可能性のDRAT証明

本論文は、重要な単調理論の部分集合であるSAT Modulo Monotonic Theories (SMMT)に対して、効率的に不可能性証明を生成する初めての手法を提供する。提案手法は、理論述語の命題的定義を利用し、効率的なHorn近似を生成することで、DRATプルーフを生成する。実験では、提案手法が実用的なSMMT問題に対して最小限のオーバーヘッドで動作し、従来は不可能だった多くの問題に対して証明を生成・検証できることを示す。