Unknot Recognition Through Quantifier Elimination

Authors: Meesum Syed Mohammad and Prathamesh T. V. H.

Paper Information

Title:Unknot Recognition Through Quantifier Elimination
Authors:Meesum Syed Mohammad and Prathamesh T. V. H.
Proceedings:SCSC Papers
Editors: Anna Maria Bigatti and Martin Brain
Keywords:real algebraic geometry, knot theory, algorithms, logic, symbolic computation, SMT solving

ABSTRACT. Unknot recognition is one of the fundamental questions in low dimensional topology. In this work, we show that this problem can be encoded as a validity problem in the existential fragment of the first-order theory of real closed fields. This encoding is derived using a well-known result on \su representations of knot groups by Kronheimer-Mrowka. We further show that applying existential quantifier elimination to the encoding enables an \unknot algorithm with a complexity of the order $2^{\OO(n)}$, where $n$ is the number of crossings in the given knot diagram. Our algorithm is simple to describe and has the same runtime as the currently best known unknot recognition algorithms. This leads to an interesting class of problems, of interest to both SMT solving and knot theory.

Talk:Jul 11 17:00 (Session 67F: Research papers)