Delta-Decision Procedures for Exists-Forall Problems over the Reals

TL;DR

This paper introduces a delta-complete algorithm for solving nonlinear SMT problems with universal quantification over reals, advancing the capability to handle complex quantified formulas in robotics and AI.

Contribution

It presents the first delta-complete method for nonlinear SMT over reals with quantifiers, combining counterexample-guided synthesis, interval constraint propagation, and local optimization.

Findings

Handles many new problems beyond existing SMT solvers

Demonstrates effectiveness on complex quantified nonlinear problems

Ensures delta-completeness through careful numerical and symbolic reasoning

Abstract

Solving nonlinear SMT problems over real numbers has wide applications in robotics and AI. While significant progress is made in solving quantifier-free SMT formulas in the domain, quantified formulas have been much less investigated. We propose the first delta-complete algorithm for solving satisfiability of nonlinear SMT over real numbers with universal quantification and a wide range of nonlinear functions. Our methods combine ideas from counterexample-guided synthesis, interval constraint propagation, and local optimization. In particular, we show how special care is required in handling the interleaving of numerical and symbolic reasoning to ensure delta-completeness. In experiments, we show that the proposed algorithms can handle many new problems beyond the reach of existing SMT solvers.