Number theory combination: natural density and SMT

TL;DR

This paper explores how the natural density of finite models' sizes can inform the combination of theories in SMT, revealing connections between model theory and number theory.

Contribution

It introduces a novel approach linking natural density to theory combination in SMT, expanding the analytical tools available for combining theories.

Findings

Natural density can partially characterize theory properties in SMT.

Connections between number theory and theory combination are established.

Provides new insights into the feasibility of combining theories in SMT.

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.