ikpx
ikpx (incremental knightship partial extender) is a tool for finding spaceships by extending partials, written by Adam P. Goucher in 2018. It was used to find Sir Robin, the first elementary knightship in Conway's Game of Life.
| ikpx | ||
| ||
| Homepage | Click here | |
|---|---|---|
| Purpose | Searching for knightships | |
| Created by | Adam P. Goucher | |
| Platform | Platform-independent (Python) | |
In particular, the search program can find spaceships which move a cells left and b cells upwards every p generations, provided that the parameters are coprime. Without loss of generality, b is assumed to be nonzero and at least as large as a.
Quotient lattice
Inspired by gfind, the internal representation of patterns interleaves the phases of the pattern. This is slightly more complex in the case of oblique spaceships, where one cannot simply interleave the rows of the phases. As such, ikpx uses the more general idea of a quotient lattice.
Specifically, the history of the pattern can be considered as a subset of the three-dimensional integer lattice, where (x, y, t) indicates the cell at coordinates (x, y) at generation t. Oscillators and spaceships correspond to singly-periodic subsets of this lattice. If the parameters are coprime, then quotienting the integer lattice by the periodicity direction (-a, -b, p) gives a quotient lattice. In the case of orthogonal spaceships, where a = 0, this coincides exactly with the representation used in gfind.
For convenience, a pair of Golly scripts called golly2ikpx.py and ikpx2golly.py are included for converting between the quotient lattice representation and the phases of the pattern.
The choice of coordinates of the quotient lattice is designed so that the front of the spaceship corresponds to the top of the representation, and the back of the spaceship corresponds to the bottom of the spaceship.
iglucose
The search tree is substantially pruned by using a lookahead: we only consider partials that can be extended by another k rows at the current search width. This is accomplished by the use of an incremental SAT solver called iglucose, modified by Marijn Heule and Tomas Rokicki from the Glucose SAT solver, itself a descendent of MiniSAT. The modifications mean that iglucose can be operated interactively by ikpx, which feeds constraints to iglucose and awaits partial results in return.
The effect is that the vast majority of CPU usage is by the optimised iglucose code, rather than the Python script orchestrating the search.
Features
As the Python script is not a performance bottleneck, it is free to include many features and optimisations.
Floating rows
Most spaceship search programs mandate that the spaceship fits entirely within a rectangle of width w. Instead, ikpx only requires the spaceship to locally have a width of w, so the shape of the partial is permitted to drift arbitrarily in a horizontal direction. An effect of this is that a shifted copy of a partial is considered equivalent to the original partial, eliminating any redundancy in the search tree.
Adaptive widening
When completing a search in gfind without any results, it is common for the operator to attempt a search at the next width up. This discards all of the time spent searching, starting completely afresh. As an alternative, ikpx increments the width whenever the search completes, and retains the existing search tree so that the work need not be repeated.
Saving and restoring
Every hour, ikpx periodically dumps its search tree(s) in compressed pickled files. Also, a SIGINT (operating system interrupt) causes the program to similarly save its progress before exiting. A subsequent run of ikpx with the same target directory will resume its progress from the backup, allowing a search to persist even if the program is terminated. When restoring, it is perfectly possible to use different hyperparameters (i.e. change w and k), allowing one to find spaceships with sections of different widths. This idea, albeit with a different search program, allowed Tim Coe to discover the spaghetti monster.
Importing partials
An RLE saved by Golly after running golly2ikpx.py can be opened by ikpx and included in the search tree. Sir Robin was found by importing a partial discovered by Tomas Rokicki using a separate search program and running at a lower width.
Meet-in-the-middle
It is possible to run ikpx to extend partial front-ends of spaceships, partial back-ends of spaceships, or both simultaneously. In the latter case, it uses a hashtable lookup to see whether a front-end can be joined to a back-end to yield a complete result. This same methodology is used in cryptanalysis, where it can give a quadratic speedup over brute force.
In any case, when extending front-ends it also looks for a direct completion, which was the methodology that found Sir Robin. This was somewhat surprising, as both the author and Tomas Rokicki expected the meet-in-the-middle approach to find a solution long before the direct completion approach.
Parallelism
The script is designed to run on multicore computers, running many simultaneous instances of iglucose to take advantage of the number of processors. This gives ikpx an advantage over single-threaded search programs.
ikpx2
A new version of ikpx, known as ikpx2, is currently under development. This version is written entirely in C++ and uses a new SAT solver (Armin Biere's kissat), and is able to support symmetry and arbitrary isotropic non-totalistic rules.[1] The GitLab repository was made public on August 24, 2020.[2]
Also see
- Tutorials/ikpx
References
- Adam P. Goucher (August 8, 2020). Re: Ikpx and grills (discussion thread) at the ConwayLife.com forums
- Adam P. Goucher (August 24, 2020). Message in #tools on the Conwaylife Lounge Discord server