Quantifier Elimination versus Generalized Interval Evaluation A comparison on a Special Cla.pdfVIP

Quantifier Elimination versus Generalized Interval Evaluation: A Comparison on a Specific Class of Quantified Constraints Carlos Grand´on Alexandre Goldsztejn Projet COPRIN, INRIA (Sophia-Antipolis) University of Nice–Sophia-Antipolis Carlos.Grandon@sophia.inria.fr Alexandre@G Abstract is coupled with a bisection algorithm, an accu- rate reliable outer approximation of the solu- This paper presents and compares tion set of a numerical Constraint Satisfaction two methods for checking if a box is Problem (CSP) can be achieved ([8]). How- included inside the solution set of an ever, when the solution set has a non-null (hy- equality constraint with existential per)volume, such a branch and prune algo- quantification of its parameters. We rithm will bisect again and again the boxes focus on distance constraints, where included inside the solution set, leading to in- each existentially quantified parame- efficient computations. This situation can be ter has only one occurrence, because strongly improved using a test for detecting of their usefulness and their simplic- inner boxes so that boxes which are proved ity. The first method relies on a to lie inside the solution set will not be bi- specific quantifier elimination based sected any more. Furthermore, in addition on geometric considerations whereas to the speedup of computations, such inner the second method relies on compu- boxes often have interesting interpretations. tations with gene