Proving and solving semi-definite . . .

Semidefinite Programming (SDP) is a class of convex optimization problems with a linear objective function and linear matrix inequality (LMI) constraints. SDP problems have many applications in engi-neering and applied mathematics. We propose a reasonably fast algorithm to prove and solve SDP exactly by exploiting the convexity of the SDP feasibility domain. This is achieved by combining a symbolic algorithm of cylindrical algebraic decomposition (CAD) and a lifting strategy that takes into account the convexity properties of SDP. The effectiveness of our method is examined by applying it to some examples on QEPCAD and maple