Unknot Detection by Equational Reasoning

Addendum to:

Detecting unknots via equational reasoning, I: Exploration , by Andrew Fish and Alexei Lisitsa, (accepted for Calculemus 2014 , part of CICM 2014)

Introduction

One of the most well-known and intriguing problems in computational topology is Unknot Detection (UKD), which is formulated as follows. Given a knot, that is a closed loop without self-intersection embedded of in 3-dimensional Euclidean space R^{3}. Is it possible to deform it continously within R^{3} to a trivial unknotted circle without passing through itself? Picture below shows the planar projections (diagrams) of two knots with a negative a) and positive b) answers to such a question.

Unknot detection (or unknot recognizion) problem has attracted a lot of attention, but some of the fundamental questions about it remain open. In particular, it is unknown whether it is possible to recognize unknots in PTIME. It is known though that the problem lies in the intersection of NP and coNP [8,11]. There has been a slow but steady development of the algorithms for unknot detection and their experimental evaluation. Early algorithm presented by W. Haken in his proof of the decidability of UKD [7] served mainly to theoretical purposes and deemed to be too complex to attempt to implement it. Since then various algorithms for unknot detection have been proposed with the various degree of implementability and efficiency [5]. The algorithms based on monotone simplifications [5] provide with the practically fast recoginition of unknots but not necessarily with a decision procedure. The algorithms based on normal surface theory implemented in Regina system [2] provide with an efficient recognition of non-trivial knots. In particular it is reported that every non-trivial knot with the crossing number less or equal to 12 is recognized as such by the procedure from [2] in under 5 min. There still efficiency problems with the existing algorithms, in the worst case they are exponential, and it appears that establishing that a particular diagram with a few hundreds (or even dozens) crossings represents a non-trvial knot may well be out of reach of the available procedures.
That makes an exploration of alternative procedures for unknot detection an intersting and well-justifed task.
Here we propose to explore the following route to the efficient practical algorithms for unknot detection. Unknotedness property can be faithfully characterized by the properties of algebraic invariants associated with knot projections. One can try to prove the properties of concrete invariants by using the methods and procedures develeoped in automated reasoning area.

Key observation:

The task of unknot detection can be reduced to the task of (dis)provng the first-order formulae for which there are efficient generic automated procedures, notwithstanding the fact that generally first-order validity is undecidable.

Involutory quandles and Unknot detection

An involutory quandle [13] is an algebraic structure which consists a set Q and a binary operation * (product) satisfying the properties:

x * x = x for all x in Q.
(x * y) * y = x for all x,y in Q.
(x * z) * (y * z) = (x * y) * z for all x,y,z in Q.

With every knot diagram D one can associate an involutory quandle IQ(D) as follows. A solid arc of the diagram is a fragment of the diagram coming from an undercrossing to an undercrossing. Every solid arc of the diagram is labelled by an unique letter (label). All labels of a diagarm D form the set G_{D} of generators. With every crossing of the diagram one associates a relation as shown at the picture below.

For a diagram D denote the set of all such relations by R_{D}.
Then the presentation (G_{D} | R_{D}) defines the invoilutory quandle IQ(D), that is a quotient of the free involutory quandle modulo equational theory defined by R_{D}. The importance of involutary quandles in the context of unknot detection relies on the following properties [9,10,13]:

Involutory quandle is a knot invariant, i.e. it does not depend on a projection of a knot;
Involutory quandle IQ(D)$ of a knot diagram D is trivial, that is contains a single element e with e *e = e, iff D is a diagram of unknot.

Based on that we propose to tackle unknot recognition problem as follows:

given a knot digaram convert it to its involutary quandle presentation; then
convert the task of involutary quandle triviality detection into the task of (dis)proving a first-order equational formuala; and finally
apply generic automated reasoning tools for first-order equational logic to tackle (dis)proving task

We call the approach

Unknot detection by equational reasoning

Given a knot digaram D, consider its involutory quandle representation IQ(D) = (G_{D} | R_{D}) with G_{D} = {a_{1}, ..., a_{n} }. Denote by E_{iq} an equational theory of IQ(D), i.e. E_{iq}(D) = E_{iq} U R_{D}.

Proposition

A knot diagram D is a a diagram of unknot if and only if E_{iq}(D) |-- /\_i=1...n-1 (a_{i} = a_{i+1}), where |-- denotes derivability in the equational logic or, equivalently, in the first-order logic with equality.

Proof

(Sketch) D is a diagram of unknot iff IQ(D) is a trivial involutive quandle [13]. The proposition "IQ(D)$ is a trivial involutory quandle iff E_{iq}(D) |-- /\_i=1... n-1 (a_{i} = a_{i+1})" is an easy consequence of the soundness and completeness of equational logic (Birkhoff Theorem)[3]. See also Lemma 4.2.7 p. 30 of [13]. The case of the first-order logic with equality follows from the conservativity of first-order logic with equality over equational logic for equational theories. End of sketch.

Now we notice that if E_{iq}(D) |-- /\_i=1... n-1 (a_{i} = a_{i+1}) holds true this fact can be established by a proof of the formula E_{iq}(D) --> /\_{i=1... n-1} (a_{i} = a_{i+1}) by a complete automated theorem prover for first-order logic with equality, of which there are many around, see e.g. [1]. For an introducton to the automated theorem proving see e.g. [6].
In order to show that E_{iq}(D) |-- /\_i=1... n-1 (a_{i} = a_{i+1}) does not hold it does suffice to disprove the above implication. We propose to do that by application of a generic finite model finding procedures [4,12] to find a finite countermodel to the formula, or equivalently a finite model for E_{iq}(D) /\ not (/\_{i=1...n-1} (a_{i} = a_{i+1}).

So unknot detection procedure we propose here consists of

parallel composition of

automated proving E_{iq}(D) --> /\_{i=1... n-1} (a_{i} = a_{i+1}) by a complete first-order theorem prover; and
automated disproving E_{iq}(D) --> /\_{i=1...n-1} (a_{i} = a_{i+1}) by a complete finite model finding procedure.

Now, it is obvious that the parallel composition above provides with at least semi-decision algorithm for unknotedeness. If D is a diagram of unknot then the termination of the theorem proving is guaranteed by the completeness of a theorem prover. On the other hand if D is a diagram of a non-trivial knot then the termination can be guaranteed only if a finite countermodel exists. In general in the first-order logic there are the formulae which can only be refuted on the infinite countermodels, so for arbitrary formulae the termination of the automated disproving can not be guaranteed. However, for the specific type of formulae E_{iq}(D) --> /\_{i=1 ... n-1} (a_{i} = a_{i+1}) we conjecture that they have finite countermodel property, that is if there exists a countermodel for a formula of this form at all, then there is a finite countermodel too. As we mentioned before a countermodel for E_{iq}(D) |-- /\_{i=1 ... n-1} (a_{i} = a_{i+1}) is a model for E_{iq}(D) /\ not (/\_{i=1.. n-1} (a_{i} = a_{i+1}). It follows that

such a countermodel is a homomorphic image of the involutory quandle IQ(D) of D (by satisfaction of E_{iq}(D)); and
it is non-trivial involutory quandle (by satisfaction of not(/\_{i=1 ... n-1} (a_{i} = a_{i+1})).

Thus the required finite countermodel property is equivalent to the property of the involutory quandles of knots to be residually finite formulated in the folliowng conjecture.

Conjecture

For any knot diagram D if IQ(D) is not trivial (i.e. consists of more than one element) then there is a finite non-trivial involutory quandle Q, a homomorphic image of IQ(D).

Two remarks on the conjecture:

the knot groups, the invaraints closely related to the involutory quandles are residually finite;
the only reference dealing with residual finitness of knot quandles known to the author is a question posed on MathOverflow

In the next Section we illustrate the practical applicability of the proposed semi-desicion procedure to the various instances of unknot detection problem. In the experiments we use an automated theorem prover Prover9 and a finite model finder Mace4, both by W. McCune [12].

Experiments

Culprit Unknot

shown at athe picture below is an interesting unknot which requires for its untangling by Reidemeister moves to increase the number of crossings before it could be simplified.

Here is the formula of the form E_{iq}(D) --> /\_{i=1 .. n-1} (a_{i} = a_{i+1}) for this diagram in the syntax of Prover9/Mace4:

Assumptions, that is E_{iq}(D):

x * x = x.
(x * y) * y = x.
(x * z) * (y * z) = (x * y) * z.
a1 = a9 * a7.
a3 = a1 * a2.
a2 = a3 * a4.
a5 = a2 * a10.
a6 = a5 * a4.
a7 = a6 * a1.
a8 = a7 * a4.
a10 = a8 * a9.
a4 = a10 * a3.
a9 = a4 * a8.

Goals:

(a1 = a2) & (a2 = a3) & (a3 = a4) & (a4 = a5) & (a5 = a6) & (a6 = a7) & (a7 = a8) & (a8 = a9) & (a9 = a10).

Prover9 proves the formula in 0.03s demonstrating thereby that culprit is indeed unknot. The proof can be found here. .

Haken's Gordian unknot

is the one of the most known concrete hard unknots whose diagram has 141 crossings.

Prover9 produces the proof of the formula of the form E_{iq}(D) --> /\_{i=1 ... n-1} (a_{i} = a_{i+1}) for this diagram in just under 15s, demonstrating that indeed it is unknot. The input and the proof produced by Prover9 can be found here. .

Trefoil

is the simplest non-trivial knot

Here is the formula of the form E_{iq}(D) --> /\_{i=1 .. n-1} (a_{i} = a_{i+1}) for this diagram: Assumptions, that is E_{iq}(D):

x * x = x.
(x * y) * y = x.
(x * z) * (y * z) = (x * y) * z.
a * b = c.
b * c = a.
c * a = b.

Goals:

(a = b) & (b = c)

Mace4 finds a countermodel of size 3 in less than 0.01s. Here is the output:

interpretation( 3, [number=1, seconds=0], [
function(a1, [ 0 ]),
function(a2, [ 1 ]),
function(a3, [ 2 ]),
function(*(_,_), [
0, 2, 1,
2, 1, 0,
1, 0, 2 ])
]).
The square table above represents an interpretation for * operation of involutory quandle, which by the virtue of the method is

a finite involutory quandle, a homomorphic image of IQ(D);
a non-trivial involutory quandle;
is of minimal size among those satsifying conditions above (by the default model finding strategy applied by Mace4).

In fact, for the case of trefoil this involutory quandle is IQ(D).

Other non-trivial knots

We have applied the method for all knots with the number of crossings less or equal 10 taken from Knotinfo . In almost all cases (with the exception of a few quite intriguing failed cases) the method has turned out practically efficient, in many cases a countermodel is found in under a few seconds. The time statistics will appear here soon. The related data can be found as a set of separate files , one for a knot, with a disproving task specification, the resulting model and the time it took Mace4 to find a countermodel.
Better interface to access this data is under construction.

References

[1] The CADE ATP System Competition, The World Championship for Automated Theorem Proving http://www.cs.miami.edu/~tptp/CASC/ (accessed 07.06.2013)
[2] {BenOZ12} Benjamin A. Burton and Melih Olzen, A fast branching algorithm for unknot recognizion with experimental polynomial-time behaviour arXiv:1211.1079 [math.GT],
[3] {Bir35} G.~Birkhoff. On the structure of abstract algebras, {\em Proc. Cambridge Philos. Soc.,} 31:433--454, 1935
[4] {Model} R.~Caferra, A.~Leitsch, N.~Peltier, {\em Automated Model Building}, Applied Logic Series, 31, Kluwer, 2004.
[5] {Dyn} I. A. Dynnikov, Recognition algorithms in knot theory, Uspekhi Mat. Nauk 58 (2003), no. 6(354), 45–92.
[6] {GLM} J.~Goubault-Larrecq and Ian Mackie, {\em Proof Theory and Automated Deduction}, Applied Logic Series, 6, Kluwer, 2001
[7] {Hak61} Wolfgang Haken, Theorie der Normalﬂ¨achen, Acta Math. 105 (1961), 245–375.
[8] {coNP} Joel Hass, Jeﬀrey C. Lagarias, and Nicholas Pippenger, The computational complexity of knot and link problems, J. Assoc. Comput. Mach. 46 (1999), no. 2, 185–211.
[9] {Joyce1982a} Joyce, D., A Classifying Invariant of Knots, the Knot Quandle, Journal of Pure and Applied Algebra 23 (1982) 37-65.
[10] {Joyce1982b} Joyce, D., Simple Quandles, Journal of Algebra 79 (1982) pp. 307-318.
[11]{NP} Greg Kuperberg, Knottedness is in NP, modulo GRH, Preprint, arXiv:1112.0845, November 2011
[12] {McCune} W.~McCune, Prover9 and Mace4, http://www.cs.unm.edu/~mccune/mace4/
[13] {Winker} Steven N. Winker, Quandles, Knot Invariants and the N-fold Branching Cover