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

Authors: Soonho Kong, Armando Solar-Lezama and Sicun Gao

Paper Information

Title:Delta-Decision Procedures for Exists-Forall Problems over the Reals
Authors:Soonho Kong, Armando Solar-Lezama and Sicun Gao
Proceedings:CAV All Papers
Editors: Georg Weissenbacher, Hana Chockler and Igor Konnov
Keywords:SMT, Optimization, Quantifier, Delta-completeness

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.

Talk:Jul 17 11:00 (Session 119A: SAT, SMT and Decision Procedures)