Reducing the Complexity of Quantified Formulas via Variable Elimination

TL;DR

This paper introduces a method for simplifying quantified SMT formulas through variable elimination based on analyzing ground terms, leading to potentially easier-to-solve formulas and improved solving times across different SMT solvers.

Contribution

It presents a novel variable elimination technique for quantified SMT formulas using set constraints derived from ground term analysis, reducing quantifiers and simplifying formulas.

Findings

Significant reduction in solving time for many formulas

Method is effective across different SMT solvers like Z3 and CVC4

Simplification often results in fewer quantifiers and easier formulas

Abstract

We present a general simplification of quantified SMT formulas using variable elimination. The simplification is based on an analysis of the ground terms occurring as arguments in function applications. We use this information to generate a system of set constraints, which is then solved to compute a set of sufficient ground terms for each variable. Universally quantified variables with a finite set of sufficient ground terms can be eliminated by instantiating them with the computed ground terms. The resulting SMT formula contains potentially fewer quantifiers and thus is potentially easier to solve. We describe how a satisfying model of the resulting formula can be modified to satisfy the original formula. Our experiments show that in many cases, this simplification considerably improves the solving time, and our evaluations using Z3 and CVC4 indicate that the idea is not specific to a particular solver, but can be applied in general.