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）高效生成不可满足性证明的方法。该子类包含许多有用的有限域理论（例如，位向量和多种图论性质），并在亚马逊云服务（Amazon Web Services）中投入生产。我们的方法使用理论谓词的命题定义，从中生成这些定义的紧凑Horn近似，进而利用SAT社区在DRAT上的大量研究成果，生成高效的DRAT证明。在实际SMMT问题的实验中，我们的证明生成开销极小（几何平均耗时增加7.41%，最坏情况下为28.8%），并且能够为许多之前难以处理的问题生成并验证证明。