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

arXiv: https://arxiv.org/abs/1807.08137 · HTML: https://mlsanity.com/paper/1807.08137/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 21 Jul 2018.

## Built on by (most cited first, 1 of 1)

- [LinSyn: Synthesizing Tight Linear Bounds for Arbitrary Neural Network Activation Functions](https://mlsanity.com/paper/2201.13351/) (2022)

## Abstract (arXiv)

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.