Delta-Decision Procedures for Exists-Forall Problems over the Reals
© The Author(s) 2018. We propose δ -complete decision procedures for solving satisfiability of nonlinear SMT problems over real numbers that contain universal quantification and a wide range of nonlinear functions. The methods combine interval constraint propagation, counterexample-guided synthesis,...
| Main Authors: | , , |
|---|---|
| Other Authors: | |
| Format: | Article |
| Language: | English |
| Published: |
Springer International Publishing
2021
|
| Online Access: | https://hdl.handle.net/1721.1/137908 |
| Summary: | © The Author(s) 2018. We propose δ -complete decision procedures for solving satisfiability of nonlinear SMT problems over real numbers that contain universal quantification and a wide range of nonlinear functions. The methods combine interval constraint propagation, counterexample-guided synthesis, and numerical optimization. In particular, we show how to handle the interleaving of numerical and symbolic computation to ensure delta-completeness in quantified reasoning. We demonstrate that the proposed algorithms can handle various challenging global optimization and control synthesis problems that are beyond the reach of existing solvers. |
|---|