Universally Quantified Interval Constraint Solving

Frdric Benhamou and Frdric Goualard

Institut de Recherche en Informatique de Nantes, France

Motivations

Object Ω with trajectory: [ \begin{matrix}x(θ) = 3 sin θ cos θ(sin θ − cos θ) \\ y(θ) = 3 sin θ cos θ(sin θ + cos θ) \\ z(θ) = 0 \end{matrix}

Positions of a camera Γ s.t. |Γ, Ω| ≥ 0.5 at any time?

∀θ ∈ −ππ:

Non-linear real constraint: compulsory to solve it soundly Object Ω with trajectory: [ \begin{matrix}x(θ) = 3 sin θ cos θ(sin θ − cos θ) \\ y(θ) = 3 sin θ cos θ(sin θ + cos θ) \\ z(θ) = 0 \end{matrix}

\sqrt{(3 sin θ cos θ(sin θ − cos θ) − x)^{2} + (3 sin θ cos θ(sin θ + cos θ) − y)^{2} + z^{2}} ≥ 0.5

Universally Quantified Interval Constraint Solving – p. 2

Positions of a camera Γ s.t. |Γ, Ω| ≥ 0.5 at any time?

∀θ ∈ −ππ:

Non-linear real constraint: compulsory to solve it soundly Object Ω with trajectory: [ \begin{matrix}x(θ) = 3 sin θ cos θ(sin θ − cos θ) \\ y(θ) = 3 sin θ cos θ(sin θ + cos θ) \\ z(θ) = 0 \end{matrix}

\sqrt{(3 sin θ cos θ(sin θ − cos θ) − x)^{2} + (3 sin θ cos θ(sin θ + cos θ) − y)^{2} + z^{2}} ≥ 0.5

Universally Quantified Interval Constraint Solving – p. 2

Positions of a camera Γ s.t. |Γ, Ω| ≥ 0.5 at any time?

∀θ ∈ −ππ:

Non-linear real constraint: compulsory to solve it soundly Object Ω with trajectory: [ \begin{matrix}x(θ) = 3 sin θ cos θ(sin θ − cos θ) \\ y(θ) = 3 sin θ cos θ(sin θ + cos θ) \\ z(θ) = 0 \end{matrix}

\sqrt{(3 sin θ cos θ(sin θ − cos θ) − x)^{2} + (3 sin θ cos θ(sin θ + cos θ) − y)^{2} + z^{2}} ≥ 0.5

Universally Quantified Interval Constraint Solving – p. 2

Positions of a camera Γ s.t. |Γ, Ω| ≥ 0.5 at any time?

∀θ ∈ −ππ:

Non-linear real constraint: compulsory to solve it soundly

\sqrt{(3 sin θ cos θ(sin θ − cos θ) − x)^{2} + (3 sin θ cos θ(sin θ + cos θ) − y)^{2} + z^{2}} ≥ 0.5

Universally Quantified Interval Constraint Solving – p. 2

Outline

• Sound techniques • Cylindrical Algebraic Decomposition

• Interval arithmetic and inner-approximation computation

• Complete techniques • Interval constraint solving

• Interval constraint solving and soundness

• Solving constraints with universal quantifiers • Conclusion and perspectives

Universally Quantified Interval Constraint Solving – p. 3

Cylindrical Algebraic Decomposition

[Collins, 1973] (quantifier elimination)

• Powerful method (handling of universal/existential quantifiers)

• Sound solving of real constraints

But:

• Method restricted to polynomial constraints • High complexity (time consuming)

Cylindrical Algebraic Decomposition

[Collins, 1973] (quantifier elimination)

• Powerful method (handling of universal/existential quantifiers)

• Sound solving of real constraints

But:

• Method restricted to polynomial constraints • High complexity (time consuming)

Interval Arithmetic

[Moore, 1966] Interval set : ab = {x ∈| a ≤ x ≤ b} Interval extension:

• Extension of a real function. f:^{n} →, F:^{n} → s.t. ∀B: D_{f}(B) ⊆ F (B)

• Extension of a real relation ρ ⊆^{n} . Set of boxes R such that:

(a_{1}, …, a_{n}) ∈ ρ ⇒ ∃(I_{1}, …, I_{n}) ∈ Rs.t.a_{1} ∈ I_{1}, …, a_{n} ∈ I_{n}

Approximation of a relation

Outer approximation of ρ: ρ = ⋂{B ∈^{n}|⊆ B} Inner approximation of ρ: Inner(ρ) = {a ∈^{n}| {a} ⊆ ρ} Splitting/evaluation scheme (SES) for straightforward inner approximation computation: Example. c: f(x) ≤ 0?

Outer approximation of ρ: ρ = ⋂{B ∈^{n}|⊆ B} Inner approximation of ρ: Inner(ρ) = {a ∈^{n}| {a} ⊆ ρ} Splitting/evaluation scheme (SES) for straightforward inner approximation computation: Example. c: f(x) ≤ 0?

Outer approximation of ρ: ρ = ⋂{B ∈^{n}|⊆ B} Inner approximation of ρ: Inner(ρ) = {a ∈^{n}| {a} ⊆ ρ} Splitting/evaluation scheme (SES) for straightforward inner approximation computation: Example. c: f(x) ≤ 0?

Outer approximation of ρ: ρ = ⋂{B ∈^{n}|⊆ B} Inner approximation of ρ: Inner(ρ) = {a ∈^{n}| {a} ⊆ ρ} Splitting/evaluation scheme (SES) for straightforward inner approximation computation: Example. c: f(x) ≤ 0?

Outer approximation of ρ: ρ = ⋂{B ∈^{n}|⊆ B} Inner approximation of ρ: Inner(ρ) = {a ∈^{n}| {a} ⊆ ρ} Splitting/evaluation scheme (SES) for straightforward inner approximation computation: Example. c: f(x) ≤ 0?

EIA4

[Jardillier & Languénou, 1998] (Modelling of camera movements) Solving ∀v ∈ ab: c(x, v) with the SES:

⇒ algorithm EIA4 (very costly)

EIA4

[Jardillier & Languénou, 1998] (Modelling of camera movements) Solving ∀v ∈ ab: c(x, v) with the SES:

⇒ algorithm EIA4 (very costly)

EIA4

[Jardillier & Languénou, 1998] (Modelling of camera movements) Solving ∀v ∈ ab: c(x, v) with the SES:

⇒ algorithm EIA4 (very costly)

EIA4

[Jardillier & Languénou, 1998] (Modelling of camera movements) Solving ∀v ∈ ab: c(x, v) with the SES:

⇒ algorithm EIA4 (very costly)

EIA4

[Jardillier & Languénou, 1998] (Modelling of camera movements) Solving ∀v ∈ ab: c(x, v) with the SES:

⇒ algorithm EIA4 (very costly)

Interval constraint solving

• Variables x_{1}, …, x_{n} → domains D_{1}, …, D_{n}

• Constraint c(x_{1}, …, x_{n})

→ contracting operator c

[Benhamou & Older, Apt, …]

D = D_{1} × ⋯ × D_{n} D′ ⊆ D

• Properties: contractance, monotony, completeness (c ∩ D ⊆ N[c](D))

• Constraint system c_{1}, …, c_{m} : domain propagation algorithm (AC3 [Mackworth,1977])

• Discarding values: local consistency + splitting

Universally Quantified Interval Constraint Solving – p. 8

Box consistency

[Benhamou, McAllester, Van Hentenryck, 1994] Given c a real constraint, C an interval extension for c, B = I_{1} × ⋯ × I_{n} a box

c is box-consistent w.r.t. B iff ∀k ∈ {1, …, n}: I_{k} = I_{k} ∩ {a_{k} ∈| C(I_{1}, …, I_{k−1}, {a_{k}}, I_{k+1}, …, I_{n})}

Box consistency operator:

B∩c ⊆ OCb_{c}(B) = max{B′ | B′ ⊆ B ∧cisbox − consistent B′} • Efficiency (systems of non-linear real equations with

punctual solutions)

• No restriction to polynomials

• Completeness: no solution lost But:

• Continuum of solutions? (systems of inequations)

• Soundness ?

• Quantified variables?

• Efficiency (systems of non-linear real equations with punctual solutions)

• No restriction to polynomials

• Completeness: no solution lost But:

• Continuum of solutions? (systems of inequations)

• Soundness ?

• Quantified variables?

Achieving soundness

Computing with interval constraint prog. techniques on ¬c: ⇒ completeness for ¬c ⇒ correctness for c For discarded box B = I_{1} × ⋯ × I_{n} × I_{v}: ¬(∃x_{1} … ∃x_{n}∃v: x_{1} ∈ I_{1} … x_{n} ∈ I_{n}v ∈ I_{v} ∧ ¬c(x_{1}, …, x_{n}, v))

That is: ∀x_{1} … ∀x_{n}∀v: x_{1} ∈ I_{1} … x_{n} ∈ I_{n}v ∈ I_{v} ⇒ c(x_{1}, …, x_{n}, v) (computation of inner approximation for c)

Negation of c: easy for inequations

Achieving soundness

Computing with interval constraint prog. techniques on ¬c: ⇒ completeness for ¬c ⇒ correctness for c For discarded box B = I_{1} × ⋯ × I_{n} × I_{v}: ¬(∃x_{1} … ∃x_{n}∃v: x_{1} ∈ I_{1} … x_{n} ∈ I_{n}v ∈ I_{v} ∧ ¬c(x_{1}, …, x_{n}, v))

That is: ∀x_{1} … ∀x_{n}∀v: x_{1} ∈ I_{1} … x_{n} ∈ I_{n}v ∈ I_{v} ⇒ c(x_{1}, …, x_{n}, v) (computation of inner approximation for c)

Negation of c: easy for inequations

Handling quantifiers

Solving ∀v ∈ I_{v}: c • Computing box consistency on ¬c

• Saving discarded boxes B′ = I′_{1} × ⋯ × I′_{n} × I′_{v} with I_{v} = I′_{v}

• Splitting undiscarded boxes and iterating Solving ∀v ∈ I^{1}: c_{1} ∧ ⋯ ∧ ∀v ∈ I^{m}: c_{m}

• Applying the previous scheme on c_{1}, …, c_{n} in sequence once

• Using the output after c_{i} as input for c_{i+1}

Universally Quantified Interval Constraint Solving – p. 12

Handling quantifiers

Solving ∀v ∈ I_{v}: c • Computing box consistency on ¬c

• Saving discarded boxes B′ = I′_{1} × ⋯ × I′_{n} × I′_{v} with I_{v} = I′_{v}

• Splitting undiscarded boxes and iterating Solving ∀v ∈ I^{1}: c_{1} ∧ ⋯ ∧ ∀v ∈ I^{m}: c_{m}

• Applying the previous scheme on c_{1}, …, c_{n} in sequence once

• Using the output after c_{i} as input for c_{i+1}

Universally Quantified Interval Constraint Solving – p. 12

Solving ∀v ∈ I_{v}: c

1 ICAb3_{c}(in: B ∈^{n}, v ∈; out: W ∈ n) 2 3 B’ cB 4 vB’=vB 5 D cB’ 6 W B′DvB′ 8 (D_{1}, D_{2}) vDvB’ 9 W W ∪ cD_{1}v ∪ cD_{2}v 10 11 W 12 14

Constraint systems and ∀

Solving ∀v ∈ I^{1}: c_{1} ∧ ⋯ ∧ ∀v ∈ I^{m}: c_{m}

1 ICAb5(in: = {(c_{1}, I^{1}), …, (c_{m}, I^{m})},

A ∈ n, v ∈; out: W ∈ n)

2 4 B∅

5 D ∈ A 7 B B ∪ c_{1}DvI^{1}, v 9 12 14 15 16 A 17 18

Properties

Given i, relation associated with ∀v ∈ I_{v}: c_{i} Soundness:

\begin{matrix}ICAb3_{c}(B, v) ⊆ Inner(B ∩ c) \\ ICAb5(, \{B\}, v) ⊆ Inner(B ∩ 1 ∩ ⋯ ∩ m) \end{matrix}

Comparison with EIA4: EIA4({c_{1}, …, c_{m}}, B, v) ⊆ ICAb5(S, {B}, v)

ICAb5 vs. EIA4

All solutions:

Benchmark  EIA4 ICAb5 EIA4/ICAb5
Projection_{3,5}  783  68  11
Projection_{3,10}  >9000 3634  >2
Projection_{5,5}  >9000 3612  >2
School Problem_{3,1}  156  13  12
Flying Saucer_{4,1}  1459 1078  1
Simple Circle_{2,1}  12789  651  19
Simple Circle_{2,2}  1579  56  28

Time in s. on a SUN UltraSparc 1/167 MHz.

N.B.: first solution only ⇒ speed-up much more important

Universally Quantified Interval Constraint Solving – p. 16

Conclusion and perspectives

Alg. ICAb5:

• solving of non-linear real constraints (polynomial or not) with one universally quantified variable per constraint

• Speed-up compared to splitting/evaluation (EIA4)

• Still costly

Solutions?

• More precise interval extensions (Bernstein)

• Other interval arithmetics (Kaucher/Markov, modal arithmetic)

• Cooperation of symbolic/numerical methods (CAD?)

Handling of constraints as full first-order expressions?

Universally Quantified Interval Constraint Solving

Frdric Benhamou and Frdric Goualard

Institut de Recherche en Informatique de Nantes, France

Interval constraint solving (2)

• Constraint system c_{1}, …, c_{m} : domain propagation algorithm (AC3 [Mackworth,1977])

Properties:

• Termination

• Contractance

• Confluency

• Completeness • Constraint system c_{1}, …, c_{m} : domain propagation

algorithm (AC3 [Mackworth,1977])

Properties:

• Termination

• Contractance

• Confluency

• Completeness • Constraint system c_{1}, …, c_{m} : domain propagation

algorithm (AC3 [Mackworth,1977])

Properties:

• Termination

• Contractance

• Confluency

• Completeness • Constraint system c_{1}, …, c_{m} : domain propagation

algorithm (AC3 [Mackworth,1977])

Properties:

• Termination

• Contractance

• Confluency

• Completeness • Constraint system c_{1}, …, c_{m} : domain propagation

algorithm (AC3 [Mackworth,1977])

Properties:

• Termination

• Contractance

• Confluency

• Completeness