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 近似定义，进而构建高效的 DRAT 证明，充分利用了 SAT 领域在 DRAT 上的大量投入。在实际 SMMT 问题实验表明：证明生成开销极小（几何平均减速 7.41%，最坏情况 28.8%），且能对许多此前难以处理的问题实现证明生成与验证。