Event Description
The Department of Computer Science at Drexel's College of Computing & Informatics (CCI) presents the Dr. Werner Krandick Lecture featuring Dr. Christopher Brown, professor of computer science at the United States Naval Academy.
Title: "Combining SAT/SMT and Computer Algebra to solve real polynomial constraints"
This event will be held in person and streamed online (please register via Zoom to receive online access).
Abstract:
One of the research problems that interested Werner Krandick the most was the efficient computation of real roots of univariate polynomials. This is a fundamental and important problem on its own, but it is also important as a tool for solving other problems. One motivation for Werner's work in this area was the importance of real root isolation as an engine for Cylindrical Algebraic Decomposition (CAD), an important technique in the field of Computer Algebra that is used to solve a variety of problems relating to real (multivariate) polynomial constraints, i.e. boolean combinations of sign conditions on multivariate polynomials. Recently, researchers in the field of Satisfiability Modulo Theory (SMT) solving have brought different algorithmic ideas to bear on the satisfiabilty problem for real polynomial constraints. This talk examines how the different approaches of these two communities have been combined to produce powerful new algorithms for computing with real (multivariate) polynomial constraints --- all relying on the "engine" of real root computation for univariate polynomials. |
