Unknot Recognition Through Quantifier Elimination

TL;DR

This paper presents a novel approach to unknot recognition by encoding it as a first-order theory validity problem and applying quantifier elimination, resulting in an algorithm with exponential complexity comparable to existing methods.

Contribution

It introduces a new encoding of unknot recognition as a real closed fields validity problem and develops an algorithm with similar complexity to current best methods.

Findings

The encoding leverages SU(2) representations of knot groups.

The proposed algorithm has complexity $2^{O(n)}$, matching existing algorithms.

The approach simplifies unknot recognition using quantifier elimination.

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(2) representations of knot groups by Kronheimer-Mrowka. We further show that applying existential quantifier elimination to the encoding enables an UnKnot Recogntion algorithm with a complexity of the order $2^{\mathcal{O}(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.