Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Efficient Solving of Quantified Inequality Constraints over the Real Numbers

Stefan Ratschan

TL;DR

This work tackles the challenging problem of solving quantified inequality constraints over the real numbers, presenting a terminating branch-and-prune solver based on narrowing operators. By formalizing a framework for reusable pruning (outer/inner narrowing) and introducing notions of box-, hull-, and tight-consistency, it enables efficient pruning of bounded search spaces for quantified constraints. The paper provides a complete algorithm, proves termination for numerically stable inputs, and demonstrates practical efficiency with a range of implementation optimizations and timings that outperform previous cylindrical box decomposition approaches. The results extend constraint programming techniques to quantified real-number problems beyond polynomials, offering a scalable, numerically robust approach with direct applicability to open problems in numerical CSPs and optimization.

Abstract

Let a quantified inequality constraint over the reals be a formula in the first-order predicate language over the structure of the real numbers, where the allowed predicate symbols are $\leq$ and $<$. Solving such constraints is an undecidable problem when allowing function symbols such $\sin$ or $\cos$. In the paper we give an algorithm that terminates with a solution for all, except for very special, pathological inputs. We ensure the practical efficiency of this algorithm by employing constraint programming techniques.

Efficient Solving of Quantified Inequality Constraints over the Real Numbers

TL;DR

This work tackles the challenging problem of solving quantified inequality constraints over the real numbers, presenting a terminating branch-and-prune solver based on narrowing operators. By formalizing a framework for reusable pruning (outer/inner narrowing) and introducing notions of box-, hull-, and tight-consistency, it enables efficient pruning of bounded search spaces for quantified constraints. The paper provides a complete algorithm, proves termination for numerically stable inputs, and demonstrates practical efficiency with a range of implementation optimizations and timings that outperform previous cylindrical box decomposition approaches. The results extend constraint programming techniques to quantified real-number problems beyond polynomials, offering a scalable, numerically robust approach with direct applicability to open problems in numerical CSPs and optimization.

Abstract

Let a quantified inequality constraint over the reals be a formula in the first-order predicate language over the structure of the real numbers, where the allowed predicate symbols are and . Solving such constraints is an undecidable problem when allowing function symbols such or . In the paper we give an algorithm that terminates with a solution for all, except for very special, pathological inputs. We ensure the practical efficiency of this algorithm by employing constraint programming techniques.

Paper Structure

This paper contains 18 sections, 11 theorems, 5 figures, 2 tables, 2 algorithms.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. A Framework for Reusable Pruning
  4. Consistency of Quantified Constraints
  5. Pruning Algorithm
  6. Solver
  7. Efficient Implementation
  8. Connectives with Arbitrary Arity
  9. Quantifier Blocks
  10. Removing Empty Disjunctive Branches
  11. Combination with Negated Constraint
  12. Branching Strategy
  13. Incremental Disjunctive Pruning
  14. Shortcut for Disjunctions
  15. Reusing Dual Information
  16. ...and 3 more sections

Key Result

Theorem 1

Let $\overline{N}$ be a function on bounded constraints and let $\underline{N}(\phi, B):= (\Vec{\neg}\phi_{N}, B_{N})$ where $(\phi_{N}, B_{N})=\overline{N}(\Vec{\neg}\phi, B)$. Then $\overline{N}$ is an outer narrowing operator iff $\underline{N}$ is an inner narrowing operator.

Figures (5)

  • Figure 1: Conjunction---Structural Tight Consistency
  • Figure 2: Universal Quantification---Structural Tight Consistency
  • Figure 3: Existential Pruning
  • Figure 4: Universal Pruning
  • Figure 5: Universal Pruning

Theorems & Definitions (33)

  • Definition 1
  • Definition 2
  • Theorem 1
  • proof
  • Definition 3
  • Example 1
  • Example 2
  • Definition 4
  • Definition 5
  • Definition 6
  • ...and 23 more