=Paper=
{{Paper
|id=Vol-2189/paper8
|storemode=property
|title=Unknot Recognition Through Quantifier Elimination
|pdfUrl=https://ceur-ws.org/Vol-2189/paper8.pdf
|volume=Vol-2189
|authors=Meesum Syed Mohammad,Prathamesh T. V. H.
|dblpUrl=https://dblp.org/rec/conf/scsquare/MeesumP18
}}
==Unknot Recognition Through Quantifier Elimination==
https://ceur-ws.org/Vol-2189/paper8.pdf
Unknot Recognition Through Quantifier
Elimination
Syed M. Meesum1[0000−0002−1771−403X] and T. V. H.
Prathamesh2[0000−0003−3842−3626]
1
Institute of Computer Science,University of Wroclaw, Poland
2
Department of Computer Science,University of Innsbruck, Austria
meesum.syed@gmail, prathamesh.t@gmail.com
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 Recognition algorithm with a complexity
of the order 2O(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.
Keywords: real algebraic geometry, knot theory, algorithms, symbolic compu-
tation, SMT solving.
1 Introduction
In mathematics, a knot refers to an entangled loop. The fundamental problem
in the study of knots is the question of knot recognition: can two given knots
be transformed to each other without involving any cutting and pasting? This
problem was shown to be decidable by Haken in 1962 [7] using the theory of
normal surfaces. We study the special case in which we ask if it is possible to
untangle a given knot to an unknot. The UnKnot Recognition recognition
algorithm takes a knot presentation as an input and answers Yes if and only if
the given knot can be untangled to an unknot. The best known complexity of
UnKnot Recognition recognition is 2O(n) , where n is the number of crossings
in a knot diagram [2,7].
More recent developments show that the UnKnot Recognition recogni-
tion is in NP ∩ co-NP. Using the theory of normal surfaces, Hass, Lagarias and
Pippenger [8] proved existence of an NP membership certificate for UnKnot
Recognition. A notion which is closer to the commonly accepted notion of
untangling a knot is that of using Reidemeister moves. The existence of a polyno-
mial length sequence of Reidemeister moves having size O(n11 ), that untangles
78 S. M. Meesum and T. V. H. Prathamesh
an unknot, was proved to exist by Lackenby [12]. Searching over all possible
Reidemeister moves will give a simple to describe algorithm having runtime of
11
2O(n ) . According to Lackenby [12], a proof sketch for co-NP membership of
UnKnot Recognition was first announced by Agol, but not written down
in detail. Assuming the Generalized Reimann Hypothesis, a polynomial-time
certificate for non-membership of a knot in UnKnot Recognition was proved
to exist by Kuperberg [11]. Finally, an unconditional proof for the membership
of UnKnot Recognition in co-NP was given by Lackenby [13].
Several approaches to unknot recognition can be found in literature, such as
a complete knot invariant such as Khovanov homology, branching algorithms [2]
involving normal surface theory, manifold hierarchies[13], Dynnikov diagrams [4],
equational reasoning [5], and automated reasoning[15].
Most of the known algorithms deciding UnKnot Recognition are complex
and have an involved analysis. There are few implementations of this algorithm.
One of the implementations is known to show polynomial time behaviour to
recognize an unknot, but behaves exponentially to detect that a given diagram
represents a knotted knot. [2]
The authors believe that this paper presents a simpler alternate algorithm,
which relies on reducing the above problem to a sentence in the existential theory
of reals [17]. This enables application of the decision procedure for existential
theory of reals using quantifier elimination, to obtain an algorithm which is
exponential in complexity, thus of the same complexity class as the best known
approaches. The algorithm presented in this paper has not yet been implemented.
Acknowledgments: The authors would like to thank the Institute of Mathe-
matical Sciences, HBNI, Chennai, India, where a part of the work was carried out.
The first author is supported by the NCN grant number 2015/18/E/ST6/00456.
The second author is supported by the FWF project number P30301.
2 Preliminaries
This section contains some of the basic definitions in knot theory, and a brief
note on quantifier elimination and existential theory of reals without explicitly
stating the algorithm. For a more detailed introduction to knot theory one may
refer to [18,3,14,9], and for quantifier elimination in existential theory of reals,
one may refer to [6] [1].
For a natural number n, we use [n] to denote the set {1, 2, . . . , n}. We use
SU(2) to denote the group which contains 2 × 2 complex hermitian matrices
with unit determinant, with multiplication as the group operation. For a natural
number d, we use S d to denote d
√ the subset of R with euclidean norm equal to
one. The symbol i denotes −1, the imaginary root of unity. The symbol ∧ is
used to denote the operation of logical conjunction. The symbol ∨ is used to
denote the operation of logical disjunction.
Unknot Recognition Through Quantifier Elimination 79
2.1 Knot Theory
Basic Definitions
Definition 1. A (tame) knot K is the image of a smooth injective map from S 1
to S 3 .
Remark 1. S 3 in the above definition can be replaced by R3 . But we use S 3 ,
because some of the concepts that we introduce such as knot groups, exist only
in the context of the embedding of a circle in S 3 .
Two knots are considered to be the same, if they are related by an equivalence
condition called ambient isotopy. It is defined as follows:
Definition 2 (Ambient Isotopy). The knots K1 and K2 are ambient isotopic
if there exists a smooth map F : S 3 × [0, 1] → S 3 such that:
– ∀x ∈ S 3 . F (x, 0) = x.
– F (K1 , 1) = K2 .
– ∀t ∈ [0, 1]. F (S 3 , t) is a homeomorphism of S 3 .
Ambient isotopy describes when a knot can be transformed into another by
a deformation that does not involve any cutting and pasting. To draw a knot
on paper, we use the convention that wherever the string is shown broken it
is assumed to be passing under the unbroken string. To illustrate the above
condition, consider the following knots:
1) Unknot 2) A Twist 3) Trefoil Knot
The first two knot diagrams shown above can be deformed into each other by
twisting/untwisting, thus they represent the same knot. Deforming either of the
first two knots into the third knot, would involve cutting and pasting. Thus it is
different from the former knots.
Definition 3. An unknot is a knot which is ambient isotopic to the circle S 1 .
A knot k is knotted if and only if it is not an unknot.
Determining when two diagrams represent the same knot, is the key problem
of knot theory. The special case of it, determining when a given knot diagram is
equivalent to unknot is called the unknot recognition problem. There have been
several algorithms and approaches to the knot recognition, listed in the previous
section.
80 S. M. Meesum and T. V. H. Prathamesh
Knot Group One of the known invariants of knots is the fundamental group
of the knot complement. Knot complement refers to the compact 3-manifold
obtained by considering the complement of a tubular neighbourhood of the knot.
This invariant can detect knots up to mirror image. Presentations of this group,
called the Wirtinger presentation, can be easily computed from a knot diagram
in the following manner:
– The knot diagram is oriented in one of the two possible directions. The string
constituting the knot is given a direction which fixes the direction of all the
arcs occurring in the knot diagram.
– Every connected arc is associated to a distinct generator.
– Every crossing gives rise to a relation in the presentation. The relation
depends on the orientation of the arcs in the crossing, in the manner as shown
in Figure 1.
Computing the Wirtinger presentation of a group from the diagram can be
achieved using the steps described above in time which is a linear function of the
number of crossings in the given knot diagram.
SU(2) representations of the knot group The following theorem by Kron-
heimer - Mrowka, translates unknot recoginition to existence of non-commutative
SU(2) representations of the knot group.
Proposition 1 ([10], [11]). If K is knotted, then it has an non-commutative
SU(2) representations of the knot group π1 (S 3 \ K).
The following lemma is derived from the theorem above. The reverse direction of
the lemma follows from the fact the knot group of the unknot is Z, and all its
SU(2) representations are commutative.
Lemma 1. A knot K is knotted if and only if there exists a non-commutative
SU(2) representation of the knot group π1 (S 3 \ K).
We note that every finitely presented group has a trivial homomorphism to the
group SU(2) via a mapping of each generator to the identity matrix.
xk xk+1
xj xj xj xj
xk+1 xk
xjxkxj-1 = xk+1 xj-1xkxj = xk+1
Fig. 1. Wirtinger presentation relations for the knot group.
Unknot Recognition Through Quantifier Elimination 81
2.2 Quantifier Elimination in Existential Theory of Reals
Decidability of the first-order existential theory of reals refers to the existence of
a decision procedure for validity of all sentences of the form:
∃X̄. F (X̄),
where F is any quantifier free formula of polynomial equalities and inequalities
in real variables X̄. It follows from the Tarski-Seidenberg theorem that the
problem above is decidable by a quantifier elimination algorithm. The quantifier
elimination in this case, in fact holds true for deciding validity of all first-order
sentences. Quantifier elimination algorithm refers to computation of a quantifier
free sentence, which is equivalent to the sentence with quantifiers. Validity of
the quantifier free sentences can be computed, which makes the algorithm a
decision procedure for the first-order theory. Quantifier elimination algorithm in
the existential fragment is restricted to finding equivalent quantifier free sentences
only for first-order sentences with existential quantifiers, of the form described
above.
The known complexity bounds for the quantifier elimination in the general
first-order theory of reals are doubly exponential. The existential fragment has
a much lower complexity bound and there are several algorithms for it. Our
analysis will be based on the following result:
Proposition 2 (see Proposition 4.2 in [17]). Given a set P of equations,
each of which is either a ` polynomial equalities or inequality of degree d in k
variables, and with integer coefficients of bit length L, we can decide the feasibility
of P with L log L log log L(` · d)O(k) bit operations.
3 Algorithm
The algorithm Unknot-QE appears as Algorithm 1 on the next page.
Remark 2. The algorithm can be simplified leading to improvements in efficiency,
within the same complexity class, but our choice of description is motivated by
expository concerns.
The key idea behind the algorithm can be stated in terms of the following
theorem which will be proved in the next section.
Theorem 1. There exists a computable map Φ, which takes a knot diagram
K to a sentence in the existential fragment of the first order theory of reals. A
knot K is knotted if and only if Φ(K) is valid. Moreover, applying an existential
quantifier elimination algorithm to Φ(K) leads to a decision method for UnKnot
Recognition.
82 S. M. Meesum and T. V. H. Prathamesh
Algorithm: Unknot-QE
Input: A knot group π1 (S 3 \ K) = h g1 , g2 , . . . , gn | R1 , R2 , . . . , Rn i
Output: Output Yes if K is an unknot, otherwise output No
1 begin
2 E ←− ∅
3 P ←− ∅
4 for k ← 1 to n do
ak + ibk ck + idk
5 Mk ←−
−ck + idk ak − ibk
6 end for
7 for k ← 1 to n do
8 if Rk = gj gk gj−1 gk+1
−1
then
9 Ek ←− Mk+1 Mj − Mj Mk
10 end if
11 if Rk = gj−1 gk gj gk+1
−1
then
12 Ek ←− Mk Mj − Mj Mk+1
13 end if
/* the real part of the entries of the first row of Ek */
14 EkRe ←− ReU (Ek )
/* the complex part of the entries of the first row of Ek */
15 EkIm ←− ImU (Ek )
16 Put all the polynomials in EkRe and EkIm in the set P
17 Put a2k + b2k + c2k + d2k − 1 in P
18 end for
Put the equation p∈P p2 = 0 in E
P
19
20 N ←− ∅
21 for k ← 2 to n do
22 Put ak − a1 , bk − b1 , ck − c1 and dk − d1 in N
23 end for
Put the inequality p∈N p2 6= 0 in E
P
24
25 if E is satisfiable then
26 return Yes
27 else
28 return No
29 end if
30 end
Algorithm 1: Description of the algorithm for Unknot detection.
Unknot Recognition Through Quantifier Elimination 83
4 Proof of the Algorithm
In the proof, we reduce the Kronheimer-Mrowka property, stated in Section
2.1, to a first-order sentence in the existential theory of quantifier elimination.
Observe that every knot group has Wirtinger presentations which correspond to
knot diagrams. These presentations are of the following form:
h g1 , g2 , . . . , gn | R1 , R2 , . . . , Rn i.
For i ∈ [n], the symbol gi denotes a generator of the group and Ri denotes a
relation satisfied by the generators. In the Wirtinger presentation, each Rk is
either gj gk gj−1 gk+1
−1
or gj−1 gk gj gk+1
−1
, where j ∈ [n] and depends on k, we use
+(Rk ) or −(Rk ) to denote them respectively.
Finding a non-commutative SU(2) representation of π1 (S 3 \ K), if it exists,
can be seen as a conjunction of the following steps:
1. Mapping generators of the Wirtinger presentation to matrices in SU(2).
2. Checking that the above map extends to a well defined homomorphism, i.e.
the matrices corresponding to generators satisfy the generating relations of
the Wirtinger presentation.
3. Checking that the map is non-commutative.
In the following paragraphs, we elaborate on and construct equivalent con-
ditions for each of the above steps. Let gk be a generator in the Wirtinger
presentation, associated to a knot diagram. Consider a map Φ from the set of
generators to M, in which we map gk to Mk .
ak + ibk ck + idk
Mk = (1)
−ck + idk ak − ibk
Here ak , bk , ck , dk are real variables. For Mk to be an element of SU(2), it must
be unitary (i.e. the inverse of Mk is equal to transpose of its complex-conjugate)
and it must have unit determinant, which gives us the following extra condition
on the variables used to define it.
Observation 2 (folklore) Mk ∈ SU(2) if and only if (a2k + b2k + c2k + d2k = 1).
In addition, the mapped elements Mk ’s have to satisfy the knot group relations
obtained from the Wirtinger presentation i.e.
(+(Rk ) → Mj Mk Mj−1 Mk+1
−1
= I) ∧ (−(Rk ) → Mj−1 Mk Mj Mk+1
−1
= I) (2)
where I is the 2 × 2 identity matrix.
For k ∈ [n], we define Ek as follows:
(
Mk+1 Mj − Mj Mk +(Rk )
Ek =
Mk Mj − Mj Mk+1 −(Rk )
The condition on matrices in Equation (2) can be restated in terms ot Ek as
follows:
84 S. M. Meesum and T. V. H. Prathamesh
Observation 3 For Mk ∈ SU(2), for i ∈ [n], a knot group embedding must
00
satisfy Ek = .
00
The above observation meets the goal of step (2). The above matrix equality
can be rewritten as a system of four quadratic equations in real variables in the
following fashion:
– Decompose the matrix Ek into real and imaginary parts – Re(Ek ) and
Im(Ek ): then Ek = 0 if and only if Re(Ek ) = 0 and Im(Ek ) = 0.
– Define ReU (Ek ) and ImU (Ek ) to be the sets of polynomial equalities:
p(x) = 0,
where p(x) is an entry in the top row of the Re(Ek ) and Im(Ek ) respectively.
We similarly define ReD (Ek ) and ImD (Ek ) for the bottom row. Either by
simplifying Ek or by noticing the fact that the matrices Mk form a group
and their product matrix must also be of the same form as Equation (1), one
can observe that:
ReU (Ek ) ∪ ImU (Ek ) = ReD (Ek ) ∪ ImU (Ek ).
Consider the set P, consisting of all the polynomials ReU (Ek ), ImU (Ek ) and
ak + b2k + c2k + d2k − 1 = 0, where k ∈ [n]. The following lemma allows us to
2
decrease the number of equalities we have in the system of equations.
Lemma 2 (Reverse Rabinoswitch Encoding [16]).
Let P = {p1 = 0, . . . , pm = 0} be the system of m equality constraints,
P as defined
above. Then p1 = 0 ∧ p2 = 0 · · · ∧ pm = 0 is satisfiable if and only if i∈[m] p2i = 0
is satisfiable.
The above equation gives an equivalent condition for checking the existence
of a SU(2) representation of a knot group. We need to further ensure that the
representation is non-commutative. In general, to check that the generators
are non-commutative, we would have to check that at least one of the pairs
of generators does not commute. However, the special structure of knot group
relations allows for a much simpler encoding into polynomial inequalities. In the
following lemma we show that finding a non-commutative SU(2) representation is
equivalent to finding a representation which maps at least two distinct generators
of the Wirtinger presentation to distinct elements of SU(2).
Lemma 3. A knot group π1 (S 3 \ K), with generators gi , has a non-commutative
homomorphism ρ to a group if and only if ρ(gi ) 6= ρ(gj ), for some i 6= j.
Proof. In the forward direction, observe that if the generator’s images are all
equal then ρ is commutative. In the backward direction, assume that the image
set of {gi }1≤i≤n has at least two distinct elements. Therefore, there must exist
an index k ∈ [n] such that ρ(gk ) 6= ρ(gk+1 ). Without loss of generality assume
Unknot Recognition Through Quantifier Elimination 85
the relation Rk = +(Rk ), similar steps would be true for the −(Rk ) form of the
relations. Since ρ(Rk ) = I, we have
ρ(gj )ρ(gk )ρ(gj )−1 ρ(gk+1 )−1 = I.
As ρ(gk ) 6= ρ(gk+1 ), it must be the case that
ρ(gj )ρ(gk )ρ(gj )−1 6= ρ(gk )
=⇒ ρ(gj )ρ(gk ) 6= ρ(gk )ρ(gj ).
Therefore ρ is non-commutative.
If ρ is the SU(2) representation, then it suffices to check that there exist
at least two distinct matrices in the image to obtain the existence of a non-
commutative representation, in addition to the earlier mentioned constraints.
The following series of observations further simplify the criterion:
Observation 4 Consider the matrices Mj and Mk , as defined above where
j, k ∈ [n].
(Mj 6= Mk ) ↔ (aj 6= ak ∨ bj 6= bk ∨ cj 6= ck ∨ dj 6= dk )
be real numbers. There exist indices j, k ∈ [n]
Observation 5 Let r1 , . . . , rm W
m
such that rj 6= rk if and only if `=2 (r1 6= r` ) is true.
The following lemma allows us to convert the system of inequalities encoding
the constraint of non-commutativity into just one equivalent inequality.
Lemma 4. Let N = {p1 6= 0, . . . , pm 6= 0} be a system of m inequality con-
straints. Then p1 6= 0 ∨ p2 6= 0 ∨ · · · ∨ pm 6= 0 is satisfiable if and only if
2
P
i∈[m] i 6= 0 is satisfiable.
p
Proof. The lemma follows from the negation of the statement of Lemma 2.
Combining Lemmas 3, 4 and Observations 4, 5, we get that it suffices to add
the the following inequality, to check non-commutativity:
Xn
(ai − a1 )2 + (bi − b1 )2 + (ci − c1 )2 + (di − d1 )2 6= 0
i=1
Let E be the set consisting of above inequality and the equation in Lemma 2.
It is easy to see from Lemma 2, Observations 4 and 5 and Lemma 4, that there
exists a non-commutative representation from the knot group to SU(2), if and
only if E has a solution. This completes the proof of Theorem 1.
86 S. M. Meesum and T. V. H. Prathamesh
5 Complexity Analysis
The algorithm consists of first computing Wirtinger presentation from the input
knot diagram, which can be done in linear time. The formula E can be constructed
in polynomial time. Next, we analyse the complexity of deciding the feasibility of
the constructed existential formula. If the number of crossings in the provided
knot diagram is n then the number of real variables in the system of equations is
4n. The system of equations E consists of exactly two statements; one equality
and one inequality, with maximum total degree of any monomial of 4. Finally,
note that the coefficients of polynomials occurring in our system of equations are
from the set {−2 − 1, 1, 2}, as the coefficients of the polynomials before squaring
are from the set {−1, 1}. Using Proposition 2, we get the following result.
Theorem 6. The procedure Unknot-QE solves the problem UnKnot Recog-
nition in time 2O(n) , where n is the number of crossings in the given knot
diagram.
6 Conclusion
In this article, we presented an algorithm for UnKnot Recognition, a proof of
correctness, and an analysis of its complexity. The key advantage of this algorithm
over the existent algorithms is the simplicity of description while having the
same runtime complexity as the other currently best algorithms. The simplicity
of this algorithm is largely from an expository perspective, if the existential
quantifier elimination is treated as a blackbox. As an open problem, it would
be of interest to probe whether one can reduce the runtime complexity further
by using a variant of the algorithm presented. It may be possible to do so by
decreasing the number of variables in the equation via substitution methods.
Practical aspects of this algorithm also need to be explored further, for instance-
an implementation using existent tools such as SMT solvers and Cylindrical
Algebraic Decomposition would be useful. A more ‘efficient’ or implementable
algorithm for quantifier elimination in the existential theory of reals would further
aid both the theoretical and practical aspects of unknot recognition.
References
1. Saugata Basu, Richard Pollack, and Marie-Françoise Coste-Roy. Algorithms in real
algebraic geometry, volume 10. Springer Science & Business Media, 2007.
2. Benjamin A Burton and Melih Ozlen. A fast branching algorithm for unknot
recognition with experimental polynomial-time behaviour. arXiv preprint arXiv:
1211.1079v3, 2014.
3. Richard H Crowell and Ralph Hartzler Fox. Introduction to knot theory, volume 57.
Springer Science & Business Media, 2012.
4. IA Dynnikov. Arc-presentations of links: monotonic simplification. Fundamenta
Mathematicae, 190:29–76, 2006.
Unknot Recognition Through Quantifier Elimination 87
5. Andrew Fish, Alexei Lisitsa, David Stanovskỳ, and Sarah Swartwood. Efficient knot
discrimination via quandle coloring with sat and#-sat. In International Congress
on Mathematical Software, pages 51–58. Springer, 2016.
6. D Yu Grigor’ev. Complexity of deciding Tarski algebra. Journal of symbolic
Computation, 5(1-2):65–108, 1988.
7. Wolfgang Haken. Theorie der normalflächen. Acta Mathematica, 105(3-4):245–375,
1961.
8. Joel Hass, Jeffrey C Lagarias, and Nicholas Pippenger. The computational com-
plexity of knot and link problems. Journal of the ACM (JACM), 46(2):185–211,
1999.
9. Akio Kawauchi. A survey of knot theory. Birkhäuser, 2012.
10. Peter B Kronheimer, Tomasz S Mrowka, et al. Witten’s conjecture and property P.
Geometry & Topology, 8(1):295–310, 2004.
11. Greg Kuperberg. Knottedness is in NP, modulo GRH. Advances in Mathematics,
256:493–506, 2014.
12. M Lackenby. A polynomial upper bound on Reidemeister moves. Annals of
Mathematics, 182(2):491–564, 2015.
13. Marc Lackenby. The efficient certification of knottedness and thurston norm. arXiv
preprint arXiv:1604.00290, 2016.
14. WB Raymond Lickorish. An introduction to knot theory, volume 175. Springer
Science & Business Media, 2012.
15. Alexei Lisitsa and Alexei Vernitski. Automated reasoning for knot semigroups and
π -orbifold groups of knots. In Mathematical Aspects of Computer and Information
Sciences, pages 3–18. Springer International Publishing, 2017.
16. Grant Olney Passmore and Paul B Jackson. Combined decision techniques for the
existential theory of the reals. In International Conference on Intelligent Computer
Mathematics, pages 122–137. Springer, 2009.
17. James Renegar. On the computational complexity and geometry of the first-order
theory of the reals. part I: Introduction. preliminaries. the geometry of semi-algebraic
sets. the decision problem for the existential theory of the reals. Journal of symbolic
computation, 13(3):255–299, 1992.
18. Edward Witten, Martin Bridson, Helmut Hofer, Marc Lackenby, and Rahul Pand-
haripande. Lectures on Geometry. Oxford University Press, 2017.