Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Relational Theory of Grounding and a new Grounder for SMT

Pierre Carbonnelle

TL;DR

A theoretical framework for grounding first order logic formulas with aggregates, based on relational algebra is proposed and a method for efficiently grounding such formulas is formulated, which allows certain formulas that quantify over infinite domains to be transformed into equivalents of finite size.

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

A Relational Theory of Grounding and a new Grounder for SMT

TL;DR

A theoretical framework for grounding first order logic formulas with aggregates, based on relational algebra is proposed and a method for efficiently grounding such formulas is formulated, which allows certain formulas that quantify over infinite domains to be transformed into equivalents of finite size.

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
Paper Structure (38 sections, 1 theorem, 8 equations, 1 figure, 4 tables)

This paper contains 38 sections, 1 theorem, 8 equations, 1 figure, 4 tables.

Table of Contents

  1. Introduction
  2. Related work
  3. Preliminaries
  4. Sorted first-order logic.
  5. Relational algebra.
  6. A relational framework for theories of grounding
  7. Model expansion.
  8. Grounding.
  9. Valuation relation.
  10. Grounding relation.
  11. Interpretation relation.
  12. Grounding with relational algebra
  13. Validation
  14. Implementation
  15. Benchmark
  16. ...and 23 more sections

Key Result

Lemma 11

The $\top U$ grounding relation of term $\phi$ for the set $X$ of all valuations of its free variables, projected on the free variables, is the exact $\top U$ x-generator for the term $\phi$.

Figures (1)

  • Figure 1: A point ($n$, $t$) in the curve of a solver means that $n$ problems of the DIRT benchmark are grounded and solved within $t$ seconds by the solver. Lower and further-right curves indicate better performance. The graph is limited by the timeout at 600 seconds.

Theorems & Definitions (11)

  • Example 1
  • Example 2
  • Example 3
  • Example 4
  • Example 5
  • Example 6
  • Example 7
  • Example 8
  • Example 9
  • Example 10
  • ...and 1 more