Delta-Complete Decision Procedures for Satisfiability over the Reals

Details Delta-Complete Decision Procedures for Satisfiability over the Reals Delta-Complete Decision Procedures for Satisfiability over the Reals

2012-04-16

arxiv.org/abs/1204.3513v1

Computer Science

Logic in Computer Science

A shorter version appears in IJCAR 2012

Scientific paper

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 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.

Affiliated with

Also associated with

No associations

Rating

Delta-Complete Decision Procedures for Satisfiability over the Reals does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Delta-Complete Decision Procedures for Satisfiability over the Reals, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Delta-Complete Decision Procedures for Satisfiability over the Reals will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-6816