Solving parametric linear matrix inequalities

We consider linear matrices A = A0 + x1 A1 + & centerdot;& centerdot; & centerdot;+ xnAn,where the Ai's are m & times; m symmetric matrices with entries in a ring 7Z. When 7Z = & Ropf;, the feasibility problem consists in deciding whether the linear matrix inequality (LMI) A >= 0 is feasible, i.e., the xi's can be instantiated to obtain a positive semi-definite matrix. When 7Z = & Qopf;[y1, ... , yt], the problem asks for a formula on the parameters y1,...,yt, which describes the values of the parameters for which the specialized LMI is feasible. This problem can be solved using general quantifier elimination algorithms, with a complexity that is exponential in n. In this work, we leverage the LMI structure of the problem to design an algorithm that computes a formula Phi describing a dense subset of the feasible region of parameters. The complexity of this algorithm is exponential in n, m and t but becomes polynomial in n when m and tare fixed. We apply the algorithm to a parametric sum-of-squares problem and to the convergence analyses of certain first-order optimization methods. Both problems are known to be equivalent to the feasibility of certain parametric LMIs and lead instances which are out of reach of the previous state of the art. We demonstrate that our implementations of our algorithm can tackle these problems in practice, already for small values of n, m and t.