单调理论SAT模的不可满足性DRAT证明
计算机科学中的逻辑
2024-04-19 v3
摘要
生成不可满足性证明是大多数SAT求解器的一项有价值的能力，也是SMT求解器的一个活跃研究领域。本文首次提出了一种高效生成不可满足性证明的方法，专门针对SMT的一个重要子集：单调理论SAT模（SMMT），该子集包含许多有用的有限域理论（例如，位向量和许多图论性质），并在亚马逊网络服务中用于生产。我们的方法使用理论谓词的命题定义，从中生成定义的紧凑Horn近似，从而产生高效的DRAT证明，利用了SAT社区在DRAT上的大量投入。在实际SMMT问题的实验中，我们的证明生成开销极小（几何平均减速7.41%，最坏情况28.8%），并且我们能够为许多以前难以处理的问题生成和检查证明。
引用
@article{arxiv.2401.10703,
title = {DRAT Proofs of Unsatisfiability for SAT Modulo Monotonic Theories},
author = {Nick Feng and Alan J. Hu and Sam Bayless and Syed M. Iqbal and Patrick Trentin and Mike Whalen and Lee Pike and John Backes},
journal= {arXiv preprint arXiv:2401.10703},
year = {2024}
}