An Instantiation-Based Approach for Solving Quantified Linear Arithmetic

TL;DR

This paper introduces an instantiation-based decision procedure for quantified linear arithmetic formulas, enhancing SMT solver capabilities with improved performance on benchmarks from model checking, static analysis, and synthesis.

Contribution

It develops a new framework for instantiation-based decision procedures applicable to quantified linear arithmetic, with implementation and evaluation demonstrating superior performance.

Findings

Outperforms existing tools on standardized benchmarks

Successfully integrates into SMT solver architecture

Effective for formulas with one quantifier alternation

Abstract

This paper presents a framework to derive instantiation-based decision procedures for satisfiability of quantified formulas in first-order theories, including its correctness, implementation, and evaluation. Using this framework we derive decision procedures for linear real arithmetic (LRA) and linear integer arithmetic (LIA) formulas with one quantifier alternation. Our procedure can be integrated into the solving architecture used by typical SMT solvers. Experimental results on standardized benchmarks from model checking, static analysis, and synthesis show that our implementation of the procedure in the SMT solver CVC4 outperforms existing tools for quantified linear arithmetic.