Quandle colorings with SAT and #SAT
Addendum to the paper:
Knottedness Certification with MiniSat
Given a PD code of a
knot, a procedure iterates over all quandles from SQ family, converts the quandle colorability task into a SAT instance and checks its satisfiability by MiniSAT. The iteration proceeds until the first satisfiable case is found.
This is a solution to the Q-colorability problem, giving witness to the non-triviality of the knot. For all knots from the K12 family the detection time was in the interval 0.013--3.31s with the vast majority of knots being detected under 1s.
The figure below presents the cumulative frequency of running times for this case.
For the case of A13 family
the range of times was 0.015--5.654 seconds, with a mean time of 0.087s and a median time of 0.039 seconds.
The cumulative frequency graph of running times is presented below.
Scalability of SAT with random knots
The set R consisted of 52 randomly generated knots of varying sizes: 10 knots
of size 25; 10 knots of size 50; 10 knots of size 75; 10 knots of size 100; and 12
of size 125. Recognition of knottedness in R via SAT solving was
virtually instant (much less than $1$ second) for 49 of the cases, whilst for the
other 3 cases (all of size 125) it took just under 290 seconds. The time range was
0.015--288.807 seconds with a mean value of 16.67 seconds and a median value of
0.052 seconds.
The size of the smallest quandle by which the knot is colorable has a
critical effect on the running time.
Scalability of SAT with large torus knots
Average running times (s) for Q-colorability for some torus knots,
averaged over all quandles in SQ
| Torus knot |
Time |
| (3,14)-torus |
0.15s |
| (3,62)-torus |
1.19s |
| (3,104)-torus |
2.07s |
| (3,602)-torus |
3.11s |
Quandle colorings for K12 and CP with #SAT
Note: the values are not normalized and presented exactly as produced by #sat.
In order to get true values one needs to multiply them by the size of the corresponding quandle.
The histogram shown below presents the distribution of the running
times for the K12 family of knots, where for each knot the time is averaged
over all of the 26 quandles in {\bf CQ}. The range of values here is 0.014--153.935
seconds with the mean and the median values being 5.32 seconds and 3.52 seconds,
respectively.
Due to the small size of the CQ family (having only 26 elements
versus 354 for SQ for istance), in the figure below instead of a histogram
the mean values of running times are depicted, averaged over K12 as a function
of the quandle identifiers (i.e. the values $1, \ldots,26$). The range is
0.014--111.07 seconds, with mean and median values of 5.32 and 0.095 seconds,
respectively. The quandle 26 of size 182 is an obvious outlier.
Addendum to the Addendum (unpublished)
Numbers of quandle colorings for all knots with 13 crossings and all quandles from CP family (Q1,...,Q26) (raw data to be cleaned and tabulated)
Last updated 14.11.2018