06076914

a

06076914 Gao, Sicun Avigad, Jeremy Clarke, Edmund M. $\delta $-complete decision procedures for satisfiability over the reals. Gramlich, Bernhard (ed.) et al., Automated reasoning. 6th international joint conference, IJCAR 2012, Manchester, UK, June 26--29, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-31364-6/pbk). Lecture Notes in Computer Science 7364. Lecture Notes in Artificial Intelligence, 286-300 (2012). 2012 Berlin: Springer EN

doi:10.1007/978-3-642-31365-3_23

Summary: We introduce the notion of ``$\delta $-complete decision procedures'' for solving SMT problems over the real numbers, with the aim of handling a wide range of nonlinear functions including transcendental functions and solutions of Lipschitz-continuous ODEs. Given an SMT problem $\varphi $ and a positive rational number $\delta $, a $\delta $-complete decision procedure determines either that $\varphi $ is unsatisfiable, or that the ``$\delta $-weakening'' of $\varphi $ is satisfiable. Here, the $\delta $-weakening of $\varphi $ is a variant of $\varphi $ that allows $\delta $-bounded numerical perturbations on $\varphi $. We establish the existence and complexity of $\delta $-complete decision procedures for bounded SMT over reals with functions mentioned above. We propose to use $\delta $-completeness as an ideal requirement for numerically-driven decision procedures. As a concrete example, we formally analyze the DPLL$\langle $ICP$\rangle $ framework, which integrates Interval Constraint Propagation in DPLL$(T)$, and establish necessary and sufficient conditions for its $\delta $-completeness. We discuss practical applications of $\delta $-complete decision procedures for correctness-critical applications including formal verification and theorem proving.