  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 prove the
existence of \delta-complete decision procedures for bounded SMT over reals
with functions mentioned above. For functions in Type 2 complexity class C,
under mild assumptions, the bounded \delta-SMT problem is in NP^C.
\delta-Complete decision procedures can exploit scalable numerical methods for
handling nonlinearity, and we propose to use this notion as an ideal
requirement for numerically-driven decision procedures. As a concrete example,
we formally analyze the DPLL<ICP> framework, which integrates Interval
Constraint Propagation (ICP) 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.

Logic in Computer Science;Symbolic Computation