This post will be a very short one, simply a demonstration of the longest NS1D0 sequence I've been able to produce with our algorithm so far. This is an NS1D0 sequence of order 175: [0, 101, 65, 137, 91, 33, 67, 10, 83, 90, 68, 173, 69, 28, 73, 50, 140, 74, 37, 70, 120, 95, 171, 116, 51, 42, 124, 130, 147, 84, 82, 170, 63, 44, 57, 157, 97, 71, 15, 25, 138, 54, 146, 35, 23, 34, 66, 117, 21, 165, 123, 96, 112, 26, 31, 45, 27, 48, 115, 158, 114, 55, 136, 174, 127, 13, 16, 12, 47, 87, 135, 9, 17, 162, 7, 76, 22, 168, 144, 172, 133, 118, 20, 72, 152, 99, 98, 1]
The SAT solver took 43 seconds to produce this sequence, which used 22,801 variables and 20,339,846 clauses. The solve required 3 iterations through the SAT solver, one of the fewest numbers of iterations I've found for higher order SAT solvers such as this. Many of this order require 9 or more iterations, at which point the SAT solver takes up such a large amount of memory that my computer shuts down the iPython kernel; however this would not be a problem on a computer with more memory available.
From this NS1D0 sequence we can produce a Steiner Triple System of order 525, a system which has 45,850 triples. This system is much too large to include on this post, but for those interested it can be found at https://www.cs.drexel.edu/~lap368/sts.html
Verifying The Results
In order to verify that the results we were getting were valid, I wrote two short python scripts, one to check if a given list is a valid NS1D0 sequence; and another to check if a given list of lists is a valid Steiner Triple System. Both of these are available in the checks.py file in the public gitlab for this project. The NS1D0 sequence and its generated Triple System both pass the tests.
Comments