Generating proofs of unsatisfiability is a valuable capability of most SAT solvers, and is an active area of research for SMT solvers. This paper introduces the first method to efficiently generate proofs of unsatisfiability specifically for an important subset of SMT: SAT Modulo Monotonic Theories (SMMT), which includes many useful finite-domain theories (e.g., bit vectors and many graph-theoretic properties) and is used in production at Amazon Web Services. Our method uses propositional definitions of the theory predicates, from which it generates compact Horn approximations of the definitions, which lead to efficient DRAT proofs, leveraging the large investment the SAT community has made in DRAT. In experiments on practical SMMT problems, our proof generation overhead is minimal (7.41% geometric mean slowdown, 28.8% worst-case), and we can generate and check proofs for many problems that were previously intractable.

翻译：生成不可满足性证明是大多数SAT求解器的重要能力，也是SMT求解器的活跃研究方向。本文首次提出一种高效生成不可满足性证明的方法，专门针对SMT的一个重要子集：单调理论SAT模理论（SMMT），该理论涵盖了许多有用的有限域理论（例如位向量和多种图论性质），并已在亚马逊云科技的生产环境中得到应用。我们的方法使用理论谓词的命题定义，从中生成这些定义的紧凑Horn近似，进而利用SAT社区在DRAT上的大量投入，生成高效的DRAT证明。在实用SMMT问题的实验中，我们的证明生成开销极低（几何平均减速7.41%，最坏情况28.8%），并且能够为许多先前难以处理的问题生成并验证证明。