×

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
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] 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
[2] 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
[3] 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
[4] Cauchy, A. L.B., Calcul des indices des fonctions, J. Éc. Polytech., 15, 25, 176-229, (1832)
[5] 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
[6] 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
[7] Coq, The Coq Proof Assistant, (2016)
[8] Gathen, J.; Gerhard, J., Modern Computer Algebra, (1999), Cambridge University Press: Cambridge University Press New York, NY, USA · Zbl 0936.11069
[9] Girard, A., Invention nouvelle en l’algébre, (1629), Blauew
[10] 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
[11] 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
[12] 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)
[13] 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
[14] 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
[15] 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
[16] Henrion, D.; Naldi, S.; Safey El Din, M., Spectra—a maple library for solving linear matrix inequalities in exact arithmetic, (2016), ArXiv preprint
[17] Higham, N., Accuracy and Stability of Numerical Algorithms, (2002), SIAM · Zbl 1011.65010
[18] Hong, H.; Safey El Din, M., Variant quantifier elimination, J. Symb. Comput., 47, 7, 883-901, (2012) · Zbl 1238.14001
[19] 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
[20] Knapp, A. W., Basic Algebra, (2006), Birkhäuser Basel · Zbl 1106.00001
[21] Landau, E., Über die darstellung definiter funktionen durch quadrate, Math. Ann., 62, 272-285, (1906) · JFM 37.0252.01
[22] Lasserre, J.-B., Global optimization with polynomials and the problem of moments, SIAM J. Optim., 11, 3, 796-817, (2001) · Zbl 1010.90061
[23] Lickteig, T.; Roy, M.-F., Sylvester-Habicht sequences and fast Cauchy index computation, J. Symb. Comput., 31, 3, 315-341, (2001) · Zbl 0976.65043
[24] Magron, V.; Allamigeon, X.; Gaubert, S.; Werner, B., Formal proofs for nonlinear optimization, J. Formaliz. Reason., 8, 1, 1-24, (2015)
[25] 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)
[26] 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
[27] Mignotte, M., Mathematics for Computer Algebra, (1992), Springer-Verlag New York, Inc.: Springer-Verlag New York, Inc. New York, NY, USA
[28] 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
[29] Parrilo, P., Structured Semidefinite Programs and Semialgebraic Geometry Methods in Robustness and Optimization, (2000), California Institute of Technology, Ph.D. thesis
[30] Peyrl, H.; Parrilo, P., Computing sum of squares decompositions with rational coefficients, Theor. Comput. Sci., 409, 2, 269-281, (2008) · Zbl 1156.65062
[31] 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
[32] Prestel, A.; Delzell, C., Positive Polynomials: From Hilbert’s 17th Problem to Real Algebra, Springer Monogr. Math, (2001), Springer Berlin Heidelberg · Zbl 0987.13016
[33] 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
[34] 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
[35] Schweighofer, M., Algorithmische Beweise für Nichtnegativ- und Positivstellensätze, (1999), Diplomarbeit an der Universität Passau, Master’s thesis
[36] 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
[37] Swokowski, W., Fundamentals of College Algebra, 216-221, (1989), PWS-Kent Pub. Co.
[38] Volkova, A.; Lauter, C.; Hilaire, T., Reliable verification of digital implemented filters against frequency specifications, (24th IEEE Symposium on Computer Arithmetic, (2017), IEEE)
[39] 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.