Unformatted text preview:

MIT 6 972 Algebraic techniques and semide nite optimization April 27 2006 Lecture 18 Lecturer Pablo A Parrilo Scribe Quanti er elimination QE is a very powerful procedure for problems involving rst order formulas over real elds The cylindrical algebraic decomposition CAD is a technique for the e cient im plementation of QE that e ectively reduces an seemingly in nite problem into a nite but potentially large instance For much more information about QE and CAD including a reprint of Tarski s original 1930 work we recommend the book CJ98 1 Quanti er elimination A quanti er free formula is an expression consisting of polynomial equations f x 0 and inequalities f x 0 combined using the Boolean operators and or and implies We often also allow strict inequalities f x 0 and inequations f x 0 since these are just shorthands for particular boolean combinations of equations and inequalities In general a formula in prenex form is an expression in the variables x x1 xn of the following type 1 Q1 x1 Qs xs F f1 x fr x where Qi is one of the quanti ers for all and there exists Furthermore F f1 x fr x is assumed to be a quanti er free formula If there is a quanti er corresponding to the variable xi we say that xi is quanti ed or free otherwise Example 1 The following are valid formulas x x 0 x2 ax b 0 x y x y 2 2 2 1 0 1 The rst formula has two free variables since the variables a and b are unquanti ed while for the other two all variables are quanti ed We will interpret the symbols in a formula as taking only real values Notice that a formula without free variables usualled called a closed formula or a sentence is either true or false For instance the last two expressions in Example 1 are sentences with the rst one being false and the second being true Notice also that the truth value may depend on the order of the quanti ers Tarski showed that for every formula including quanti ers there is always an equivalent quanti er free formula Obtaining the latter from the former is called quanti er elimination Theorem 2 Tarski Seidenberg For every rst order formula over the real eld there exists an equiv alent quanti er free formula Furthermore there is an explicit algorithm to compute this quanti er free formula The Tarski Seidenberg theorem is an extremely powerful result since it provides a complete charac terization and algorithmic technique for an extremely large collection of problems involving polynomials Unfortunately there are very serious computational barriers to the e cient practical implementation of these ideas since the resulting algorithms have extremely poor scaling properties with respect to the number of variables towers of exponentials Newer methods such as the partial cylindrical algebraic decomposition CAD technique due to Collins and described below or the critical point method are by comparison much better Nevertheless by necessity they still behave exponentially or worse in terms of the number of variables 18 1 2 Tarski Seidenberg Example 3 Consider the quanti ed rst order formula x y x2 ay 2 1 ax2 a2 xy 2 0 2 This formula is equivalent to the quanti er free expression a 0 a3 8a 16 0 which de nes the interval 0 a where a 3 538 Thus the original expression 2 is true only for a 0 a 2 1 Geometric interpretation A geometric interpretation of the Tarski Seidenberg theorem is the following Theorem 4 The projection of a semialgebraic set is semialgebraic 2 2 Applications Add many more ToDo Static output feedback An early application of Tarski Seidenberg in control theory was the so lution of the static output feedback stabilization problem in ABJ75 Given matrices A Rn n B Rn m we want to nd a matrix K Rm n such that the matrix A BK is Hurwitz i e all its eigenvalues are in the left hand plane Since the existence of such a matrix can be easily expressed as a formula in rst order logic1 the decidability and existence of an e ective but not e cient algorithm immediately follows Simultaneous stabilization A very interesting result by Blondel Blo94 BG93 shows that the si multaneous stabilization of three linear time invariant systems is not decidable and thus cannot be semialgebraic Notice however that for any given bound on the degree of the controller the problem is decidable 3 Cylindrical Algebraic Decomposition CAD There are a few approaches for e ective implementation of the QE procedure One of the most well known which is also relatively easy to understand is the cylindrical algebraic decomposition CAD due to Collins Col75 We describe the elements of this approach below We remark that much better algorithms in the theoretical complexity sense are known see for instance the article by Renegar Ren91 also reprinted in CJ98 or BPR03 In particular for CAD the number of operations usually scales in a doubly exponential fashion with the number of variables while the newer methods are doubly exponential in the number of quanti er alternations 1 For instance K x A BK x x x 0 0 Notice that we are being a bit sloppy with notation since for a fully real formulation we should split x and into real and imaginary parts There are many other equivalent expressions using for instance a Lyapunov equation or the Routh array 18 2 3 0 1 Description Given a set P of multivariate polynomials in n variables a CAD is a special partition of Rn into com ponents called cells over which all the polynomials have constant signs The algorithm for computing a CAD also provides a point in each cell called sample point which can be used to determine the sign of the polynomials in the cell A cell is called cylindrical if it has the form S Rk for some k n A decomposition of Rn is a CAD if all polynomials have constant sign on each cell and all cells are cylindrical The CAD associated to the formula 1 depends only on its quanti er free part F f1 x fr x Since all possible truth values of the formula are in correspondence with the values at the sample points we can use the CAD to evaluate its truth value and to perform quanti er elimination The basic CAD construction consists of two steps projection and lifting plus an additional third one if formula construction is desired In the rst projection phase we computes successive sets of polynomials in n 1 n 2 1 variables The main idea is given an input set of polynomials to compute at each step a new set of polynomials obtained by eliminating one variable at a time In general the elimination order does matter and a good choice leads to lower computational complexity The second


View Full Document

MIT 6 972 - Quantifier elimination

Download Quantifier elimination
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view Quantifier elimination and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Quantifier elimination 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?