| ||||
| ||||
![]() Title:Delta-Decision Procedures for Exists-Forall Problems over the Reals Conference:CAV2018 Tags:Delta-completeness, Optimization, Quantifier and SMT 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. Delta-Decision Procedures for Exists-Forall Problems over the Reals ![]() Delta-Decision Procedures for Exists-Forall Problems over the Reals | ||||
Copyright © 2002 – 2025 EasyChair |