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

TL;DR

This paper introduces theory-agnostic, scalable methods for enumerating complete sets of theory lemmas in SMT solving, improving efficiency and scalability over traditional approaches.

Contribution

It presents novel, parallelizable lemma-enumeration techniques that are agnostic to specific theories, enhancing SMT solving capabilities for complex instances.

Findings

Significant efficiency improvements demonstrated in experiments.

Techniques enable scaling to more complex SMT instances.

Parallelizable methods outperform traditional approaches.

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.