Delta-Complete Decision Procedures for Satisfiability over the Reals

TL;DR

This paper introduces lta-complete decision procedures for SMT problems over the reals, enabling reliable handling of nonlinear and transcendental functions with bounded numerical perturbations.

Contribution

It formalizes lta-completeness for SMT over reals, proves its existence for various functions, and analyzes the lta-completeness of the DPLL<ICP> framework.

Findings

lta-complete procedures exist for bounded SMT over reals with complex functions.

Bounded lta-SMT is in NP^C for functions in Type 2 complexity class C.

Necessary and sufficient conditions for elta-completeness of DPLL<ICP> are established.

Abstract

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.