# Universally quantified interval constraint solving

**View the full content.**View Full Document

0 0 9 views

**Unformatted text preview:**

Universally Quantified Interval Constraint Solving Fre de ric Benhamou and Fre de ric Goualard Institut de Recherche en Informatique de Nantes France Universally Quantified Interval Constraint Solving p 1 Motivations x 3 sin cos sin cos 3 3 2 2 1 1 0 0 1 1 2 2 3 3 Object with trajectory y 3 sin cos sin cos z 0 Universally Quantified Interval Constraint Solving p 2 Motivations x 3 sin cos sin cos 3 3 3 2 2 1 1 0 0 1 1 2 2 Positions of a camera s t 0 5 at any time 3 Object with trajectory y 3 sin cos sin cos z 0 Universally Quantified Interval Constraint Solving p 2 Motivations x 3 sin cos sin cos 3 2 2 1 1 0 0 1 1 2 2 Positions of a camera s t 0 5 at any time 3 Object with trajectory y 3 sin cos sin cos z 0 3 sin cos sin cos x 2 3 sin cos sin cos y 2 z 2 3 3 0 5 Universally Quantified Interval Constraint Solving p 2 Motivations x 3 sin cos sin cos Object with trajectory y 3 sin cos sin cos z 0 Positions of a camera s t 0 5 at any time 3 sin cos sin cos x 2 3 sin cos sin cos y 2 z 2 0 5 Non linear real constraint compulsory to solve it soundly 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 Universally Quantified Interval Constraint Solving p 4 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 Universally Quantified Interval Constraint Solving p 4 Interval Arithmetic Moore 1966 Interval set I a b x R a 6 x 6 b Interval extension Extension of a real function f Rn R F In I s t B Df B F B 5 4 3 f 2 1 3 2 1 1 2 3 4 5 6 1 2 3 Extension of a real relation Rn Set of boxes R such that a1 an I1 In R s t a1 I1 an In Universally Quantified Interval Constraint Solving p 5 Approximation of a relation Outer approximation of Hull Inner approximation of Inner T B In B a Rn Hull a Splitting evaluation scheme SES for straightforward inner approximation computation Example c f x 6 0 5 4 3 f 2 1 3 2 1 1 2 3 4 5 6 1 2 3 D Universally Quantified Interval Constraint Solving p 6 Approximation of a relation Outer approximation of Hull Inner approximation of Inner T B In B a Rn Hull a Splitting evaluation scheme SES for straightforward inner approximation computation Example c f x 6 0 5 4 3 f 2 1 3 2 1 1 2 3 4 5 6 1 2 3 D Universally Quantified Interval Constraint Solving p 6 Approximation of a relation Outer approximation of Hull Inner approximation of Inner T B In B a Rn Hull a Splitting evaluation scheme SES for straightforward inner approximation computation Example c f x 6 0 5 4 3 f 2 1 3 2 1 1 2 3 4 5 6 1 2 3 D Universally Quantified Interval Constraint Solving p 6 Approximation of a relation Outer approximation of Hull Inner approximation of Inner T B In B a Rn Hull a Splitting evaluation scheme SES for straightforward inner approximation computation Example c f x 6 0 5 4 3 f 2 1 3 2 1 1 2 3 4 5 6 1 2 3 D Universally Quantified Interval Constraint Solving p 6 Approximation of a relation Outer approximation of Hull Inner approximation of Inner T B In B a Rn Hull a Splitting evaluation scheme SES for straightforward inner approximation computation Example c f x 6 0 5 4 3 f 2 1 3 2 1 1 2 3 4 5 6 1 2 3 D Universally Quantified Interval Constraint Solving p 6 EIA4 Jardillier Langu nou 1998 Modelling of camera movements Solving v a b c x v with the SES x a v b Universally Quantified Interval Constraint Solving p 7 EIA4 a x Jardillier Langu nou 1998 Modelling of camera movements Solving v a b c x v with the SES v b Universally Quantified Interval Constraint Solving p 7 EIA4 a x Jardillier Langu nou 1998 Modelling of camera movements Solving v a b c x v with the SES v b Universally Quantified Interval Constraint Solving p 7 EIA4 a x Jardillier Langu nou 1998 Modelling of camera movements Solving v a b c x v with the SES v b Universally Quantified Interval Constraint Solving p 7 EIA4 a x Jardillier Langu nou 1998 Modelling of camera movements Solving v a b c x v with the SES v b algorithm EIA4 very costly Universally Quantified Interval Constraint Solving p 7 Interval constraint solving Variables x1 xn domains D1 Dn Constraint c x1 xn contracting operator N c B ENHAMOU O LDER A PT D D1 D n N c D D Properties contractance monotony completeness c D N c D Constraint system c1 cm domain propagation algorithm AC3 M ACKWORTH 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 I1 In a box c is box consistent w r t B iff k 1 n Ik Hull Ik ak R C I1 Ik 1 Hull ak Ik 1 In 5 4 D0 3 f 2 1 3 2 1 1 1 2 3 4 5 6 2 Box consistency operator 3 D B c OCbc B max B B B c is box consistent w r t B Universally Quantified Interval Constraint Solving p 9 Interval constraint solving Efficiency systems of non linear real equations with punctual solutions No restriction to polynomials Completeness no solution lost Universally Quantified Interval Constraint Solving p 10 Interval constraint solving 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 Universally Quantified Interval Constraint Solving p 10 Achieving soundness Computing with interval constraint prog techniques on c completeness for c correctness for c For discarded box B I1 In Iv x1 xn v x1 I1 xn In v Iv c x1 xn v Universally Quantified Interval Constraint Solving p 11 Achieving soundness Computing with interval constraint prog techniques on c completeness for c correctness for c For discarded box B I1 In Iv x1 xn v x1 I1 xn In v Iv c x1 xn v That is x1 xn v x1 …