Delta-Decision Procedures for Exists-Forall Problems over the Reals
Delta-Decision Procedures for Exists-Forall Problems over the Reals
复制标题
DOI：
10.1007/978-3-319-96142-2_15
复制
发表时间：
2018-07
期刊：
影响因子：
--
通讯作者：
Soonho Kong;Armando Solar-Lezama;Sicun Gao
中科院分区：
文献类型：
--
作者：
Soonho Kong;Armando Solar-Lezama;Sicun Gao
我们提出了解决实数上非线性SMT问题的可满足性的完整决策过程，这些问题包含普遍的量化和广泛的非线性函数。该方法将区间约束传播、反例引导综合和数值优化相结合。特别地，我们展示了如何处理数值和符号计算的交错，以确保量化推理中的delta完备性。我们证明了所提出的算法可以处理现有求解器无法解决的各种具有挑战性的全局优化和控制综合问题。
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.