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

1. Problem Statement

In Satisfiability Modulo Theories (SMT), lifting Boolean reasoning techniques often requires generating theory lemmas (T-lemmas). These are T-valid clauses that rule out truth assignments which are propositionally satisfying but T-inconsistent.

While standard SMT solving generates these lemmas "lazily" on demand during the search, certain complex SMT tasks—such as minimal unsat-core extraction, MaxSMT, and the compilation of T-OBDDs or T-SDDs—require the "eager" pre-computation of a complete set of T-lemmas upfront.

Existing "classic" eager SMT encodings are insufficient for this purpose because:

1. They are specific to a few simple theories (e.g., EUF, DL, LRA).
2. They do not comply with theory combination.
3. They often produce excessive numbers of unnecessary lemmas.

Currently, there is a lack of theory-agnostic methods to efficiently enumerate complete sets of T-lemmas for arbitrary formulas, particularly for Knowledge Compilation (KC) applications where computational overhead is pushed into an offline phase to enable polynomial-time online queries.

2. Methodology

The authors propose a framework for enumerating T-lemmas that is agnostic to the underlying theory. The approach builds upon a baseline method using AllSMT (enumerating all T-satisfiable assignments) and introduces three orthogonal, composable improvements to enhance scalability:

2.1 Baseline: Total AllSMT Enumeration

The baseline method (Algorithm 2) performs a total, non-projected AllSMT enumeration on the input formula $\phi[\alpha]$. It iteratively finds T-satisfiable total truth assignments, blocks them, and collects T-lemmas learned by the solver until the formula becomes unsatisfiable.

• Limitation: This approach relies on enumerating total assignments. As demonstrated in Example 2, naive partial enumeration can fail to generate necessary T-lemmas because the solver may never explore the specific T-inconsistent total assignment that triggers a conflict. However, enumerating all total assignments is often computationally intractable due to combinatorial explosion.

2.2 Improvement 1: Divide-and-Conquer (D&C)

To mitigate the cost of total enumeration, the authors propose a Divide-and-Conquer strategy (Algorithm 3):

1. Perform a partial AllSMT enumeration to decompose the Boolean search space into a set of disjoint, T-satisfiable partial assignments ($M_{\alpha}^p$).
2. For each partial assignment $\mu \in M_{\alpha}^p$, perform a total AllSMT enumeration on the restricted formula $\phi \land \mu$.
3. The total enumerations are executed in parallel.

• Rationale: This transforms one large, intractable total enumeration into one cheaper decomposition step plus many smaller, manageable total enumerations.

2.3 Improvement 2: Projected Enumeration

The authors observe that T-inconsistency is determined exclusively by the assignment to Theory atoms ($\alpha_T$), not Boolean atoms ($\alpha_B$).

• Method: Perform AllSMT enumeration projected only onto $\alpha_T$ (Algorithm 4).
• Theoretical Basis: Theorem 1 proves that projecting the enumeration onto T-atoms yields a complete set of T-lemmas.
• Benefit: This drastically reduces the search dimension. A single T-satisfiable assignment on $\alpha_T$ represents up to $2^k$ total assignments on the full set of atoms (where $k$ is the number of Boolean atoms), significantly reducing memory usage and blocking clause size.

2.4 Improvement 3: Theory-Driven Partitioning

If the set of atoms in $\phi$ can be partitioned into disjoint sets ($\alpha_1, \dots, \alpha_n$) such that no atom in one set shares variables or uninterpreted symbols with atoms in another, the problem can be decomposed further (Algorithm 5).

• Method: Based on Property 1 and Theorem 2, T-lemmas can be enumerated independently for each partition. The algorithm iteratively partitions atoms, enumerates lemmas for each partition projected onto that partition's atoms, and accumulates the results.
• Benefit: This allows the decomposition of a single total enumeration into $n$ independent projected enumerations, offering potential exponential speedups for problems with disjoint components.

3. Key Contributions

1. Theory-Agnostic Framework: The first explicit presentation of methods to enumerate complete sets of T-lemmas for arbitrary theories, moving beyond theory-specific eager encodings.
2. Scalability Techniques: The introduction of three orthogonal techniques:
   • Divide-and-Conquer: Parallelizes the search by decomposing the Boolean space.
   • Projected Enumeration: Reduces search dimensionality by focusing on T-atoms.
   • Partitioning: Exploits structural disjointness in the formula to solve subproblems independently.
3. Theoretical Guarantees: Formal proofs (Theorems 1 and 2) demonstrating that these optimizations preserve the completeness of the T-lemma set required to rule out all T-inconsistent assignments.
4. Integration with Knowledge Compilation: The work serves as an enabling technique for lifting Knowledge Compilation methods (specifically Decision Diagrams like OBDDs and SDDs) to the SMT level, addressing the previous bottleneck of T-lemma enumeration.

4. Experimental Results

The techniques were evaluated on two benchmark sets:

• Synthetic SMT(LRA) instances: 450 randomly generated problems from [16].
• Temporal Planning instances: 90 SMT encodings of "Painter" domain planning problems.

Performance Metrics:

• Time Efficiency:
  • On synthetic benchmarks, D&C improved performance by up to 2 orders of magnitude over the baseline, solving 17 more problems within the timeout.
  • Adding Projection further improved results, solving 30 more problems than D&C alone and drastically reducing time for previously solved instances.
  • Partitioning showed no improvement on synthetic data (as few problems had disjoint partitions) but was highly effective on planning problems.
  • On planning problems, Partitioning was the dominant factor, enabling the solution of problems with horizon 5 that were previously intractable, achieving speedups of several orders of magnitude.
• Number of Lemmas:
  • D&C tended to produce slightly more lemmas due to parallel redundancy.
  • Projection and Partitioning generally reduced the number of enumerated lemmas by mitigating redundant exploration and generating stronger, smaller lemmas.
• Lemma Size:
  • Partitioning on planning problems resulted in significantly smaller (fewer literals) T-lemmas, likely due to early pruning of T-inconsistent branches involving only specific partitions.

5. Significance and Claims

The paper claims that these techniques drastically enhance the efficiency and scalability of T-lemma enumeration compared to the baseline AllSMT approach.

• Enabling Role: The primary significance is enabling the practical application of Knowledge Compilation to SMT. The authors note that in their previous work [16], T-lemma enumeration was the "main bottleneck" for compiling Decision Diagrams. By resolving this bottleneck, the proposed methods pave the way for scaling these compilation techniques to complex, real-world instances.
• Modesty: The authors are careful to note that improvements are context-dependent. For instance, projection did not help with planning problems because the T-atom assignments were deterministic consequences of Boolean assignments in those specific encodings. Similarly, partitioning only yielded benefits when the problem structure naturally allowed for disjoint partitions.

In summary, the paper provides a robust, theory-agnostic toolkit for eager T-lemma enumeration, transforming a previously intractable step into a scalable process, thereby facilitating advanced SMT applications like MaxSMT and Knowledge Compilation.