Source-linked AI summary
Delta-Complete Decision Procedures for Satisfiability over the Reals
Sicun Gao, Jeremy Avigad, Edmund Clarke
TL;DR
SMT over nonlinear real functions can be intractable or undecidable, while numerical solvers raise correctness concerns in critical applications. The paper introduces δ-completeness, proves bounded δ-SMT decidability and complexity results, analyzes DPLL⟨ICP⟩, and identifies practical correctness guarantees, subject to bounded-composition assumptions.
Problem
SMT formulas involving nonlinear polynomials, transcendental functions, and differential equations are highly complex or undecidable, while numerical errors threaten correctness-critical uses.
Method
The paper defines δ-SMT and δ-complete procedures, then applies the framework to bounded SMT over Type 2 computable functions and formally analyzes DPLL⟨ICP⟩.
Results
Bounded δ-SMT is decidable; it is NP-complete for exponentiation and trigonometric functions and PSPACE-complete for Lipschitz-continuous ODEs.
Takeaways & Limitations
δ-completeness supplies correctness guarantees for numerically driven procedures in bounded model checking, invariant validation, theorem proving, and related critical applications.
Takeaways & Limitations
The complexity analysis requires a uniform bound on the number of function compositions in the formula.
Abstract
from arXiv · showhide
We introduce the notion of "δ-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 δ, a δ-complete decision procedure determines either that \varphi is unsatisfiable, or that the "δ-weakening" of \varphi is satisfiable. Here, the δ-weakening of \varphi is a variant of \varphi that allows δ-bounded numerical perturbations on \varphi. We prove the existence of δ-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 δ-SMT problem is in NP^C. δ-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 δ-completeness. We discuss practical applications of δ-complete decision procedures for correctness-critical applications including formal verification and theorem proving.
1 Introduction
The paper introduces δ-SMT and δ-completeness to provide formal correctness guarantees for numerically driven procedures on nonlinear real-arithmetic problems. It establishes decidability and complexity results, analyzes DPLL⟨ICP⟩, and discusses correctness-critical applications.
- Motivation: Nonlinear polynomials, transcendental functions, and differential equations make SMT solving highly intractable or undecidable.Nonlinear polynomial formulas have very high complexity, while including sine makes SMT undecidable.
- Motivation: Numerical solvers scale on nonlinear benchmarks, but numerical errors can produce incorrect answers in correctness-critical problems.Exact arithmetic and post-processing validation address this concern but reduce numerical methods’ power and are difficult to implement.
- δ-SMT and δ-completeness: δ-SMT asks whether a formula is unsatisfiable or whether its δ-weakening is satisfiable, capturing what numerically driven procedures can correctly decide.The δ-weakening permits bounded numerical relaxation of the original formula.
- Results: For exponentiation and trigonometric functions, bounded δ-SMT is NP-complete; with Lipschitz-continuous ODEs, it is PSPACE-complete.These results are obtained using techniques from computable analysis.
- Results: δ-completeness is proposed as the correctness requirement for numerically driven procedures, with DPLL⟨ICP⟩ analyzed through necessary and sufficient conditions.The framework integrates interval constraint propagation into DPLL(T).
- Applications: In bounded model checking, unsat certifies absolute safety to a depth, whereas δ-sat indicates possible unsafety under δ-bounded perturbations.The paper extends similar guarantees to invariant validation and theorem proving.
2 SMT with Type 2 Computable Functions
The paper develops a Type 2 computability framework for real functions and bounded SMT over structures containing such functions. It formalizes computability, continuity, complexity, and standard-form transformations for bounded formulas.
- 2.1 Basics of Computable Analysis: Type 2 computability represents real numbers through convergent rational approximations and computes function values to arbitrary requested precision.Oracle machines operate on names of real inputs and output rational approximations.
- 2.1 Basics of Computable Analysis: Computable real functions are continuous and uniformly continuous on compact domains with computable moduli of continuity.A modulus converts a desired output precision into a sufficient global input precision.
- 2.1 Basics of Computable Analysis: Addition, multiplication, absolute value, min, max, exp, sin, and solutions of Lipschitz-continuous ODEs are computable, with exp and sin P-computable and ODE solutions PSPACE-complete.Compositions of computable functions remain computable.
- 2.2 Bounded SMT over RF: The bounded SMT setting uses a finite collection of Type 2 computable functions and variables restricted to bounded intervals over the structure ⟨R,F⟩.Bounded formulas are represented as Σ1-sentences with bounded quantifiers.
- 2.2 Bounded SMT over RF: Atomic constraints use compositions of functions from F and comparisons with zero, while bounded domains are products of rational-endpoint intervals.The formulation permits open or closed interval bounds.
- 2.2 Bounded SMT over RF: Every bounded Σ1-sentence can be transformed into an equivalent standard form by eliminating disequalities and inequalities through Boolean and sign transformations.Positive inequality constraints are then represented using newly introduced bounded variables.
- 2.2 Bounded SMT over RF: The standard-form transformation introduces bounded existential variables to encode positive terms, as illustrated by the exponential and sine example.The example rewrites the implication using auxiliary variables with specified interval bounds.
3 The Bounded δ-SMT Problem
The bounded δ-SMT problem introduces numerical perturbations so nonlinear real-arithmetic formulas can be decided, with complexity characterized under boundedness and computability assumptions.
- Problem definition: The bounded δ-SMT problem decides whether a bounded formula is false or its δ-weakening is true.The δ-weakening permits δ-bounded numerical perturbations, and either answer may be returned when the cases overlap.
- Decidability: For finite collections of Type 2 computable functions and positive rational δ, bounded δ-SMT is decidable.The paper gives a direct decision procedure for the equality-only standard form considered here.
- Assumptions and scope: The complexity analysis requires uniformly bounded formula classes and restricts function compositions to control evaluation cost.These are described as technical restrictions that can be addressed by choosing a sufficiently rich function set and loose uniform variable bounds.
- Complexity: NP^C membership holds for uniformly bounded formulas whose functions lie in a Type 2 class C with P ⊆ C ⊆ PSPACE.A nondeterministic machine guesses a sample point and uses a C-complexity function oracle for polynomial-time evaluation.
- Complexity: For finite sets of P-time computable functions such as {+, ×, exp, sin}, uniformly bounded δ-SMT is NP-complete.For finite sets of Lipschitz-continuous ODEs over compact domains, the problem is in PSPACE and is PSPACE-complete for some theories.
4 δ-Completeness of the DPLL⟨ICP⟩Framework
The paper formally analyzes ICP and its integration with DPLL(T) for bounded δ-SMT, identifying conditions that guarantee δ-completeness. It shows that well-defined pruning is both necessary and sufficient, including for interval ODE pruning.
- Interval Constraint Propagation: ICP solves real constraints through branch-and-prune, using interval extensions to prune impossible regions and branching when pruning cannot isolate a solution.The algorithm terminates by repeatedly shrinking boxes until a sufficiently small potentially satisfiable box is found.
- Interval Constraint Propagation: A valid interval extension contains every function value over a box, while well-defined pruning contracts boxes, preserves possible zeros, and never removes real solutions.These requirements are W1, W2, and W3, respectively.
- δ-Completeness of ICPε: Theorem 4.2 states that for every δ, some ε makes ICPε δ-complete for conjunctive bounded Σ1-sentences if and only if its pruning operator is well-defined.The proof uses uniform continuity on bounded domains to relate box precision ε to the requested δ tolerance.
- δ-Completeness of ICPε: Each pruning condition is necessary: without W1 termination can fail, without W2 returned boxes can violate δ-satisfiability, and without W3 satisfiable formulas can be declared unsatisfiable.The counterexamples include f(x)=x^2+1 on [-1,1], where an invalid returned box fails δ-completeness for δ<2.
- Applications within the Framework: Box-consistent pruning is well-defined, and interval ODE pruning is well-defined when computed by an interval ODE solver.These results provide concrete pruning operators covered by the general theorem.
- DPLL⟨ICP⟩: DPLL⟨ICP⟩ is δ-complete for bounded Σ1-sentences exactly when its ICPε pruning operators are well-defined.If pruning is not well-defined, the integrated framework is not δ-complete even for conjunctions of theory atoms.
5 Applications
The paper applies δ-complete procedures to bounded model checking, invariant validation, and theorem proving. These applications use unsat results as exact certificates while interpreting δ-sat results through bounded numerical perturbations.
- Bounded Model Checking: In bounded model checking, unsat proves that a continuous or hybrid system is safe up to the chosen depth.The checked formula encodes an initial state, transitions, and membership in unsafe states.
- Bounded Model Checking: A δ-sat result means the system is unsafe or would become unsafe under a δ-bounded perturbation, with a counterexample certificate provided.The user selects δ according to the intended error tolerance of the system.
- Invariant Validation: For invariant validation, unsat of the negated invariant conditions confirms that the proposed invariant is inductive and proves safety.A δ-sat result instead indicates that the invariant fails or could fail under a small numerical perturbation.
- Theorem Proving: In theorem proving, the procedure repeatedly tests the negation at decreasing δ values, proving the statement when an unsat result is returned.This supports an iterative refinement process when δ-sat is initially obtained.
6 Conclusion
The paper establishes δ-complete decision procedures as a framework for reliable numerical reasoning over bounded real SMT problems with broad classes of nonlinear functions. It proves conditions for DPLL⟨ICP⟩ and positions the framework for verification and theorem proving.
- Conclusion: The framework covers bounded SMT over reals with Type 2 computable functions, including transcendental functions and solutions of Lipschitz-continuous ODEs.The paper also establishes the complexity of the resulting problem.
- Conclusion: δ-completeness replaces exact-solver completeness as the correctness requirement for numerically driven procedures in this domain.The paper proves necessary and sufficient conditions for δ-completeness of DPLL⟨ICP⟩.
- Conclusion: The results provide a foundation for scalable numerically driven decision procedures and their use in formal verification and theorem proving.