Thomas Sturm
CNRS, France
Abstract
Subtropical real root finding is a heuristic method designed to solve large multivariate polynomials. This method considers the polynomial as a collection of exponent vectors associated with sign information on the coefficients. It employs linear programming to heuristically identify points where the values of the polynomial have opposite signs. In successful cases, the intermediate value theorem is utilized to compute a zero of the polynomial represented as a tuple of real algebraic numbers. By implementing this approach using the Reduce computer algebra system and the
Gurobi LP solver, we have achieved success in solving hundreds of problems derived from established mathematical models in chemistry and systems biology. These problems involved polynomials with up to 800,000 monomials in 10 variables and degrees up to 12, with an incompleteness failure rate of approximately 10 percent.
The method has been adapted to satisfiability modulo theories solving (SMT), where the focus went from one single polynomial equation to several simulteneous strict polynomial inequalities. We found that such problems represent more than 40 percent of the QF_NRA section of the SMT-LIB library of benchmarks. Technically, input problems in the theory QF_NRA are reduced problems in QF_LRA. Then SMT itself can be used in place of LP solving, which admits linear problems that are not necessarily pure conjunctions of constraints. Systematic experiments on the SMT-LIB have shown that the method is not a sufficiently strong decision procedure by itself but a valuable heuristic to use within a portfolio of techniques.
The talk gives an overview of the method and its application, along with theoretical results regarding its incompleteness.
Short bio
Thomas Sturm studied computer science at the University of Passau, Germany, where he held positions as a researcher and faculty member (Privatdozent) after finishing his studies in 1995. In 2008 he was awarded a Ramón y Cajal Fellowship by the Spanish Ministry of Science and Innovation and moved to the University of Cantabria in Santander. In 2011 he joined the MPI for Informatics in Saarbrücken, Germany, where he headed a research group for Arithmetic Reasoning. In 2016 he was appointed as a research director at French CNRS. Sturm has worked as a visiting researcher at various international institutes and research facilities including SRI International in Menlo Park, Zuse Institute Berlin, Fujitsu Laboratories Japan, Lomonosov Moscow State University, and Forschungszentrum Jülich. Sturm is an editor at the Journal of Symbolic Computation (Elsevier) and at Mathematics in Computer Science (Springer).
Sturm’s research interests span the domains of exact and efficient computation, computer algebra, logic, and formal reasoning. This includes the development of effective quantifier elimination methods and decision procedures for various algebraic theories, their efficient implementation, and their application in the sciences and in engineering. On the foundational side, he is working on methods from tropical algebra in a liberal sense with strong focus on the real numbers as the domain of interest. His methods are used in SMT solving and in mathematical biology. On the applied side, one focus is interdisciplinary research on specialized decision methods for the qualitative analysis of dynamic properties of reaction systems in chemistry and systems biology.