A Relational Theory of Grounding and a new Grounder for SMT

TL;DR

This paper introduces a relational framework for grounding SMT formulas, enabling efficient transformation of quantified formulas into finite equivalents, and presents a new grounder that improves SMT solver performance.

Contribution

It proposes a novel relational algebra-based grounding method for SMT formulas, including infinite domain quantifiers, and implements a practical grounder that enhances solver efficiency.

Findings

xmt-lib significantly improves Z3 performance

Grounding formulas with aggregates is more efficient

Finite size formulas can be derived from infinite domain quantifiers

Abstract

Satisfiability Modulo Theories (SMT) specifications often rely on quantifiers to remain concise and declarative. However, checking the satisfiability of such specifications directly can be inefficient. A common optimization is to ground the specification - that is, to expand quantified formulas into equivalent variable-free formulas. While dedicated tools known as grounders are a cornerstone of Answer Set Programming (ASP) solvers, they are are largely absent from SMT solving workflows. As a result, users frequently resort to writing ad-hoc, error-prone code to perform this transformation. In this work, I propose a theoretical framework for grounding first order logic formulas with aggregates, based on relational algebra. Within this framework, I formulate a method for efficiently grounding such formulas. Remarkably, the method allows certain formulas that quantify over infinite domains to be transformed into equivalent formulas of finite size. I have implemented this method in a new SMT-LIB grounder, called xmt-lib. It leverages an embedded relational database (SQLite) to execute relational operations efficiently. An evaluation on a public benchmark for grounders demonstrates that xmt-lib significantly improves the performance of the Z3 SMT solver compared to its purely declarative use, and makes it com