Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Combining Combination Properties: Minimal Models

Guilherme Vicentin de Toledo, Yoni Zohar

TL;DR

The paper completes a long-running program in SMT theory combination by examining the computability of minimal-model cardinalities, a key ingredient in shininess, and by fully characterizing how this property interacts with the established suite of combination properties. It formalizes minmod as a computable function from quantifier-free formulas to finite sets of cardinalities and proves core links to finite model properties and finiteness notions via general and empty-signature results. The authors extend prior work with new Busy Beaver-based theories and introduce a non-computable function to realize remaining combinations, while also providing a taxonomy of possible and impossible property com-binations (excluding unicorns). They show that many combinations are constrained by computability and finiteness interactions, yielding a practical guide for SMT solvers and theory architects. The work paves the way for further automation and exploration of additional properties and signature configurations in the theory-combination landscape.

Abstract

This is a part of an ongoing research project, with the aim of finding the connections between properties related to theory combination in Satisfiability Modulo Theories. In previous work, 7 properties were analyzed: convexity, stable infiniteness, smoothness, finite witnessability, strong finite witnessability, the finite model property, and stable finiteness. The first two properties are related to Nelson-Oppen combination, the third and fourth to polite combination, the fifth to strong politeness, and the last two to shininess. However, the remaining key property of shiny theories, namely, the ability to compute the cardinalities of minimal models, was not yet analyzed. In this paper we study this property and its connection to the others.

Combining Combination Properties: Minimal Models

TL;DR

The paper completes a long-running program in SMT theory combination by examining the computability of minimal-model cardinalities, a key ingredient in shininess, and by fully characterizing how this property interacts with the established suite of combination properties. It formalizes minmod as a computable function from quantifier-free formulas to finite sets of cardinalities and proves core links to finite model properties and finiteness notions via general and empty-signature results. The authors extend prior work with new Busy Beaver-based theories and introduce a non-computable function to realize remaining combinations, while also providing a taxonomy of possible and impossible property com-binations (excluding unicorns). They show that many combinations are constrained by computability and finiteness interactions, yielding a practical guide for SMT solvers and theory architects. The work paves the way for further automation and exploration of additional properties and signature configurations in the theory-combination landscape.

Abstract

This is a part of an ongoing research project, with the aim of finding the connections between properties related to theory combination in Satisfiability Modulo Theories. In previous work, 7 properties were analyzed: convexity, stable infiniteness, smoothness, finite witnessability, strong finite witnessability, the finite model property, and stable finiteness. The first two properties are related to Nelson-Oppen combination, the third and fourth to polite combination, the fifth to strong politeness, and the last two to shininess. However, the remaining key property of shiny theories, namely, the ability to compute the cardinalities of minimal models, was not yet analyzed. In this paper we study this property and its connection to the others.
Paper Structure (66 sections, 168 theorems, 121 equations, 4 figures, 3 tables)

This paper contains 66 sections, 168 theorems, 121 equations, 4 figures, 3 tables.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. First-Order Many-Sorted Logic
  4. Theory Combination Properties
  5. On Minimal Models
  6. The Main Theorem
  7. Proof of \ref{['mainresult']}: The Impossible Cases
  8. General Signatures
  9. Empty Signatures
  10. Summary
  11. Proof of \ref{['mainresult']}: The Possible Cases
  12. Existing Theories
  13. New Theories
  14. New Theories With the Busy Beaver Function
  15. Theories With a new Non-Computable Function
  16. ...and 51 more sections

Key Result

Theorem 1

Let $\Sigma$ be a first-order, many-sorted signature; if a set of $\Sigma$-formulas $\Gamma$ is satisfiable, then there exists an interpretation $\mathcal{A}$ that satisfies $\Gamma$ where $|\sigma^{\mathcal{A}}|\leq\aleph_{0}$ for all $\sigma\in\mathcal{S}_{\Sigma}$.

Figures (4)

  • Figure 1: Cardinality formulas. All of $x_{i}$, and $y$ are of sort $\sigma$.
  • Figure 2: Venn diagrams for \ref{['CMMF+FM=>FW', 'SM+ES=>CMMF', '-SI+ES=>CMMF', 'CV+-SI+-FMP+-CMMF', '-FMP+ES+OS=>CMMF']}
  • Figure 3: Special formulas: $k\in\mathbb{N}\setminus\{0\}$, $x$ is of sort $\sigma_{1}$, and $s^{k}(x)$ is defined by $s^{1}(x)=s(x)$ and $s^{k+1}(x)=s(s^{k}(x))$. We denote $\psi_{=}^{1}$ by $\psi_{=}$, and $\psi_{\vee}^{1}$ by $\psi_{\vee}$.
  • Figure 4: Possible scenarios when $\psi_{\neq}\wedge\psi_{\vee}^{2}$ holds

Theorems & Definitions (337)

  • Theorem 1
  • Theorem 2
  • Lemma 1
  • Proposition 1
  • Proposition 2
  • Proposition 3
  • Definition 4.1
  • Conjecture 1
  • Theorem 3
  • Theorem 4
  • ...and 327 more