Certified MaxSAT Preprocessing

要約

過去数十年にわたるブール充足可能性 (SAT) 解法の進歩に基づいて、最大充足可能性 (MaxSAT) は NP 困難最適化問題を解くための実行可能なアプローチになりましたが、MaxSAT ソルバーの正確性を確保することは依然として重要な懸案事項です。
SAT の場合、この問題は証明ログの使用によって主に解決されています。つまり、ソルバーは、正確さを証明するために、機械検証可能な満足 (不) 証明を出力します。
ただし、MaxSAT に関しては、プルーフ ロギング ソルバーが開発され始めたのはごく最近のことです。
さらに、これらの初期の取り組みは、中核となる解決プロセスのみを対象としており、入力問題インスタンスを適切なソルバーに渡す前に実質的に再定式化できる前処理フェーズを無視しています。
この研究では、擬似ブール証明ロギングを使用して、最新の幅広い最新の MaxSAT 前処理技術の正確性を証明する方法を示します。
VeriPB ツールと CakePB ツールを組み合わせて拡張することで、入力と前処理された出力の MaxSAT 問題インスタンスが同じ最適値を持つかどうか、正式に検証されたエンドツーエンドの証明チェックを提供します。
適用された MaxSAT ベンチマークの広範な評価により、私たちのアプローチが実際に実行可能であることが示されました。

要約(オリジナル)

Building on the progress in Boolean satisfiability (SAT) solving over the last decades, maximum satisfiability (MaxSAT) has become a viable approach for solving NP-hard optimization problems, but ensuring correctness of MaxSAT solvers has remained an important concern. For SAT, this is largely a solved problem thanks to the use of proof logging, meaning that solvers emit machine-verifiable proofs of (un)satisfiability to certify correctness. However, for MaxSAT, proof logging solvers have started being developed only very recently. Moreover, these nascent efforts have only targeted the core solving process, ignoring the preprocessing phase where input problem instances can be substantially reformulated before being passed on to the solver proper. In this work, we demonstrate how pseudo-Boolean proof logging can be used to certify the correctness of a wide range of modern MaxSAT preprocessing techniques. By combining and extending the VeriPB and CakePB tools, we provide formally verified, end-to-end proof checking that the input and preprocessed output MaxSAT problem instances have the same optimal value. An extensive evaluation on applied MaxSAT benchmarks shows that our approach is feasible in practice.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google