1 Introduction

Automated reasoning tools, particularly satisfiability modulo theories (SMT) solvers [6], are widely used in applications requiring high levels of trust including cloud security [2] and hardware and software verification [15, 23,24,25, 28]. Because SMT solvers are large and complex pieces of software, some tools now produce proof certificates [3] that justify solver reasoning thereby increasing confidence for unsatisfiable results.

To derive unsatisfiability, an SMT solver performs: i) preprocessing—rewriting and simplification; ii) clausification—transforming the preprocessed input into clauses forming the Boolean abstraction; iii) propositional satisfiability (SAT) reasoning over the clauses; and iv) theory reasoning—using theory solvers to learn theory lemmas constructed as clauses that refine the Boolean abstraction; eventually deriving a contradiction when no solution exists. An SMT proof certificate contains the information necessary to verify reasoning underlying the SAT refutation, including both the SAT reasoning steps used to derive a contradiction and the preprocessing, clausification, and theory reasoning proof steps used to justify the relevant clauses and theory lemmas that appear in the SAT reasoning. Each proof step is accompanied by a justification with sufficient details for efficient validity checking. While justifications for SAT reasoning and clausification are straightforward to log, those for preprocessing and theory lemmas can be substantially more complex, as they must capture the intricate reasoning of rewriting engines and theory solvers.

The standard eager approach has the preprocessing module and theory solvers produce justifications online during solving [3]. For example, each time a theory solver implementing congruence closure for the theory of uninterpreted functions (QF_UF) is called, the theory solver will record the series of inferences used to deduce a theory lemma [29]. Once the SMT solver derives a conflict, the solver traces its SAT reasoning and emits all relevant theory lemmas and their justifications to the proof certificate. Any justifications for theory lemmas that are ultimately unused represent wasted computation; this overhead can be substantial for certain theories [5, Sect. 6], and is exacerbated in high-throughput applications processing up to a billion queries a day [35].

An alternative lazy approach has the SMT solver produce a proof skeleton— a subset of the full reasoning steps that omits e.g. theory lemma justifications— thereby reducing proof-logging overhead during solving. Existing frameworks support skeletons containing clausification steps, unjustified theory lemmas, and SAT reasoning [14, 18, 31]. To check such a skeleton, the SAT refutation is extracted, optionally trimmed to remove redundant reasoning steps, and the theory lemmas retained in the trimmed refutation are then justified by a dedicated elaborator and verified by a proof checker.

We present a more general approach for SMT proof skeletons (Sect. 3) that logs only core SMT reasoning: preprocessing (\(pre_i\)), clausification (\(C_i\)) and theory lemmas (\(T_i\)). Such a skeleton is accessible to SMT solvers without prior proof support for theories or SAT reasoning. Our skeleton extends the Alethe proof format [37], which supports preprocessing and quantifier reasoning beyond the scope of existing skeleton formats. The skeleton contains justifications \(J^{\text {type}}_i\) for the preprocessing and clausification steps but omits theory lemma justifications:

$$ (pre_1, J^{\text {pre}}_1), \dots , (pre_m, J^{\text {pre}}_m), (C_1, J^{\text {C}}_1), \dots , (C_r, J^{\text {C}}_r), (T_1,\_), \dots , (T_k,\_) $$

Rather than recording the SMT solver’s SAT refutation, our skeleton contains only the information needed to extract the unsatisfiable propositional formula \( F= C_1 \wedge \cdots \wedge C_r \wedge T_1 \wedge \cdots \wedge T_k\). We developed separate tools for SAT reasoning and trimming that produce an unsatisfiable core \(U= C_1 \wedge \cdots \wedge C_r \wedge T'_1 \wedge \cdots \wedge T'_j \text { with } U \subseteq F\). By performing SAT reasoning externally, we can apply trimming strategies specifically targeting theory lemma removal, reducing the number of theory lemmas in the core. Finally, we produce justifications for the remaining theory lemmas in the core: \((T'_1, J^T_1), (T'_2, J^T_2), \dots , (T'_j, J^t_j)\).

While other skeleton checking tools used hand-crafted elaborators and checkers for each supported theory to improve performance, we use a general elaborator, cvc5  [5], that can produce Alethe justifications [22] for lemmas from the quantified and quantifier-free theories of equality and uninterpreted functions (UF), linear integer and real arithmetic (LIA and LRA), and theory combinations therein (Sect. 4.2). We mitigate the overhead of using a general-purpose elaborator by i) organizing justification in batches, meaning several theory lemmas can be justified and checked at once, and ii) parallelizing theory lemma justifications.

In summary, our contributions are:

  • a generic framework for production and checking of SMT proof skeletons that relies on external SAT reasoning tools, based on the Alethe proof format, implemented in the SMT solver cvc5 and proof checker Carcara;

  • iterative proof-trimming techniques for minimizing theory lemma counts in cores, together with batched and parallelized lemma justification;

  • a large-scale evaluation on SMT-LIB benchmarks that demonstrates the effectiveness of our lazy approach on the quantifier-free logics QF_UF, QF_LIA, QF_LRA, and QF_UFLIA and its limitations on the quantified logics UF and UFLIA.Footnote 1

2 Background

2.1 Proof Production in SAT

We represent formulas for the Boolean satisfiability problem (SAT) in propositional logic using conjunctive normal form (CNF), i.e., conjunctions of clauses where each clause is a disjunction of literals. A literal \(\ell \) is either a Boolean variable x or a negated variable \(\overline{x}\). A unit clause contains a single literal. Unit propagation applies the following operation to formula F until a fixed point is reached: for all units \(\alpha \), remove clauses from F containing a literal in \(\alpha \) and remove from the remaining clauses all literals negated in \(\alpha \). If unit propagation yields the empty clause (\(\bot \)) we say it derived a conflict. An unsatisfiable core (core) of a formula is a subset of the formula that is unsatisfiable, and is minimal if removing any clause from the core will make it satisfiable.

The dominant SAT algorithm, conflict-driven clause-learning (CDCL), produces a clausal proof for unsatisfiable problems. A clausal proof is a sequence of clause additions and deletions, where each subsequent clause addition step must meet the criteria of a chosen proof system, e.g., \(F, C_{1}, C_{2}, \dots , C_{m}\) is a clausal proof of \(C_{m}\). The case of \(C_{m} = \bot \) serves as a refutation for F. We will refer to clauses in the proof as clausal lemmas to avoid confusion with theory lemmas. CDCL solvers and proof checkers commonly use the resolution asymmetric tautology with deletions (DRAT) proof system [20], but when used within SMT solvers they are restricted to a subset of DRAT, the reverse unit propagation with deletions (DRUP) proof system, to prevent unsound reasoning. A clause C is RUP w.r.t. formula F if unit propagation on F and the units \(\overline{\ell } \) for \( \ell \in C \) derives a conflict.

A DRUP proof is transformed into a linear RUP (LRUP) proof by adding hints to proof steps, i.e., identifiers that denote clauses propagated in each RUP check, used to speed up checking with a formally verified tool [39]. The proof trimming tool DRAT-trim simultaneously trims unnecessary clausal lemmas from the proof and transforms RUP steps into LRUP steps through a process called backward checking (Sect. 4.1).

2.2 Proof Production in SMT

SMT solvers generally follow the CDCL(\(\mathcal {T}\)) architecture [30], combining a CDCL SAT solver and a set of specialized theory solvers. The SAT solver searches for satisfying assignments for the Boolean abstraction of the input, in which the theory atoms are abstracted as propositional variables. The theory solvers determine whether these literals are also satisfiable modulo the combination of theories \(\mathcal {T}\). If they are not, a \(\mathcal {T}\)-valid disjunction of literals, a lemma, is learned to capture the inconsistency, which will force the SAT solver to search for a new assignment, if any exists. The other key solving components include a preprocessing module, which simplifies the input formulas as much as possible; and a clausifier, which converts the preprocessed formulas into a conjunction of clauses over theory literals, whose abstraction is the initial clause set for the SAT solver. Given the differences in these components, and the varying ways solvers simplify formulas and reason about theories, SMT solvers can differ significantly in how they produce proofs [8, 19, 21, 27], and a standard proof system or format is yet to emerge in SMT. Here we focus on the proof production architecture of cvc5, the Alethe proof format [37] and its checker Carcara  [1], which we extend for this work, and the proof system relevant to the logical fragment we consider: formulas involving any of quantifiers, equality, uninterpreted functions, and linear integer or real arithmetic.Footnote 2

Given an SMT input \(\varphi \), cvc5 can produce a refutation in the Alethe proof system with the form \(\pi :\varphi \rightarrow \bot \), i.e., deriving \(\bot \) from the assumption \(\varphi \). This proof is produced modularly, with each solving component producing individual proofs that are merged together into this refutation. The preprocessing module produces proofs \(\pi ^{\textrm{pp}}_i:\>\varphi \rightarrow \phi _i\), for each \(\phi _i\) generated during the simplification of \(\varphi \). Different simplifications may require different sets of rules, such as constant folding in different theories or if-then-else elimination. The clausifier produces proofs \(\pi ^{\textrm{cnf}}:\>\phi \rightarrow C_j\) for each clause \(C_j\) generated from the preprocessed formulas. The rules in each \(\pi ^{\textrm{cnf}}\) are a combination of Boolean transformations and introductions of Boolean formulas representing the definition of Tseytin variables, used to ensure that the CNF conversion is polynomial. The combination of theory solvers produce proofs \(\pi ^{\textrm{t}} : L\) for each theory lemma L derived. The rules in each \(\pi ^{\textrm{t}}\) depend on the respective theory. For example, the UF theory reasoning is modeled with rules to describe congruence reasoning [17], whereas the LRA theory reasoning is modeled with a rule capturing Farkas’ lemma [13, 36], which guarantees that there exists a linear combination of these inequalities equivalent to \(\bot \), that can be checked polynomially. For LIA, rules for branching and integer bound tightening are used in addition to the Farkas’ lemma. The SAT solver produces a resolution proof for the refutation of the clause set corresponding to the subset of the clausified preprocessed input and the theory lemmas needed to derive \(\bot \). Note that \(\pi ^{\textrm{res}}\) is in terms of the first-order clauses, as are the derivation rules that conclude \(\bot \) from them, since the inferences on the propositional abstraction are lifted to the original literals. By connecting the assumptions of each of these proofs, the final refutation of the input \(\varphi \) is generated. For more details see e.g. [5, 19].

Alethe proofs are a series of steps represented as an indexed list of step commands referencing their premises and justified by a given inference rule, concluding a clause, represented as a list of theory literals. The command assume is analogous but used only for introducing assumptions. The indexed steps induce a directed acyclic graph rooted on the step concluding \(\bot \) and with \(\varphi _1,\,\dots ,\, \varphi _n\) as the only assumption leaves (the input \(\varphi \) is generally given as multiple assertions ). The format supports subproofs, which simulate the effect of the \(\Rightarrow \)-introduction rule of Natural Deduction, where local assumptions are put in context and the last step in a subproof represents its conclusion and the closing of its context. The overall proof may be seen as preprocessing and a ground first-order resolution refutation with theory lemmas justified by closed subproofs. Alethe proofs can be reconstructed in several proof assistants [11, 12, 22, 38] and it has a dedicated high-performance checker and elaborator, Carcara.

Example 1

This QF_UF query requiring simple congruence reasoning is used throughout the paper, labelled CongEx. The query can be found in the Github repository.

A block of code with six logical assertions using variables a, b, d, p1, p2, and p3. Each line checks a condition combining these variables with logical operators like and, or, and not. The code tests relationships such as equality between a and b, b and d, and complex conditions involving p1, p2, and p3. This code is likely used to verify specific logical rules or constraints in a program.
Fig. 1.
A flowchart illustrating a verification process involving two main systems: Carcara and Theory Oracle. The process starts with a Query, which goes through a step labeled "cvc5" producing a Skeleton. This Skeleton enters Carcara, where it undergoes Preprocessing and Classification, leading to a Verified status. Carcara also uses Theory Lemmas, which connect to Proof Elaboration, producing a Full Proof. Theory Oracle receives inputs labeled as logical expressions from the Query and Theory Lemmas, performing Theory Trimming to extract a Core subset. This Core is passed to Theory Justification, which then sends data to Theory Checking. Theory Checking sends a Verified signal back to Proof Elaboration in Carcara. Arrows indicate the flow of data and verification steps, with solid lines for main processes and dashed lines for verification feedback. The chart shows how the two systems interact to verify queries and produce proofs.

SMT solving and proof checking. Carcara checks preprocessing and clausification steps normally. Then, the theory oracle produces, trims, and checks SAT reasoning and justifies and checks core theory lemmas. LRUP proof production and theory justifications can optionally be used for proof elaboration (dashed lines).

Full size image

3 The Alethe SMT Proof Skeleton Framework

Our SMT proof skeleton framework, shown in Fig. 1, is divided into solving, checking, and a theory oracle for the new proof rule prop_unsat. The oracle computes and trims a SAT refutation, then justifies and checks the core theory lemmas.

In cvc5, the existing eager approach [5] computes and stores all preprocessing and theory lemma justifications during solving, then after solving trims the SAT refutation and prints the relevant proof steps.Footnote 3 We instrumented cvc5 to produce an Alethe proof skeleton by logging inferences as they were derived. The skeleton includes fully justified preprocessing and clausification steps transforming the preprocessed input query into clauses , plus two new step types: unjustified theory lemma additions (hole) producing the set , and a claim of propositional unsatisfiability (prop_unsat). An example hole step from CongEx derived via transitivity is:

z sub small t squared equals c sub small a squared plus c sub small d squared plus two times c sub small a times c sub small d times cosine of the angle between c sub small a and c sub small d.

Unlike the default eager approach, proof logging within theory solvers is disabled when producing theory lemma holes, speeding up solving. Furthermore, the skeleton omits SAT reasoning and instead concludes with the prop_unsat step containing an unsatisfiable set of premises . A prop_unsat step for CongEx would, e.g., be

Table listing sample identifiers in a single row, labeled as "sample_prop_current" and "specimen," followed by columns labeled C1 through C9, T1, and T2. This table appears to organize or categorize samples by these codes, likely for tracking or comparison purposes in a study or dataset.

which uses 9 justified premises and 2 unjustified theory lemmas (T1 and T2). Their conjunction (each interpreted in their clausified format) forms an unsatisfiable propositional formula.

The checker, Carcara, accepts the resulting skeleton and verifies the preprocessing and clausification steps normally, skipping the theory lemma hole steps. Upon reaching the prop_unsat step, it calls the external theory oracle with a propositional representation of the premises (F) and an SMT-LIB representation of the theory lemmas. The oracle verifies F’s unsatisfiability by computing a refutation, then justifies and checks the relevant theory lemmas. An optional elaborator replaces the prop_unsat step by a fine-grained proof using theory lemma justifications and the LRUP proof from the oracle, enabling independent checking outside our framework. The elaborator’s detailed description and evaluation can be found in the tool’s Github repository.

The oracle operates in two phases: (1) theory trimming, using a SAT solver and proof trimmer to verify SAT reasoning and reduce the number of theory lemmas in the core; and (2) theory lemma justification and checking, using cvc5 to compute justifications for core lemmas and default Carcara to verify them. Theory lemmas are processed in batches (multiple at a time) and the process can be parallelized. If the theory oracle verifies the SAT reasoning and verifies the justifications of core lemmas it returns a verified result for the prop_unsat step and otherwise returns a not verified result. Note, the oracle could in principle use any tool to justify theory lemmas and check those justifications. We chose to use cvc5 and Carcara because they already support many theories. Furthermore, all justifications produced by cvc5 within the external oracle are verified by Carcara without nested calls to the external oracle, so the reliance on cvc5 as skeleton producer and theory lemma elaborator introduces no unsoundness.

4 Theory Oracle for the prop_unsat Proof Step

4.1 Theory Trimming with SAT Reasoning

The theory trimming module receives an unsatisfiable propositional formula F containing the clausified preprocessed input and the clausified unjustified theory lemmas , together with a mapping from theory lemma clauses to their SMT-LIB representation. It first computes a clausal proof ( ) of F using the SAT solver CaDiCaL  [7], then applies our theory-last proof trimmer to both verify the SAT reasoning and produce a core \(U \subseteq F\). Only the theory lemmas in U are subsequently justified and checked.

Theory-Last Proof Trimming. Theory-last trimming modifies the backward trimming algorithm of DRAT-trim  [40]. Standard backward trimming processes the clausal proof in reverse, performing RUP checks on active steps and using conflict analysis to mark (activate) the clauses (reasons) that contributed to each conflict (see Example 2); all marked input clauses then constitute the core. Specifically, a RUP check on step \(P_i\) will add all clauses in F and clauses \(P_1, \dots , P_{i-1}\) to the propagation engine, then propagate the units \(\overline{P}_i\) to derive a conflict. Conflict analysis marks reasons for the conflict, where a reason is the clause that propagated a specific unit. Given a conflicting clause C, conflict analysis starts from the list of negated unit literals \(\{\ell _1, \dots , \ell _k\} = C\), then for each \(\ell _i\) in the list the reason clause \(R(\ell _i)\) will be marked and the literals \(R(\ell _i) \setminus \ell _i\) will be added to the unit list. The procedure continues until only unit literals without reasons (unit clauses from the original formula or unit clauses from \(\overline{P}_i\)) remain.

Example 2

Given a formula \(F = C_1: (\overline{x}_1 \vee x_4 \vee x_6) \wedge C_2: (\overline{x}_2 \vee \overline{x}_3) \wedge C_3: (x_1 \vee x_3 \vee x_4) \wedge C_4: (\overline{x}_2 \vee x_7) \wedge C_5: (\overline{x}_2 \vee \overline{x}_4) \), to show that a clause \(D = (\overline{x}_2 \vee x_6)\) is RUP w.r.t. F, we propagate \(F \wedge (x_2 \wedge \overline{x}_6)\).

Propagation derives the corresponding units and corresponding reason clauses:

\((\overline{x}_3,C_2), (x_7,C_4), (\overline{x}_4,C_5), (\overline{x}_1,C_1)\), then \(C_3\) is in conflict.

Analysis of the conflict on \(C_3\) yields reasons \(C_2, C_5, C_1\). Note, \(C_4\) is absent because the unit \(x_7\) is not used to derive the conflict on \(C_3\).

The proof is verified once all marked proof steps have been checked. During each RUP check, core-first propagation can be used to minimize the core by partitioning propagation into two levels: \(Level_1\) (marked core clauses) and \(Level_2\) (unmarked clauses). Initially, \(Level_1\) is empty while \(Level_2\) contains input clauses and proof steps. During a RUP check, the propagation engine alternates between \(Level_1\) and \(Level_2\) as follows. First, propagation is performed on \(Level_1\). If a conflict is derived, conflict analysis proceeds immediately. Otherwise, \(Level_2\) is partially propagated until the first new unit is derived, at which point control returns to \(Level_1\) to propagate that learned unit. During conflict analysis, any reason clauses originating from \(Level_2\) are marked and promoted to \(Level_1\) for subsequent RUP checks. This approach attempts to minimize the number of newly marked clauses in each RUP check, thereby reducing the size of the core.

Theory-last trimming (Algorithm 1) modifies core-first trimming by initializing \(Level_1\) with all input clauses (line 2) and \(Level_2\) with theory lemmas and proof steps (line 3). Consequently, the initial propagations during a RUP check prioritize input clauses (line 9). Only when propagation on \(Level_1\) fails to derive a conflict does propagation proceed on \(Level_2\); thus, theory lemmas are propagated last. The function propagatePartial propagates until a new unit literal is derived, after which control returns to \(Level_1\). Lines \(13-16\) mark reason clauses, and the marked (core) theory lemmas are returned on line 17. Example 3 illustrates theory-last propagation.

The resulting core may be larger because it always contains all input clauses, but it often contains fewer theory lemmas. Theory-last trimming always produces a valid core for a valid RUP proof because the propagation engine still has access to all relevant clauses across \(Level_1\) and \(Level_2\). In the worst case, backward trimming is quadratic in the size of the proof; however, in practice, its runtime is often comparable to the time required to generate the proof.

Algorithm 1
A flowchart diagram showing the SMT solving and proof checking pipeline. On the left, a "Query" feeds into "CVC5," which outputs a "Skeleton" containing Preprocessing, Clausification, and Theory Lemmas. The skeleton is passed to "CARCARA," which checks preprocessing and clausification steps. Upon reaching the prop_unsat step, CARCARA invokes a "Theory Oracle" module below. The oracle has three sub-components arranged horizontally: "Theory Trimming" (which receives the clausified input clauses C1 to Cr and theory lemmas T1 to Tk and produces a trimmed Core with theory lemmas Ti to Tj that are a subset of T), "Theory Justification" (which produces justifications Ji to Jj for the core lemmas), and "Theory Checking." Dashed lines indicate optional paths to "Proof Elaboration," which can produce a "Full Proof" by combining SAT reasoning and justifications produced by the theory oracle with the proof skeleton. The final output is labeled "Verified.".

Theory-Last Trimming

Full size image

Example 3

Given F from Example 2, let \(C_4\) and \(C_5\) be theory lemmas. To show D is RUP, theory-last propagation would proceed as follows:

  1. 1.

    Propagate \(Level_1\): \((C_1, C_2, C_3)\) with units \(x_2 , \overline{x}_6\), giving \((\overline{x}_3,C_2)\).

  2. 2.

    No conflict was derived, so partially propagate \(Level_2\): \((C_4 ,C_5)\) with units \(x_2, \overline{x}_6, \overline{x}_3\) giving \((x_7,C_4)\).

  3. 3.

    Return to \(Level_1\) propagating the new unit \(x_7\).

  4. 4.

    Again, no conflict is derived so partially propagate \(Level_2\), giving \((\overline{x}_4,C_5)\).

  5. 5.

    Return to \(Level_1\) propagating \(\overline{x}_4\) giving \((\overline{x}_1,C_1)\) then a conflict.

  6. 6.

    Analysis gives reasons \(C_2, C_5, C_1\), so theory lemma \(C_5\) would be marked and promoted from \(Level_2\) to \(Level_1\), with \(C_4\) remaining in \(Level_2\).

Iterative Theory Trimming. The theory trimming algorithm does not guarantee optimality; algorithms for finding a minimal core require many calls to a SAT solver, in the worst case removing only one clause from the core at a time. Small reductions to the size of the core provide diminishing returns for theories where theory lemmas are easy to justify. Iterative trimming feeds the output core back into the trimming pipeline as the new input formula, repeating until the number of core theory lemmas stabilizes. Subsequent iterations benefit from fresh SAT proofs and can remove additional theory lemmas, though the first iteration typically achieves the largest reduction. This approach achieves moderate reductions with fewer calls to a SAT solver and trimming tool.

4.2 Theory Lemma Justification and Checking

Each core theory lemma \(l_1\vee \cdots \vee l_n\) is justified by proving the unsatisfiability of \(\lnot l_1\wedge \cdots \wedge \lnot l_n\) via cvc5. The justification is checked with Carcara and optionally returned for proof elaboration. The input to cvc5 is an SMT-LIB query using the original problem’s preamble, which contains the declaration of sorts and functions symbols, along with the assertion that negates the lemma. The query below, for example, would be used to justify theory lemma \(t_7\) from CongEx.

The text asserts that none of the equalities hold: a equals d, a equals b, or b equals d. It then checks the satisfiability of this condition, meaning it tests whether it is possible for all these inequalities to be true at the same time.

Rather than justifying lemmas individually, we can process them in batches, similar to the work on propositional proof skeletons [33]. Given a batch \(T_1, \dots , T_k\), their joint validity is established by proving the unsatisfiability of \(\overline{T}_1 \vee \dots \vee \overline{T}_k\). This is constructed as a single SMT-LIB query with the original problem’s preamble and an assertion forming a disjunction of the negation of the set of theory lemmas, for example:

The expression asserts that at least one of the conditions t sub small 1, t sub small 2, up to t sub small k is true by stating the logical OR of the negations of each condition. This means it checks that not all of these conditions are false simultaneously.

A single Carcara call checks the validity of the entire batch. The batch quality—the difficulty of solving and checking the batch—depends on the number of lemmas in the batch, the relationship between lemmas in the batch, and the underlying theory. Smaller batch sizes can lead to significant overhead when executing cvc5 and Carcara on thousands of trivial queries, but larger batches can grow increasingly more difficult to prove. Through experimentation, a batch size of 50 was found to balance solver overhead against per-batch difficulty. Lemmas are batched in the order they were learned by the SMT solver, keeping related theory lemmas together and enabling the SMT solver to reuse intermediate results.

Batches may be distributed across multiple cores to parallelize justification. However, the effectiveness of parallelization will still depend on the batch quality, as much harder batches can create a bottleneck. While a similar issue is recurring in parallel SMT solving [41], we did not experience this much.

In our evaluation the majority of theory lemmas were justified quickly, motivating the batch size of 50. However, initial experimentation for other theories, including the theory of bitvectors which require more complex justifications, suggest that smaller batch sizes may lead to faster verification.

4.3 Lemmas Containing Fresh Symbols

Preprocessing in quantified logics may introduce fresh symbols via Skolemization, and these symbols can appear in theory lemmas. Therefore when applying the process above to check lemmas with such symbols, the problem’s preamble has to be extended to declare them. This however is not sufficient because the fresh symbol is not unconstrained. For example, in the case of Skolemization, the introduced symbol is a witness for a particular Skolemized quantifier. So these constraints may be required in the query to justify the lemma. This is a general issue that limits e.g. validating Skolemization inferences via external solvers [32, Sec. 1.2].

We can circumvent the problem in our approach because Skolemization in Alethe is justified in an equivalence-preserving way via Hilbert’s choice operator \(\epsilon x.\>\varphi \), which is characterized via the axiom \(\exists x. \varphi [x]\rightarrow \varphi [\epsilon x.\>\varphi ]\), i.e., the operator yields a term that makes its bound formula hold [4]. Therefore, Carcara can use the formulas in the choice operators to constrain the fresh symbols appearing in lemmas. So the validity of a lemma \(L[\epsilon x.\>\varphi ]\) in the Alethe skeleton is justified by proving the unsatisfiability of the SMT formula \((\exists x. \varphi [x]\rightarrow \varphi [k])\wedge \lnot L[k]\), where k is a fresh symbol of the same type of the choice term.

In full generality symbols introduced via Skolemization may depend on other fresh symbols. For example, when Skolemizing \(\exists x_1x_2.\varphi \), first \(\exists x_2.\>\varphi [\epsilon x_1.\> \exists x_2.\>\varphi ]\) is derived, and the Skolemization of \(x_2\) will be defined by a formula containing the choice term for \(x_1\). Checking the validity of lemmas containing such choice terms, i.e., L[k] where k is \(\epsilon x.\>\varphi [\epsilon _1,\dots ,\epsilon _n]\), with \(\epsilon _1,\dots ,\epsilon _n\) being choice terms, requires the constraint to validate L to also characterize k accounting for all possible values that \(\epsilon _1,\dots ,\epsilon _n\) may assume. Thus the formula that we generate for such lemmas is \((\forall y_1\dots y_n.\>\exists x. \varphi [y_1,\dots ,y_n]\rightarrow \varphi [k])\wedge \lnot L[k]\), requiring quantifier reasoning by the backend solver.

Table 1. Solving time comparison on unsatisfiable formulas that cvc5 solves within the timeout (number of formulas shown beneath each theory).
Full size table
Table 2. Solving and checking comparison on formulas with a prop_unsat step. Solving timeouts count towards the checking PAR2. Average lemma count reports core theory lemmas from solved formulas. Best Core is the number of formulas for which a unique configuration among cvc5-pr, d-5, and t-5 found a core with the fewest theory lemmas, with no values reported for t-1 which has at least as many lemmas as t-5 and t-5-S which has exactly as many lemmas as t-5. *cvc5-pr times out on harder QF_LIA instances with many lemmas, making the average incomparable because the number of theory lemmas for unsolved problems are not included. Excluding the 75 cvc5-pr timeouts, t-5 has an average of 599.
Full size table

5 Experimental Evaluation

All experiments were performed in the Pittsburgh Supercomputing Center on nodes with 128 cores and 256 GB RAM [9]. We used a 5, 000 second timeout for solving and a 5, 000 second timeout for proof checking, and 64 experiments were run in parallel per node so each process held approximately 4GB of memory. We report the penalized average runtime (PAR2). PAR2 is the average runtime with a two times penalty for timeouts, e.g., a timeout on 5, 000 seconds is counted as a 10, 000 second runtime.

We considered benchmarks from the 2023 release of the SMT-LIB logics QF_UF, QF_LIA, QF_LRA, and QF_UFLIA , UF, and UFLIA which are representative of the fragment supported by cvc5 ’s Alethe proof production. We exclude benchmarks from the nec-smt family in QF_LIA, for which cvc5 introduces fresh terms during preprocessing in a way not yet supported by the Alethe translation. We first present the results for the quantifier-free logics, and then for quantified logics in Sect. 5.4.

For the evaluation, we first solved each formula using cvc5 without proof production. Unsatisfiable formulas without a timeout were used to compare solving times in Table 1. Next, we further filtered away formulas for which the proof did not include a prop_unsat step, i.e., cvc5 solved them purely via preprocessing. These problems for which trimming can occur were used to compare checking times in Table 2.

While we only consider the UF, LIA, and LRA theories, our approach is theory agnostic and can be readily extended to other theories once an Alethe-producing SMT solver is available for it. Extensions of cvc5 to produce Alethe proofs for example for bitvectors and strings are ongoing work, and we expect the impact of our approach to be significant in these theories, where theory reasoning is more expensive.

We used the following configurations in our main experiments, with all proofs checked by Carcara as described in Sect. 3:

  • cvc5 - Default cvc5 without proof production.

  • cvc5-proof - Default eager proof production in cvc5.

  • cvc5-theory-trim5 - Proof skeleton framework with 5 iterations of theory trimming and lemma justification performed in batches of 50. Summarized as t-5. Optionally, we could use a single trimming iteration (t-1), use a single lemma per batch (t-5-S), or use standard DRAT-trim instead of our theory-trim tool (d-5).

Fig. 2.
Three scatter plots comparing CVC5-PROOF (x-axis) against CVC5-THEORY-TRIM5 (y-axis) on log-log scales, one each for QF\_UF (top left), QF\_LRA (top right), and QF\_LIA (bottom center). Each plot contains three series of points: stars for solving time only, plus signs for solving plus checking time on 1 core, and crosses for solving plus checking time on 8 cores. A diagonal line represents equal performance. Points below the diagonal favor CVC5-THEORY-TRIM5; points above favor CVC5-PROOF. In QF\_UF and QF\_LIA, many solve plus check points fall below the diagonal, particularly at higher runtimes, indicating CVC5-THEORY-TRIM5 with 8 cores is faster. In QF\_LRA, the points are more tightly clustered near the diagonal, indicating more comparable performance.

Scatter plots showing the solving times and the full solving + checking times comparing cvc5-proof with a single core and cvc5-theory-trim5 with (1) or (8) cores. Benchmarks are the filtered set described in the parallel checking evaluation.

Full size image

5.1 Solving Time

Solving results (Table 1) show the expected ordering: cvc5-theory-trim5 is faster on average than cvc5-proof but slower than uninstrumented cvc5. Scatter plots (Fig. 2) show results for a set of hard problems, with the benchmark selection criteria described below in the parallel checking section. The solving benefit is most pronounced on a group of hard problems in QF_LIA where cvc5-proof times out at 5, 000 seconds but cvc5-theory-trim5 solves them in one to two hundred seconds.

5.2 Sequential Checking

Table 2 compares solving times, checking times, and core theory lemma counts for configurations with proof support. For QF_UF and QF_LIA, the combined solving and checking time under cvc5-theory-trim5 is often lower than under cvc5-proof, demonstrating that iterative trimming and batched justification can rival eager proof production while also providing faster solving. Iterative trimming (cvc5-theory-trim5) often produces cores with fewer theory lemmas than non-iterative (t-1) or standard DRAT-trim (d-5), with cvc5-proof cores almost never containing fewer theory lemmas than our configurations. Mean lemma reduction rates with cvc5-theory-trim5 are \(54\%\) (QF_UF), \(18\%\) (QF_LRA), \(21\%\) (QF_LIA), \(39\%\) (QF_UFLIA). On average, between \(30\sim 45\%\) of the propositional formula prior to trimming consists of theory lemmas.

The benefit of iterative trimming varies by theory. In QF_LIA, iterative trimming produces smaller cores yet higher checking times, suggesting the trimming cost exceeds the savings from fewer justifications. In QF_UF, QF_LRA, or QF_UFLIA iterative trimming reduces total checking time. Sequential single lemma elaboration (t-5-S) performs poorly across all theories, underscoring the importance of batching.

5.3 Parallel Checking

We applied parallel batch justification across 8 cores to formulas with at least a 300 seconds checking time and at least 400 core theory lemmas when using the sequential version of cvc5-theory-trim5. We chose the value of 400 so that each core can process at least one batch of size 50. No formula in QF_UFLIA met this criterion.

Table 3. Number of formulas successfully checked for cvc5-pr on a single core, cvc5-theory-trim5 on a single core (1-core) and cvc5-theory-trim5 on 8 cores (8-core), and PAR2 scores for checking time and the speedup on cvc5-theory-trim5.
Full size table

Table 3 shows for both QF_UF and QF_LIA, cvc5-theory-trim5 with 8 cores achieves faster solving-plus-checking than cvc5-proof, in addition to faster sequential solving. For QF_LRA, solving-time gains are moderate, resulting in a combined solving-plus-checking time that is often slightly worse than cvc5-proof. Note, there is no implementation for parallelizing Carcara without our proof skeleton framework, so the cvc5-proof configuration can only be run on a single core. These results highlight the benefit of skeleton checking on difficult problems containing many theory lemmas for which proof logging is computationally expensive.

5.4 Theories with Quantifiers

Results for UF and UFLIA are summarized in Table 4. The large difference in checking PAR2 is mostly due to timeouts. As discussed in Sect. 4.2, in quantified logics, justifying some lemmas may require solving quantified problems, and SMT solvers are well known to be incomplete and unstable in quantified logics [42]. So unfortunately timeouts in lemma checking with cvc5 can be expected.

Furthermore, there is less gain in the solving time, or no gain. This is explained by theory reasoning for quantified lemmas in SMT being done mostly via instantiation [34], for which the overhead of proof production is minimal (how the instance was found is irrelevant; only that it is a sound instantiation needs to be justified). Moreover, SMT solvers, and cvc5 is no different, generate instances mostly in a non-goal oriented way, i.e., they are not derived to refine the search directly, but rather on the expectation that they may be useful. As a result, solvers generate very large numbers of useless instances, which in our approach are all logged in the skeleton, and this overhead may be one reason our solving is often slightly slower than cvc5-pr. Finally, we observe that problems in UF/UFLIA mostly do not have as deep a ground structure as problems in the quantifier-free logics, and with less ground reasoning less overhead is added by producing proofs, which we would have saved.

Table 4. Timeouts, PAR2 scores, and number of core lemmas for quantified theories UF and UFLIA comparing cvc5, cvc5-pr, and t-5. Description of PAR2, Avg. Lemmas, and Best Core found in caption of Table 2.
Full size table

6 Related Work

Several works have used clausal proofs for SMT with varying success [14, 31]. The work on the extended DRAT (e DRAT) proof system [18] most closely relates to our work. They modified cvc5 to produce e DRAT proofs for QF_UF and QF_LRA consisting of the SAT proof steps as well as unjustified theory lemma steps. Then, after trimming the SAT proof with DRAT-trim, their VALIDO toolchain elaborated proof steps and checked them with theory-specific RUST and Lean [26] tools respectively. One key difference is that we leverage existing tools, avoiding the cost of developing theory-specific elaborators and checkers. This also allows us to support preprocessing proofs, a crucial component missing in e DRAT. Next, we focus on iterative proof trimming using our modified DRAT-trim with theory-last propagation. Finally, our relaxed approach with batch justification facilitates parallelization in checking. The VALIDO toolchain is not open source so we cannot compare our tools directly.

Proof skeleton frameworks have also been explored in other domains including constraint programming [16], with the focus of reducing proof logging overhead during solving.

Core extraction has also been explored in the context of SMT, with early ideas stemming from work on lemma-lifting [10]. Notably, these approaches use off-the-shelf core extractors, whereas our approach attempts to minimize theory lemmas in the core.

7 Conclusion and Future Work

We presented a general approach for producing and checking SMT proof skeletons. External SAT reasoning enables improved theory trimming, and batched parallel theory justification improves runtimes on quantifier-free logics. This framework requires only that an SMT solver logs preprocessing and clausification proofs together with theory lemma holes, making it accessible to solvers beyond cvc5 that lack full proof support.

Future work will explore harder theories including bit-vectors and mechanisms for incorporating preprocessing steps into the trimming and skeleton checking procedures. In addition, the skeleton format may be extended to support partial or fully justified theory lemmas when including such information does not compromise solver runtime.