Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Number theory combination: natural density and SMT

Guilherme V. Toledo, Yoni Zohar

TL;DR

This work introduces natural density $\mu(\mathcal{T})$ of a theory's spectrum $Spec(\mathcal{T})$ (the finite model sizes) as a tool to analyze theory combination in Satisfiability Modulo Theories (SMT). It develops both sufficient and necessary conditions linking $\mu(\mathcal{T})$ to key model-theoretic properties such as stable infiniteness, the finite model property, and (strong) finite witnessability, and extends these insights to non-empty and many-sorted signatures. The authors provide concrete constructions showing that every density in $[0,1]$ can be realized under various conditions, and they establish computability relations between spectra, minimal model functions, and densities. This density-based framework yields new, quantitative tests for the feasibility of combining theories in SMT and reveals deep connections between SMT theory combination and number theory, with potential practical benefits for decision procedures and solver design.

Abstract

The study of theory combination in Satisfiability Modulo Theories (SMT) involves various model theoretic properties (e.g., stable infiniteness, smoothness, etc.). We show that such properties can be partly captured by the natural density of the spectrum of the studied theories, which is the set of sizes of their finite models. This enriches the toolbox of the theory combination researcher, by providing new tools to determine the possibility of combining theories. It also reveals interesting and surprising connections between theory combination and number theory.

Number theory combination: natural density and SMT

TL;DR

This work introduces natural density of a theory's spectrum (the finite model sizes) as a tool to analyze theory combination in Satisfiability Modulo Theories (SMT). It develops both sufficient and necessary conditions linking to key model-theoretic properties such as stable infiniteness, the finite model property, and (strong) finite witnessability, and extends these insights to non-empty and many-sorted signatures. The authors provide concrete constructions showing that every density in can be realized under various conditions, and they establish computability relations between spectra, minimal model functions, and densities. This density-based framework yields new, quantitative tests for the feasibility of combining theories in SMT and reveals deep connections between SMT theory combination and number theory, with potential practical benefits for decision procedures and solver design.

Abstract

The study of theory combination in Satisfiability Modulo Theories (SMT) involves various model theoretic properties (e.g., stable infiniteness, smoothness, etc.). We show that such properties can be partly captured by the natural density of the spectrum of the studied theories, which is the set of sizes of their finite models. This enriches the toolbox of the theory combination researcher, by providing new tools to determine the possibility of combining theories. It also reveals interesting and surprising connections between theory combination and number theory.

Paper Structure

This paper contains 34 sections, 41 theorems, 16 equations, 3 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. First-order logic
  4. Number theory
  5. Theory combination
  6. Theory combination and natural density
  7. Sufficient conditions
  8. Necessary conditions
  9. Gentleness
  10. Smoothness and finite model property
  11. Strong finite witnessability
  12. Computability of minimal model functions
  13. Finite witnessability
  14. Summary
  15. Non-empty signatures
  16. ...and 19 more sections

Key Result

theorem 1

If $\mathcal{T}$ is a $\Sigma_{1}$-theory with a well-defined natural density, then the positivity of $\mu(\mathcal{T})$ is sufficient for $\mathcal{T}$ to: 1. be stably infinite; 2. have the finite model property; and 3. be finitely witnessable.

Figures (3)

  • Figure 1: Cardinality formulas.
  • Figure 2: $(A)$ Initial values of the function $f$ from \ref{['definition of f']}, for $a_{0}=4$, $a_{1}=3$, $a_{2}=7$, $b_{0}=6$, $b_{1}=4$ and $b_{2}=10$. $(B)$ Initial values of the functions $G$ (in red) and $f$ (in black) from the case with computable $r$ of \ref{['FW density general case']}, for $a_{0}=1$, $a_{1}=2$, $a_{2}=3$, $b_{0}=2$, $b_{1}=3$, $b_{2}=5$, $g(1)=1$, $g(2)=1$ and $g(3)=0$.
  • Figure 3: The theory $\mathcal{T}^{s}_{\varsigma}$.

Theorems & Definitions (70)

  • definition 1
  • theorem 1
  • proof : sketch
  • theorem 2
  • proof : sketch
  • lemma 1
  • lemma 2
  • theorem 3
  • proof : sketch
  • theorem 4
  • ...and 60 more