増分SATソルビングの認証

証明とモデルをチェックすることで結果を認証することは、現代のSATソルビングの重要な特徴です。仮定とコア抽出を用いた増分的ソルビングは多くのアプリケーションにとって重要ですが、増分証明証明書のサポートは依然として不足しています。私たちは、増分SATソルビングのための証明形式と対応するチェックツールを提案します。さらに、解決のヒントを活用するためにそれを拡張します。有界モデル検査および理論モジュロ充足性のための増分SATソルビングに関する実験は、私たちのアプローチの実現可能性を示し、解決のヒントがチェック時間を大幅に短縮することをさらに確認します。