Quantified Linear and Polynomial Arithmetic Satisfiability via Template-based Skolemization

TL;DR

This work addresses the challenge of satisfiability for quantified real arithmetic (LRA/NRA) by introducing a template-based Skolemization framework that enables efficient quantifier elimination. The method unfolds in three steps: synthesize Skolem templates for existential variables, eliminate universal quantifiers via Positivstellensätze and related theorems, and confirm satisfiability with a quantifier-free SMT check while optionally producing witnesses. The approach is sound, semi-complete, and subexponential in complexity with respect to the template degree, and it yields concrete witnesses for existential variables. Empirical results on LRA and NRA benchmarks show that the method, implemented in QuantiSAT, outperforms state-of-the-art SMT solvers in the number of solved instances and provides unique solutions not found by competitors, underscoring its practical impact for quantified reasoning in real-arithmetic theories.

Abstract

The problem of checking satisfiability of linear real arithmetic (LRA) and non-linear real arithmetic (NRA) formulas has broad applications, in particular, they are at the heart of logic-related applications such as logic for artificial intelligence, program analysis, etc. While there has been much work on checking satisfiability of unquantified LRA and NRA formulas, the problem of checking satisfiability of quantified LRA and NRA formulas remains a significant challenge. The main bottleneck in the existing methods is a computationally expensive quantifier elimination step. In this work, we propose a novel method for efficient quantifier elimination in quantified LRA and NRA formulas. We propose a template-based Skolemization approach, where we automatically synthesize linear/polynomial Skolem functions in order to eliminate quantifiers in the formula. The key technical ingredients in our approach are Positivstellensätze theorems from algebraic geometry, which allow for an efficient manipulation of polynomial inequalities. Our method offers a range of appealing theoretical properties combined with a strong practical performance. On the theory side, our method is sound, semi-complete, and runs in subexponential time and polynomial space, as opposed to existing sound and complete quantifier elimination methods that run in doubly-exponential time and at least exponential space. On the practical side, our experiments show superior performance compared to state-of-the-art SMT solvers in terms of the number of solved instances and runtime, both on LRA and on NRA benchmarks.

Figures (1)

• Figure 1: Runtime distribution over the LRA (left) and NRA (right) benchmarks solved by each tool. The figure to the right is in logarithmic scale for better presentation. Generally, faster tools have lower curves and the more instances a tool solves, its curve will be more to the right. Since solving more instances is primary, tools with graphs to the right are preferable.

Theorems & Definitions (15)

• Theorem 1: scowcroft1988note
• Example
• Example : Continued
• Remark : Distinction between LRA and NRA
• Example : Continued
• Theorem 2: Soundness, Semi-Completeness, Complexity, proof in the Appendix
• Theorem 3: Farkas' Lemma farkas1902theorie
• Definition 1: Semi-group generated by $\Phi$
• Theorem 4: Handelman's Theorem handelman1988representing
• Theorem 5: Putinar's Positivstellensatz putinar1993positive