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.
For the entire collection see [Zbl 1245.68010].