DRAT Proofs of Unsatisfiability for SAT Modulo Monotonic Theories

TL;DR

This paper addresses the challenge of producing independently checkable proofs for UNSAT in SAT Modulo Monotonic Theories (SMMT), a practically important fragment of SMT. The authors propose a method that starts from propositional definitions of theory predicates, then constructs proof-specific Horn upper-bounds through instantiation-based reasoning, enabling DRAT-proof verification without theory-specific checkers. They implement the approach as MonoProof within MonoSAT and demonstrate minimal solver overhead (7.41% geometric mean slowdown, 28.8% worst-case) while solving industrial-scale benchmarks that were intractable with prior methods. The work delivers pure DRAT certificates by combining propositional reasoning with Horn approximations, achieving scalable, checkable UNSAT proofs for key SMMT theories such as graph reachability and max-flow on symbolic graphs, BV comparisons, and BV sums, with a clear path to extending to additional finite-domain monotonic theories and new proof formats.

Abstract

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.

Figures (4)

• Figure 1: Overview of Our Proof Generation and Checking Method. Inputs (the problem instance file and the propositional definitions of theory predicates) are colored blue; new and modified components are colored orange. Starting from the top-left is the SMMT problem instance, which is solved by MonoSAT. We extended MonoSAT to emit a DRAT-style proof certificate, consisting of learned (via propositional or theory reasoning) clauses, similar to what is proposed in DBLP:conf/dac/OtoniBEHS21. The proof certificate is optionally pre-processed by drat-trim-theory, in which we modified the BackwardCheck procedure heule2013trimming to perform a backward traversal from the final $\bot$, outputting a subset of lemmas sufficient (combined with the original clause database) to derive $\bot$. This is extra work (since a full BackwardCheck is later performed by unmodified drat-trim for the final proof verification at the top-right of the figure), but allows us to avoid verifying some theory lemmas that are not relevant to the final proof. The resulting core lemmas are split between the propositional learned clauses, which go straight (right) to drat-trim, and the theory learned clauses, which are our proof obligations. The heart of our method is the instantiation-based Horn approximation (bottom-center, described in Sec. \ref{['sec:verifyTheory']}). In this step, we use the proof obligations as hints to transform the pre-defined, propositional theory definitions (bottom-left, examples in Sec. \ref{['sec:buildEncoding']}) into proof-specific Horn definitions. The resulting proof-specific definitions together with the CNF from the input instance can efficiently verify UNSAT using unmodified drat-trim DBLP:conf/sat/WetzlerHH14.
• Figure 2: Directed Graph for Running Example in Sec. \ref{['sec:verifyTheory']}. In the symbolic graph (left), the reachability predicate $reach_s^t$ is a function of the edge inputs $a,\ldots,h$.
• Figure 3: Cactus Plots for Solving (left) and Proof Preparation&Checking (right). Each point is the runtime for one instance, so the plot shows the number of instances ($x$-axis) that ran in less than any time bound ($y$-axis). BB denotes standard bit-blasting; LSBB, lemma-specific bit-blasting; and MonoProof is our new method. The left graph shows that MonoProof (and LSBB, which uses MonoProof's solver) is vastly faster than bit-blasting for solving the instances. The right graph shows that MonoProof is also vastly faster than bit-blasting for proving the result; LSBB timed-out on all proofs.
• Figure 4: The workflow for constructing proof-specific Horn definitions. The inputs (proof obligations and a monotonic predicate) are colored in purple, and the trusted bases are highlighted in green. The outputs of the workflow (Horn Definitions and proof-specific Horn definitions) are colored in yellow. Given a monotonic predicate, we first define the semantics of the predicate's atoms in CNFs. (2) These CNF definitions are automatically transformed into monotonic definitions offline. If the monotonic definitions are already in Horn theory, they can be directly used as Horn definitions for RUP checks. Otherwise, (3) during proof checking, they are approximated into proof-specific Horn definitions using witnesses of theory lemmas in the input proof obligation. (4) Both Horn Definitions and proof-specific definitions can verify all sound theory lemmas in a proof via RUP.

Theorems & Definitions (38)

• definition thmcounterdefinition: Positive Monotonic Predicate
• definition thmcounterdefinition: Propositional Definition
• theorem thmcountertheorem
• proof
• Example 1
• definition thmcounterdefinition: Horn Upper-Bound
• definition thmcounterdefinition: Proof-Specific Horn Definition
• Example 2
• definition thmcounterdefinition: Monotonic Definition
• definition thmcounterdefinition: Monotonic Transformation