PaperlayerView exact revision on arXiv

Source-linked AI summary

Solving quantified constraint satisfaction problems with applications to control

Éric Goubault, Nuwan Herath Mudiyanselage, Sylvie Putot

arXiv:2610.39776v1cs.LO

TL;DR

Control problems such as robust reachability can be expressed as quantified constraints, but existing methods are often limited to local solutions or one quantifier alternation. This paper combines set inversion with local approximation oracles to compute global inner and outer solution approximations, and demonstrates criteria that agree on the running example.

  • Problem

    The paper addresses global characterization of solution sets for quantified constraints, where existing approaches may be limited to local solutions or at most one quantifier alternation.

    Source: §1 · pp. 1–2

  • Method

    The method applies set inversion to the relaxed inverse problem, using local inner and outer approximations and oracles to characterize global solution approximations.

    Source: §1 · p. 2

  • Results

    On the running example, the criteria based on P, G and on ¬P, G∁ agree, certifying [17/18, 19/18] inside and [0, 1/2] outside the solution set.

    Source: §3.3 · p. 4

  • Takeaways & Limitations

    The framework is presented for applications including robust forward and backward reachability, controller synthesis, and motion planning.

    Source: §1 · p. 1

    For zero-measure solution sets, the method generally provides only an outer approximation, with an empty inner approximation.

    Source: §4.2 · p. 7

Abstract

from arXiv · show

Many problems in control can be expressed as quantified constraints, such as robust forward and backward reachability, synthesis of controllers, solutions to motion planning problems. In this paper, we develop a method for computing inner and outer approximations of global solutions to very general quantified constraints, generalizing widely the state of the art on similar problems, usually restricted to at most one alternation of quantifiers or to local solutions. By global solutions, we mean characterizing accurately the entire set of solutions, within some prescribed bounds. For this, our approach uses a set inversion technique relying on oracles for set inclusion using local solutions to related quantified reachability problems. We exemplify the approach throughout the paper on different examples related to control problems.

CSS Concepts

The paper is classified under logic and verification in theory of computation.

CSS Concepts

  • The listed computing area is logic and verification.The classification places it under theory of computation.Source: CSS Concepts · p. 1

Keywords

The paper's listed keywords are set-based methods, set inversion, quantified constraint satisfaction, reachability, and control.

Keywords

  • The listed keywords are set-based methods, set inversion, quantified constraint satisfaction problems, reachability, and control.Source: Keywords · p. 1

1 Introduction

The paper characterizes global solution sets for quantified constraints, including formulas with alternating universal and existential quantifiers. It combines set inversion with local approximation oracles and parameter subdivision to obtain inner and outer approximations.

1 Introduction

  • Robust reachability asks which initial states reach a target despite disturbances, but requiring exact reachability for every disturbance may be too strict.The paper notes that relaxations, including time relaxation, have therefore been studied.Source: §1 · p. 1
  • The paper presents the framework as applicable to robust forward and backward reachability, controller existence and synthesis, and motion planning.The problem is to characterize inputs whose images under quantified expressions reach a goal region.Source: §1 · p. 1
  • For the running example, the full solution comprises three disconnected intervals, whereas a local method would find only part of the set.The intervals lie around 1, 2, and 3; the characterization uses inner and outer approximations.Source: §1 · p. 2
  • Symbolic quantifier elimination is practically limited by complexity and by reachability problems that are not generally solvable algebraically.Other approaches include numerical and set-based reachability methods, while prior quantified set inversion is limited to one quantifier alternation.Source: §1 · p. 2
  • Prior quantified set-inversion methods also restrict the functions they handle, including reliance on explicitly given rational functions.The cited work may require rewriting functions into tree-optimal form, especially for multi-incident functions.Source: §1 · p. 2
  • The framework handles arbitrary numbers of quantifier alternations and does not require explicit functions, given outer approximations of their partial derivatives.This supports applications to flow functions defined by differential equations and general reachability problems.Source: §1 · p. 2
  • The method computes global inner and outer approximations of solution sets for quantified constraints, extending local approximation techniques through set inversion.The paper frames the inverse problem as identifying inputs whose images under quantified expressions reach a goal output.Source: §1 · pp. 1–2
  • SIVIA-style paving of the free-variable domain uses oracles to classify boxes as inside the solution set, outside it, or undecided.The proposed oracles rely on local forward inner and outer approximations; parameter subdivision can refine their precision.Source: §1 · p. 2

2 Background on local approximations

The background develops interval inner and outer approximations for quantified reachability, focusing on a single universal-existential alternation and a differentiable function.

2 Background on local approximations

  • Earlier interval-based techniques compute inner and outer approximations for quantified reachability problems with repeated ∀∃ quantifier pairs.These methods are defined over a box of variables.Source: §2 · p. 2
  • For the one-alternation case, the reachable set is the set of outputs attained for every universally quantified input by some existentially chosen input.The paper introduces this relation as R_∀∃(f, X).Source: §2 · p. 2
  • Theorem 2.1 gives interval inner and outer approximations for a continuously differentiable scalar function using interval bounds on its derivatives.The method uses the function value at the box center and bounds on derivatives with respect to each input block.Source: §2 · p. 3
  • Existential variables increase the width of reachable sets through their freedom of choice, while universal variables decrease it.The paper uses these local approximation results to implement the global method's oracles.Source: §2 · p. 3

3 Global inner and outer-approximations of solutions to QCSP

The paper constructs global inner and outer approximations by paving the domain and using local reachability approximations to classify its subsets. The section develops inclusion oracles, illustrates their criteria, and discusses their behavior across examples.

3 Global inner and outer-approximations of solutions to QCSP

  • The method seeks global solution sets by combining local inner and outer approximations with a paving of the free domain.Subsets are classified as inside the solution set, outside it, or unresolved.Source: §3 · p. 3, §3.1 · p. 3

3.1 Paving-based algorithm

  • The paving algorithm bisects unresolved boxes and uses inclusion oracles to classify boxes as contained in the solution set or its complement.A separate parameter-space partitioning strategy can improve oracle quality.Source: §3.1 · p. 3, §3.2 · p. 3

3.2 Oracles

  • Four criteria use inner or outer approximations of quantified reachable sets to decide whether a domain box lies inside or outside the solution set.The criteria use either P and G or their complements, ¬P and G∁.Source: §3.2 · pp. 3–4

3.3 Sample calculations and discussion

  • For the running example, both oracle approaches certify [17/18, 19/18] inside Σ1 and [0, 1/2] outside it.The intervals and their position relative to the first solution component are shown in Figure 2.Source: §3.3 · p. 4, Figure 2 · p. 4

3.3.1 Oracle OIN

  • The OIN calculation certifies [17/18, 19/18] ⊆ Σ1; universal-quantifier intervals act adversarially and can be interpreted as Minkowski differences.The dual criterion also proves inclusion in this example; a direct local solution is unavailable because x is implicit rather than explicit.Source: §3.3.1 · p. 4

3.3.2 Oracle OOUT

  • The OOUT calculation certifies X = [0, 1/2] is included in Σ∁ using Lemma 3.4.The example computes an inner approximation for the complement-based criterion.Source: §3.3.2 · p. 5

3.3.3 Comparison of the various criteria

  • In dimension one, the order-0 dual criteria are equivalent, while for m>1 some order-0 criteria are generally disadvantaged by coarser inner approximations.For higher-order methods, differing abstraction precision means the dual criteria need not agree.Source: §3.3.3 · p. 5

3.3.4 An application to backward reachability

  • The approach also handles backward reachability and functions that are non-polynomial or not given analytically; a Dubins-vehicle example certifies [−0.1, 0] outside Σ.The example considers an adversarial perturbation and a target x-coordinate in [0.49, 1].Source: §3.3.4 · p. 5

4 Improvements of the paving algorithm

The section refines the paving algorithm’s set-inclusion oracles by subdividing quantified parameter domains according to quantifier type. It establishes sound ways to preserve inner or outer approximations, including a midpoint strategy for combining subdivisions.

4 Improvements of the paving algorithm

  • Parameter subdivision can improve oracle precision and tighten inner and outer reachable-set bounds by narrowing parameter ranges.The tighter estimates also reflect improved evaluation of the Jacobian of function g.Source: §4 · p. 5, §4.1 · p. 6

4.1 Subdividing either existentially or universally quantified parameter domain

  • Existential parameter subdivisions combined by union yield inner approximations, while universal subdivisions combined by intersection yield outer approximations.The section uses these direction-sensitive refinements to improve approximations of reachable sets.Source: §4.1 · p. 6

4.2 Combining the subdivision of existentially and universally quantified parameters

  • Combining existential and universal subdivisions directly generally yields neither an inner nor an outer approximation, so the section uses midpoint choices instead.The midpoint construction holds some subdivided parameters at representative points while subdividing the others.Source: §4.2 · p. 7
  • Midpoint choices for existential parameters reduce each subproblem to a purely universally quantified one, enabling an inner approximation after subdivision.Dually, midpoint choices for universal parameters allow existential subdivision to produce an outer approximation.Source: §4.2 · p. 7
  • For zero-measure solution sets, the method generally provides only an outer approximation, with an empty inner approximation.For well-behaved functions in the predicates, paving methods converge in volume to the solution as subdivisions increase.Source: §4.2 · p. 7

5 Implementation and benchmarks

The prototype applies paving and parameter-refinement methods to control examples, with results showing reduced undecided regions at finer settings but differing computation times.

5 Implementation and benchmarks

  • The criteria and refinements were implemented in Julia with IntervalArithmetic and LazySets, and examples ran on a 12th Gen Intel Core i7-12700H with 16 Gio RAM.The prototype was unoptimized, interpreted rather than compiled.Source: §5 · p. 7

5.1 Running example

  • For the running example, undecided volume fell to about 6% without parameter subdivision and about 3% with subdivision as εX approached 10^-4.Subdividing all quantified parameters approached an exact solution quickly, with a less significant computation-time increase; the reported Table 3 and Figure 3 show the paving and precision trend.Source: §5.1 · pp. 7–8, Figure 3 · p. 8, Table 3 · p. 9

5.2 Stability of a controller

  • The controller-stability paving left 1.3% of the domain undecided and took 25 ms; the uncertain-ODE quantified variant solved in about the same time without subdivision.The example uses Algorithm 1 without subdivision at εX = 0.1.Source: §5.2 · p. 8, Figure 5 · p. 8

5.3 Dubins vehicle and generalized reachability

  • The Dubins reachability bounds were [-0.96, 2.96] ⊆ R∃∀∃(x) ⊆ [-1.01, 3.01] with 1.5% undecided, [-0.99, 0.99] ⊆ R∃∀∃(y) ⊆ [-1.94, 1.94] with 24%, and [-0.19, 0.19] ⊆ R∃∀∃(θ) ⊆ [-0.23, 0.23] with 7.8%.The bounds used εX = εP = 0.01 and the Section 4.1 subdivision method; computation times were 2.6 ms, 22 ms, and 1.3 ms for x, y, and θ, respectively.Source: §5.3 · p. 9, Figure 6 · p. 9

5.4 Circle collision problem

  • 6.0% of the circle-collision domain remained undecided after 25 s at εX = εP = 0.1; at 0.01, 0.4% remained after 3100 s.Both results use the Section 4.2 refinement algorithm.Source: §5.4 · p. 9, Figure 7 · p. 9

5.5 Robot collision problem

  • 9.2% of the robot-collision domain remained undecided in 5.3 s at εX = εP = 0.1, versus 0.8% in 291 s at 0.01.Without parameter subdivision, 93% remained undecided in 165 ms; Section 4.1 subdivisions left 52% undecided in 3.1 s, and only Section 4.2 produced a nonempty inner approximation.Source: §5.5 · p. 10, Figure 8 · p. 10

6 Conclusion

The paper proposes inner and outer approximations of global solutions to general quantified constraint satisfaction problems. It identifies extensions to broader quantified formulas and applications, and higher-order methods, as future work.

6 Conclusion

  • The paper proposes computing inner and outer approximations of global solutions to general quantified constraint satisfaction problems.Source: §6 · p. 10
  • Future work includes fully general quantifier elimination, disjunctions of predicates, more applications such as controller synthesis, and improved parameter subdivision strategies.Source: §6 · p. 10
  • The authors also plan to test higher-order methods instead of interval methods to increase precision and performance.Source: §6 · p. 10
Loading 2610.39776v1…