Delta-Decision Procedures for Exists-Forall Problems over the Reals
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.
Cite
@article{arxiv.1807.08137,
title = {Delta-Decision Procedures for Exists-Forall Problems over the Reals},
author = {Soonho Kong and Armando Solar-Lezama and Sicun Gao},
journal= {arXiv preprint arXiv:1807.08137},
year = {2018}
}