pith. sign in

arxiv: 2602.14634 · v2 · pith:LD5MJUVSnew · submitted 2026-02-16 · 💻 cs.LO

Beyond Eager Encodings: A Theory-Agnostic Approach to Theory-Lemma Enumeration in SMT

Emanuele Civini , Gabriele Masina , Giuseppe Spallitta , Roberto Sebastiani This is my paper

Pith reviewed 2026-05-25 06:51 UTC · model grok-4.3

classification 💻 cs.LO
keywords SMTtheory lemmaseager encodingsAllSMTlemma enumerationdivide and conquertheory-agnostic methodsparallel enumeration
0
0 comments X

The pith

Theory-agnostic methods enumerate complete sets of theory lemmas for any SMT formula using divide-and-conquer and partitioning techniques.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper establishes that starting from AllSMT, improved techniques including divide-and-conquer, projected enumeration, and theory-driven partitioning can produce complete, formula-tailored sets of theory lemmas without depending on particular theories. This approach addresses the limits of classic eager encodings, which apply only to a few easy theories, ignore theory combinations, and often generate many unneeded lemmas. The methods are designed to be highly parallelizable. A sympathetic reader would care because many SMT tasks such as unsat-core extraction, MaxSMT, and T-OBDD or T-SDD compilation require all relevant lemmas upfront rather than on demand during search. Experiments show these techniques raise efficiency enough to handle substantially more complex instances.

Core claim

The paper claims that theory-agnostic lemma-enumeration methods, built on an AllSMT baseline and augmented with divide-and-conquer, projected enumeration, and theory-driven partitioning, generate complete sets of theory lemmas tailored to a given formula, remain compatible with theory combination, avoid the restrictions and overhead of classic eager encodings, and deliver major scalability gains through parallelization, as confirmed by experimental results on harder problems.

What carries the argument

Theory-agnostic lemma enumeration via divide-and-conquer, projected enumeration, and theory-driven partitioning that extends the AllSMT baseline to produce complete, formula-specific lemma sets.

If this is right

  • Pre-computation of all needed theory lemmas becomes feasible for SMT tasks that require eager rather than lazy generation.
  • Theory combinations can be handled uniformly without custom encodings for each theory.
  • Parallel execution of the enumeration steps yields substantial runtime reductions on large instances.
  • SMT solvers gain the ability to scale unsat-core extraction, MaxSMT, and compilation tasks to formulas previously out of reach.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same partitioning ideas could be reused inside lazy SMT solvers to accelerate on-demand lemma generation.
  • Formula-tailored lemma sets might reduce memory pressure in decision procedures that currently store all possible lemmas.
  • The approach opens a route to hybrid eager-lazy pipelines where only the relevant lemma subset is materialized.

Load-bearing premise

The new enumeration techniques stay complete and efficient on arbitrary theory combinations without needing theory-specific knowledge or creating excessive overhead.

What would settle it

A concrete counter-example would be a combined-theory formula on which the methods either miss some theory lemmas required for correctness or require more time and lemmas than a standard eager encoding.

Figures

Figures reproduced from arXiv: 2602.14634 by Emanuele Civini, Gabriele Masina, Giuseppe Spallitta, Roberto Sebastiani.

Figure 1
Figure 1. Figure 1: Time taken to enumerate T -lemmas with different methods on problems from [15]. (Notice that in the cactus plot the green line (D&C+Proj.) and the red line (D&C+Proj.+Part.) are almost indistinguishable.) Benchmarks. We considered two sets of benchmarks. The first set consists of all the 450 SMT(LRA) synthetic instances from [15]. These problems were generated randomly by nesting Boolean operators up to a … view at source ↗
Figure 2
Figure 2. Figure 2: Time taken to enumerate T -lemmas with different methods on planning prob￾lems. which solves 30 more problems within the timeout and drastically reduces the time required to enumerate T -lemmas for other problems already solved by D&C. Notably, the introduction of partitioning does not yield any improvement. This is because only 92 of 450 problems have at least two partitions. The hardest of these problems… view at source ↗
Figure 3
Figure 3. Figure 3: Number of T -lemmas enumerated by different strategies on problems from [15]. 10 0 10 1 10 2 10 3 Baseline 10 0 10 1 10 2 10 3 D&C 10 0 10 1 10 2 10 3 10 4 10 5 D&C 10 0 10 1 10 2 10 3 10 4 10 5 D&C+Proj 10 0 10 1 10 2 10 3 10 4 D&C+Proj 10 0 10 1 10 2 10 3 10 4 D&C+Proj+Part 10 0 10 1 10 2 10 3 Baseline 10 0 10 1 10 2 10 3 D&C+Proj+Part [PITH_FULL_IMAGE:figures/full_fig_p014_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Number of T -lemmas enumerated by different strategies on planning problems. remark that we only show points for problems solved by both the compared strategies, so that in temporal planning problems, we only have a limited number of points. Overall, we note that there is no large difference in the number of enumerated T - lemmas between the different strategies. We can, however, observe some trends. First… view at source ↗
Figure 5
Figure 5. Figure 5: Median size of the T -lemmas found by different methods on problems from [15]. 1 2 3 4 5 6 7 8 Baseline 1 2 3 4 5 6 7 8 D&C 5 10 15 20 25 30 35 40 D&C 5 10 15 20 25 30 35 40 D&C+Proj 5 10 15 20 25 30 35 40 D&C+Proj 5 10 15 20 25 30 35 40 D&C+Proj+Part 1 2 3 4 Baseline 1 2 3 4 D&C+Proj+Part [PITH_FULL_IMAGE:figures/full_fig_p015_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Median size of the T -lemmas found by different methods on planning problems. We observe that different techniques do not consistently improve or worsen the size of T -lemmas, with a notable exception for partitioning, which, on planning problems, allows for finding much smaller T -lemmas. We conjecture that this may be due to the fact that, with projected enumeration, the literal selection heuristics of t… view at source ↗
read the original abstract

Lifting Boolean-reasoning techniques to the SMT level most often requires producing theory lemmas that rule out theory-inconsistent truth assignments. With standard SMT solving, it is common to "lazily" generate such lemmas on demand during the search; with some harder SMT-level tasks -- such as unsat-core extraction, MaxSMT, T-OBDD or T-SDD compilation -- it may be beneficial or even necessary to "eagerly" pre-compute all the needed theory lemmas upfront. Whereas in principle "classic" eager SMT encodings could do the job, they are specific for very few and easy theories, they do not comply with theory combination, and may produce lots of unnecessary lemmas. In this paper, we present theory-agnostic methods for enumerating complete sets of theory lemmas tailored to a given formula. Starting from AllSMT as a baseline approach, we propose improved lemma-enumeration techniques, including divide&conquer, projected enumeration, and theory-driven partitioning, which are highly parallelizable and which may drastically improve scalability. An experimental evaluation demonstrates that these techniques significantly enhance efficiency and enable the method to scale to substantially more complex instances.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 1 minor

Summary. The manuscript proposes theory-agnostic methods for enumerating complete sets of theory lemmas tailored to a given SMT formula. Starting from the AllSMT baseline, it introduces divide-and-conquer, projected enumeration, and theory-driven partitioning techniques claimed to be highly parallelizable. These are positioned as improvements over classic eager encodings, which are theory-specific, incompatible with theory combination, and prone to generating unnecessary lemmas. The paper asserts that an experimental evaluation demonstrates significant efficiency gains and the ability to scale to substantially more complex instances, with applications to tasks such as unsat-core extraction, MaxSMT, and T-OBDD/T-SDD compilation.

Significance. If the completeness and efficiency claims hold for arbitrary theory combinations, the work could provide a general, reusable framework for eager lemma generation that avoids the limitations of theory-specific encodings. The emphasis on parallelizability is a concrete strength that could translate to practical scalability improvements on modern hardware. The approach addresses a genuine gap between lazy SMT solving and the needs of certain higher-level SMT tasks.

major comments (2)
  1. [Experimental Evaluation] Experimental Evaluation section: The central claim that the techniques 'significantly enhance efficiency' and 'enable the method to scale to substantially more complex instances' rests on experimental results, yet the manuscript supplies insufficient detail on benchmark instances, implementation of the proposed algorithms, exact baselines (including AllSMT variants), runtime distributions, or statistical controls. This prevents verification of the absence of post-hoc selection or missing comparisons and is load-bearing for the scalability assertion.
  2. [Techniques description (divide-and-conquer, theory-driven partitioning)] Sections describing the divide-and-conquer and theory-driven partitioning techniques: The manuscript asserts that these methods remain complete and theory-agnostic for arbitrary theory combinations without excessive overhead or hidden theory-specific oracles. No explicit completeness argument, invariant, or reduction to the AllSMT baseline is provided that would cover combined theories; this assumption is load-bearing for the theory-agnostic claim.
minor comments (1)
  1. [Abstract / Introduction] The abstract and introduction could more explicitly state the precise relationship between the new techniques and the AllSMT baseline (e.g., whether they are strict refinements or orthogonal).

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive feedback on our manuscript. The comments highlight important areas for strengthening the presentation of experimental results and formal arguments. We address each major comment below and commit to revisions that enhance clarity and verifiability without altering the core contributions.

read point-by-point responses

  1. Referee: [Experimental Evaluation] Experimental Evaluation section: The central claim that the techniques 'significantly enhance efficiency' and 'enable the method to scale to substantially more complex instances' rests on experimental results, yet the manuscript supplies insufficient detail on benchmark instances, implementation of the proposed algorithms, exact baselines (including AllSMT variants), runtime distributions, or statistical controls. This prevents verification of the absence of post-hoc selection or missing comparisons and is load-bearing for the scalability assertion.

    Authors: We agree that the current Experimental Evaluation section lacks sufficient detail to allow full independent verification. In the revised manuscript we will expand this section to include: (i) explicit descriptions and sources of all benchmark instances, (ii) implementation details of the divide-and-conquer, projected enumeration, and theory-driven partitioning algorithms (including pseudocode or high-level code structure), (iii) precise definitions of the AllSMT baseline variants used for comparison, (iv) runtime distributions (e.g., via box plots or cumulative distribution functions), and (v) any statistical controls or significance tests applied. These additions will directly address concerns about post-hoc selection and missing comparisons. revision: yes

  2. Referee: [Techniques description (divide-and-conquer, theory-driven partitioning)] Sections describing the divide-and-conquer and theory-driven partitioning techniques: The manuscript asserts that these methods remain complete and theory-agnostic for arbitrary theory combinations without excessive overhead or hidden theory-specific oracles. No explicit completeness argument, invariant, or reduction to the AllSMT baseline is provided that would cover combined theories; this assumption is load-bearing for the theory-agnostic claim.

    Authors: The techniques are presented as conservative extensions of the AllSMT baseline that preserve completeness through exhaustive subspace or projection enumeration. Nevertheless, we acknowledge that an explicit, self-contained completeness argument (including invariants and reduction steps that apply to combined theories) is not currently stated at the level of detail the referee requests. We will add a dedicated subsection (or appendix) in the revised manuscript that supplies a formal completeness proof by reduction to AllSMT, covering arbitrary theory combinations and confirming the absence of hidden theory-specific oracles. revision: yes

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper describes algorithmic techniques for enumerating theory lemmas (divide-and-conquer, projected enumeration, theory-driven partitioning) that start from the AllSMT baseline and add parallelizable refinements. No equations, fitted parameters, predictions, or self-citations appear in a load-bearing role; the central claims concern completeness and scalability of the described procedures, which are presented directly without reduction to their own inputs by construction.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The approach rests on standard properties of SMT theory solvers and the completeness of AllSMT enumeration; no free parameters, new entities, or ad-hoc axioms are introduced in the abstract.

axioms (1)
  • domain assumption Theory solvers exist that can decide consistency of assignments for the theories under consideration
    The enumeration methods presuppose the availability of such oracles to generate lemmas.

pith-pipeline@v0.9.0 · 5748 in / 1201 out tokens · 37478 ms · 2026-05-25T06:51:48.214186+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. d-DNNF Modulo Theories: A General Framework for Polytime SMT Queries

    cs.LO 2026-03 unverdicted novelty 7.0

    A general technique is presented for compiling SMT formulas into d-DNNF by incorporating pre-computed theory lemmas, enabling polytime SMT queries using standard propositional d-DNNF reasoners.

Reference graph

Works this paper leans on

23 extracted references · 23 canonical work pages · cited by 1 Pith paper

  1. [1]

    In: Handbook of Satisfiability, FAIA, vol

    Barrett, C., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability Modulo Theories. In: Handbook of Satisfiability, FAIA, vol. 336, pp. 1267–1329. IOS Press, 2 edn. (2021). https://doi.org/10.3233/FAIA201017

    work page doi:10.3233/faia201017 2021

  2. [2]

    IEEE Trans ComputC-35(8), 677–691 (1986)

    Bryant, R.E.: Graph-Based Algorithms for Boolean Function Manipulation. IEEE Trans ComputC-35(8), 677–691 (1986). https://doi.org/10.1109/TC.1986.1676819

    work page doi:10.1109/tc.1986.1676819 1986

  3. [3]

    J Artif Intell Res40, 701–728 (2011)

    Cimatti, A., Griggio, A., Sebastiani, R.: Computing Small Unsatisfiable Cores in Satisfiabil- ity Modulo Theories. J Artif Intell Res40, 701–728 (2011). https://doi.org/10.1613/jair.3196

    work page doi:10.1613/jair.3196 2011

  4. [4]

    In: TACAS 2013

    Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT Solver. In: TACAS 2013. pp. 93–107. LNCS, Springer (2013). https://doi.org/10.1007/ 978-3-642-36742-7_7

    work page 2013

  5. [5]

    In: SAT 2013

    Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: A Modular Approach to MaxSAT Modulo Theories. In: SAT 2013. pp. 150–165. LNCS, Springer (2013). https://doi.org/10. 1007/978-3-642-39071-5_12

    work page 2013

  6. [6]

    In: IJCAI 2011

    Darwiche, A.: SDD: A New Canonical Representation of Propositional Knowledge Bases. In: IJCAI 2011. vol. 2, pp. 819–826. AAAI Press (2011). https://doi.org/10.5591/ 978-1-57735-516-8/IJCAI11-143

    work page 2011

  7. [7]

    J Artif Intell Res17(1), 229–264 (2002)

    Darwiche, A., Marquis, P.: A knowledge compilation map. J Artif Intell Res17(1), 229–264 (2002). https://doi.org/10.1613/jair.989

    work page doi:10.1613/jair.989 2002

  8. [8]

    In: IJCAR 2018

    Fazekas, K., Bacchus, F., Biere, A.: Implicit Hitting Set Algorithms for Maximum Satisfia- bility Modulo Theories. In: IJCAR 2018. LNCS, vol. 10900, pp. 134–151. Springer (2018). https://doi.org/10.1007/978-3-319-94205-6_10

    work page doi:10.1007/978-3-319-94205-6_10 2018

  9. [9]

    In: SAT 2024

    Fried, D., Nadel, A., Sebastiani, R., Shalmon, Y .: Entailing Generalization Boosts Enumer- ation. In: SAT 2024. LIPIcs, vol. 305, pp. 13:1–13:14. LZI (2024). https://doi.org/10.4230/ LIPIcs.SAT.2024.13

    work page 2024

  10. [10]

    In: SMT Workshop 2015 (2015), https://github.com/pysmt/pysmt

    Gario, M., Micheli, A.: PySMT: A solver-agnostic library for fast prototyping of SMT-based algorithms. In: SMT Workshop 2015 (2015), https://github.com/pysmt/pysmt

    work page 2015

  11. [11]

    In: FMCAD 2016

    Guthmann, O., Strichman, O., Trostanetski, A.: Minimal unsatisfiable core extraction for SMT. In: FMCAD 2016. pp. 57–64 (2016). https://doi.org/10.1109/FMCAD.2016.7886661

    work page doi:10.1109/fmcad.2016.7886661 2016

  12. [12]

    In: HVC 2009

    Heule, M.J.H., Kullmann, O., Wieringa, S., Biere, A.: Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads. In: HVC 2009. pp. 50–65. Springer (2012). https://doi.org/10. 1007/978-3-642-34188-5_8

    work page 2009

  13. [13]

    In: CA V 2006

    Lahiri, S.K., Nieuwenhuis, R., Oliveras, A.: SMT Techniques for Fast Predicate Abstraction. In: CA V 2006. pp. 424–437. LNCS, Springer (2006). https://doi.org/10.1007/11817963_39

    work page doi:10.1007/11817963_39 2006

  14. [14]

    J Artif Intell Res83(2025)

    Masina, G., Spallitta, G., Sebastiani, R.: On CNF Conversion for SAT and SMT Enumera- tion. J Artif Intell Res83(2025). https://doi.org/10.1613/jair.1.16870

    work page doi:10.1613/jair.1.16870 2025

  15. [15]

    In: (ECAI) 2024

    Michelutti, M., Masina, G., Spallitta, G., Sebastiani, R.: Canonical Decision Diagrams Modulo Theories. In: (ECAI) 2024. FAIA, vol. 392, pp. 4319–4327. IOS Press (2024). https://doi.org/10.3233/FAIA241007

    work page doi:10.3233/faia241007 2024

  16. [16]

    AAAI 202337(10), 12095–12102 (2023)

    Panjkovic, S., Micheli, A.: Expressive Optimal Temporal Planning via Optimization Mod- ulo Theory. AAAI 202337(10), 12095–12102 (2023). https://doi.org/10.1609/aaai.v37i10. 26426

    work page doi:10.1609/aaai.v37i10 2023

  17. [17]

    Artif Intell345, 104346 (2025)

    Spallitta, G., Sebastiani, R., Biere, A.: Disjoint projected enumeration for SAT and SMT without blocking clauses. Artif Intell345, 104346 (2025). https://doi.org/10.1016/j.artint. 2025.104346

    work page doi:10.1016/j.artint 2025

  18. [18]

    In: FMCAD 2002

    Strichman, O.: On Solving Presburger and Linear Arithmetic with SAT. In: FMCAD 2002. pp. 160–170. Springer (2002). https://doi.org/10.1007/3-540-36126-X_10

    work page doi:10.1007/3-540-36126-x_10 2002

  19. [19]

    In: CA V

    Strichman, O., Seshia, S.A., Bryant, R.E.: Deciding Separation Formulas with SAT. In: CA V

    work page

  20. [20]

    pp. 209–222. Springer (2002). https://doi.org/10.1007/3-540-45657-0_16 18 E. Civini et al

    work page doi:10.1007/3-540-45657-0_16 2002

  21. [21]

    In: AAAI

    Valentini, A., Micheli, A., Cimatti, A.: Temporal Planning with Intermediate Conditions and Effects. In: AAAI. vol. 34, pp. 9975–9982 (2020). https://doi.org/10.1609/aaai.v34i06.6553

    work page doi:10.1609/aaai.v34i06.6553 2020

  22. [22]

    226–231 (2001)

    Velev, M.N., Bryant, R.E.: Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW pp. 226–231 (2001). https://doi.org/10.1145/378239. 378469

    work page doi:10.1145/378239 2001

  23. [23]

    Xu, Z., Yin, M., Lagniez, J.M.: An Embarrassingly Parallel Model Counter. In: KR. vol. 22, pp. 670–681 (2025). https://doi.org/10.24963/kr.2025/65

    work page doi:10.24963/kr.2025/65 2025