δ-Complete Decision Procedures for Satisfiability over the Reals

<p>We introduce the notion of “<em>δ</em>-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<em>ϕ</em> and a positive rational number <em>δ</em>, a <em>δ</em>-complete decision procedure determines either that <em>ϕ</em> is unsatisfiable, or that the “<em>δ</em>-weakening” of <em>ϕ</em> is satisfiable. Here, the <em>δ</em>-weakening of <em>ϕ</em> is a variant of <em>ϕ</em> that allows <em>δ</em>-bounded numerical perturbations on <em>ϕ</em>. We establish the existence and complexity of <em>δ</em>-complete decision procedures for bounded SMT over reals with functions mentioned above. We propose to use <em>δ</em>-completeness 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 in DPLL(T), and establish necessary and sufficient conditions for its <em>δ</em>-completeness. We discuss practical applications of <em>δ</em>-complete decision procedures for correctness-critical applications including formal verification and theorem proving.</p>