# zbMATH — the first resource for mathematics

Algorithms for weighted sum of squares decomposition of non-negative univariate polynomials. (English) Zbl 1420.13058
Summary: It is well-known that every non-negative univariate real polynomial can be written as the sum of two polynomial squares with real coefficients. When one allows a (non-negatively) weighted sum of finitely many squares instead of a sum of two squares, then one can choose all coefficients in the representation to lie in the field generated by the coefficients of the polynomial. In particular, this allows for an effective treatment of polynomials with rational coefficients.
In this article, we describe, analyze and compare, from both the theoretical and practical points of view, two algorithms computing such a weighted sum of squares decomposition for univariate polynomials with rational coefficients.
The first algorithm, due to the third author, relies on real root isolation, quadratic approximations of positive polynomials and square-free decomposition, but its complexity was not analyzed. We provide bit complexity estimates, both on the runtime and the output size of this algorithm. They are exponential in the degree of the input univariate polynomial and linear in the maximum bitsize of its complexity. This analysis is obtained using quantifier elimination and root isolation bounds.
The second algorithm, due to Chevillard, Harrison, Joldes and Lauter, relies on complex root isolation and square-free decomposition, and was introduced for certifying positiveness of polynomials in the context of computer arithmetic. Again, its complexity was not analyzed. We provide bit complexity estimates, both on the runtime and the output size of this algorithm, which are polynomial in the degree of the input polynomial and linear in the maximum bitsize of its complexity. This analysis is obtained using Vieta’s formula and root isolation bounds.
Finally, we report on our implementations of both algorithms and compare them in practice on several application benchmarks. While the second algorithm is, as expected from the complexity result, more efficient on most of examples, we exhibit families of non-negative polynomials for which the first algorithm is better.

##### MSC:
 13J30 Real algebra 14P10 Semialgebraic sets and related spaces 13P10 Gröbner bases; other bases for ideals and modules (e.g., Janet and border bases) 68W40 Analysis of algorithms 68W30 Symbolic computation and algebraic computation
##### Software:
Coq; HOL Light; kepler98; mctoolbox; PARI/GP; RAGlib; SDPA; SPECTRA; univsos
Full Text:
##### References:
  Basu, S.; Pollack, R.; Roy, M.-F., On the combinatorial and algebraic complexity of quantifier elimination, J. ACM, 43, 6, 1002-1045, (1996) · Zbl 0885.68070  Basu, S.; Pollack, R.; Roy, M.-F., Algorithms in Real Algebraic Geometry, Algorithms Comput. Math., (2006), Springer-Verlag New York, Inc.: Springer-Verlag New York, Inc. Secaucus, NJ, USA  Boudaoud, F.; Caruso, F.; Roy, M.-F., Certificates of positivity in the Bernstein basis, Discrete Comput. Geom., 39, 4, 639-655, (2008) · Zbl 1141.14035  Cauchy, A. L.B., Calcul des indices des fonctions, J. Éc. Polytech., 15, 25, 176-229, (1832)  Chevillard, S.; Harrison, J.; Joldes, M.; Lauter, C., Efficient and accurate computation of upper bounds of approximation errors, Theor. Comput. Sci., 412, 16, 1523-1543, (2011) · Zbl 1211.65025  Collins, G. E., Quantifier elimination for real closed fields by cylindrical algebraic decomposition, (Automata Theory and Formal Languages 2nd GI Conference. Automata Theory and Formal Languages 2nd GI Conference, Kaiserslautern, May 20-23, 1975, (1975), Springer), 134-183  Coq, The Coq Proof Assistant, (2016)  Gathen, J.; Gerhard, J., Modern Computer Algebra, (1999), Cambridge University Press: Cambridge University Press New York, NY, USA · Zbl 0936.11069  Girard, A., Invention nouvelle en l’algébre, (1629), Blauew  Greuet, A.; Safey El Din, M., Probabilistic algorithm for polynomial optimization over a real algebraic set, SIAM J. Optim., 24, 3, 1313-1343, (2014) · Zbl 1327.90232  Guo, Q.; Safey El Din, M.; Zhi, L., Computing rational solutions of linear matrix inequalities, (Proceedings of the 38th International Symposium on Symbolic and Algebraic Computation. Proceedings of the 38th International Symposium on Symbolic and Algebraic Computation, ISSAC ’13, (2013), ACM: ACM New York, NY, USA), 197-204 · Zbl 1360.68934  Hales, T.; Adams, M.; Bauer, G.; Dat, D. T.; Harrison, J.; Truong, H. L.; Kaliszyk, C.; Magron, V.; Mclaughlin, S.; Thang, N. T.; Truong, N. Q.; Nipkow, T.; Obua, S.; Pleso, J.; Rute, J.; Solovyev, A.; An, T. T.H.; Trung, T. N.; Diep, T. T.; Urban, J.; Ky, V. K.; Zumkeller, R., A formal proof of the Kepler conjecture, Forum Math., Pi, 5, (2017)  Harrison, J., HOL Light: a tutorial introduction, (Srivas, M. K.; Camilleri, A. J., FMCAD. FMCAD, Lect. Notes Comput. Sci., vol. 1166, (1996), Springer), 265-269  Harrison, J., Verifying nonlinear real formulas via sums of squares, (Proceedings of the 20th International Conference on Theorem Proving in Higher Order Logics. Proceedings of the 20th International Conference on Theorem Proving in Higher Order Logics, TPHOLs’07, (2007), Springer-Verlag: Springer-Verlag Berlin, Heidelberg), 102-118 · Zbl 1144.68357  Henrion, D.; Naldi, S.; Safey El Din, M., Exact algorithms for linear matrix inequalities, SIAM J. Optim., 26, 4, 2512-2539, (2016) · Zbl 1356.90102  Henrion, D.; Naldi, S.; Safey El Din, M., Spectra—a maple library for solving linear matrix inequalities in exact arithmetic, (2016), ArXiv preprint  Higham, N., Accuracy and Stability of Numerical Algorithms, (2002), SIAM · Zbl 1011.65010  Hong, H.; Safey El Din, M., Variant quantifier elimination, J. Symb. Comput., 47, 7, 883-901, (2012) · Zbl 1238.14001  Kaltofen, E. L.; Li, B.; Yang, Z.; Zhi, L., Exact certification in global polynomial optimization via sums-of-squares of rational functions with rational coefficients, J. Symb. Comput., 47, 1, 1-15, (2012) · Zbl 1229.90115  Knapp, A. W., Basic Algebra, (2006), Birkhäuser Basel · Zbl 1106.00001  Landau, E., Über die darstellung definiter funktionen durch quadrate, Math. Ann., 62, 272-285, (1906) · JFM 37.0252.01  Lasserre, J.-B., Global optimization with polynomials and the problem of moments, SIAM J. Optim., 11, 3, 796-817, (2001) · Zbl 1010.90061  Lickteig, T.; Roy, M.-F., Sylvester-Habicht sequences and fast Cauchy index computation, J. Symb. Comput., 31, 3, 315-341, (2001) · Zbl 0976.65043  Magron, V.; Allamigeon, X.; Gaubert, S.; Werner, B., Formal proofs for nonlinear optimization, J. Formaliz. Reason., 8, 1, 1-24, (2015)  Mehlhorn, K.; Sagraloff, M.; Wang, P., From approximate factorization to root isolation with application to cylindrical algebraic decomposition, J. Symb. Comput., 66, 34-69, (Jan. 2015)  Melczer, S.; Salvy, B., Symbolic-numeric tools for analytic combinatorics in several variables, (Proceedings of the ACM on International Symposium on Symbolic and Algebraic Computation. Proceedings of the ACM on International Symposium on Symbolic and Algebraic Computation, ISSAC ’16, (2016), ACM: ACM New York, NY, USA), 333-340 · Zbl 1360.68945  Mignotte, M., Mathematics for Computer Algebra, (1992), Springer-Verlag New York, Inc.: Springer-Verlag New York, Inc. New York, NY, USA  Nakata, M., A numerical evaluation of highly accurate multiple-precision arithmetic version of semidefinite programming solver: SDPA-GMP, -QD and -DD, (Computer-Aided Control System Design, 2010 IEEE International Symposium on. Computer-Aided Control System Design, 2010 IEEE International Symposium on, CACSD, (Sept 2010)), 29-34  Parrilo, P., Structured Semidefinite Programs and Semialgebraic Geometry Methods in Robustness and Optimization, (2000), California Institute of Technology, Ph.D. thesis  Peyrl, H.; Parrilo, P., Computing sum of squares decompositions with rational coefficients, Theor. Comput. Sci., 409, 2, 269-281, (2008) · Zbl 1156.65062  Pourchet, Y., Sur la représentation en somme de carrés des polynômes à une indéterminée sur un corps de nombres algébriques, Acta Arith., 19, 1, 89-104, (1971) · Zbl 0244.10019  Prestel, A.; Delzell, C., Positive Polynomials: From Hilbert’s 17th Problem to Real Algebra, Springer Monogr. Math, (2001), Springer Berlin Heidelberg · Zbl 0987.13016  Rantzer, A.; Parrilo, P. A., On convexity in stabilization of nonlinear systems, (Proceedings of the 39th IEEE Conference on Decision and Control, vol. 3, (2000)), 2942-2945  Safey El Din, M.; Zhi, L., Computing rational points in convex semialgebraic sets and sum of squares decompositions, SIAM J. Optim., 20, 6, 2876-2889, (2010) · Zbl 1279.90127  Schweighofer, M., Algorithmische Beweise für Nichtnegativ- und Positivstellensätze, (1999), Diplomarbeit an der Universität Passau, Master’s thesis  Strzebonski, A.; Tsigaridas, E., Univariate real root isolation in an extension field, (Proceedings of the 36th International Symposium on Symbolic and Algebraic Computation. Proceedings of the 36th International Symposium on Symbolic and Algebraic Computation, ISSAC ’11, (2011), ACM: ACM New York, NY, USA), 321-328 · Zbl 1323.68628  Swokowski, W., Fundamentals of College Algebra, 216-221, (1989), PWS-Kent Pub. Co.  Volkova, A.; Lauter, C.; Hilaire, T., Reliable verification of digital implemented filters against frequency specifications, (24th IEEE Symposium on Computer Arithmetic, (2017), IEEE)  Yun, D. Y., On square-free decomposition algorithms, (Proceedings of the Third ACM Symposium on Symbolic and Algebraic Computation. Proceedings of the Third ACM Symposium on Symbolic and Algebraic Computation, SYMSAC ’76, (1976), ACM: ACM New York, NY, USA), 26-35
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.