Tutorials/LLS
So you've decided to search for patterns using Oscar Cunningham's Logic Life Search tool. Excellent!
Installation
Prerequisites
Are you a Windows user? If so, you'll need a Unix-like environment.
- Start by installing Cygwin
- When prompted to choose which packages to install, make sure gcc-core, git, gzip, make, python3, and tar are all selected.
- If prompted, confirm that you also want to install any required prerequisites.
If you already have Cygwin installed, you obviously do not need to install it again, but make sure all the packages listed above are installed.
Installing LLS
You can now install LLS itself. The easiest way to do this by going to the LLS homepage, clicking the download button and selecting 'zip' and then unzipping this file to create the logic-life-search-master directory, which you can place anywhere convenient on your machine.
If you prefer, you can use the Git version control system to download LLS and keep it updated. LLS is published on GitLab. Don't worry, you won't have to learn how to use Git,[note 1], but you'll be using a few commands.
Start by "cloning" the code so you'll have a full copy (don't worry, this'll only take a few seconds):
$ git clone https://gitlab.com/OscarCunningham/logic-life-search.git Cloning into 'logic-life-search'... remote: Counting objects: 73, done. remote: Compressing objects: 100% (52/52), done. remote: Total 73 (delta 29), reused 35 (delta 14), pack-reused 0 Unpacking objects: 100% (73/73), done. $
This'll create a subdirectory called "logic-life-search" containing LLS. No further compilation is required, and again you may place this directory anywhere you wish.
Staying up-to-date
LLS is still evolving; you may want to pull in new changes and improvements made by the author. To do this, use the "git pull" command (be sure to enter the LLS directory if you're not already in it):
$ git pull remote: Counting objects: 84, done. remote: Compressing objects: 100% (32/32), done. remote: Total 84 (delta 65), reused 71 (delta 52), pack-reused 0 Unpacking objects: 100% (84/84), done. From https://gitlab.com/OscarCunningham/logic-life-search ac5758a..153f87e develop -> origin/develop Already up to date. $
Using the development version
New features are first made in the "develop" branch of the program. By default, you're using the "master" branch; use the "git checkout" command to switch to a different one:[note 2]
On May 15, 2022, commonly-used features were moved to the master branch. This means that unless you want specific improvements that you know are only available in the "develop" branch, it is probably no longer necessary to follow these instructions.
$ git checkout develop Switched to branch 'develop' Your branch is up to date with 'origin/develop'. $
To switch back to the stable "master" branch again, simply use "git checkout" again:
$ git checkout master Switched to branch 'master' Your branch is up to date with 'origin/master'. $
Installing a SAT solver
LLS works by converting a pattern search problem into a boolean satisfiability (SAT) problem and solving that using a SAT solver tool, so you'll need a SAT solver.
LLS currently supports many SAT solvers, but we'll focus on kissat and lingeling in this tutorial, as they appear to work best across different platforms, including Windows/Cygwin. At the date of writing, the fastest SAT solver freely available is kissat.
Installing kissat
Download kissat from [1]
Click on "Expand" to the right to view the detailed instructions for installing kissat.
Start by "cloning" the code so you'll have a full copy (don't worry, this'll only take a few seconds):
$ git clone https://github.com/arminbiere/kissat.git Cloning into 'kissat'... remote: Enumerating objects: 993, done. remote: Counting objects: 100% (121/121), done. remote: Compressing objects: 100% (55/55), done. remote: Total 993 (delta 86), reused 66 (delta 66), pack-reused 872 Receiving objects: 100% (993/993), 707.04 KiB | 2.87 MiB/s, done. Resolving deltas: 100% (443/443), done.
Now enter kissat's directory, and run configure.sh:
$ cd kissat
Now run ./configure && make test to build kissat. There may be some warnings; ignore these, they're Mostly Harmless™.
$ ./configure && make test configure: default configuration (see '-h') configure: reusing existing build directory 'build' configure: assuming GCC version 11.3.0 uses C99 by default configure: compiler 'gcc -W -Wall -O3 -DNDEBUG' configure: linker 'gcc' (no additional options) configure: using default 'ar' (no cross compilation) configure: no 'tissat' binary generated (without '--test') configure: no 'libkissat.so' shared library generated (without '-shared') configure: no 'kitten' binary generated (without '--kitten') configure: linking src/makefile make -C "/cygdrive/c/repos/kissat/build" test make[1]: Entering directory '/cygdrive/c/repos/kissat/build' gcc -W -Wall -O3 -DNDEBUG -c ../src/allocate.c gcc -W -Wall -O3 -DNDEBUG -c ../src/analyze.c gcc -W -Wall -O3 -DNDEBUG -c ../src/ands.c gcc -W -Wall -O3 -DNDEBUG -c ../src/arena.c gcc -W -Wall -O3 -DNDEBUG -c ../src/assign.c gcc -W -Wall -O3 -DNDEBUG -c ../src/averages.c gcc -W -Wall -O3 -DNDEBUG -c ../src/backbone.c gcc -W -Wall -O3 -DNDEBUG -c ../src/backtrack.c ... many more lines omitted ... Running 568 jobs in parallel using up to 8 processes. All 568 test jobs succeeded in 8.62 seconds.
That's it, kissat is built. If you're on Windows/Cygwin, the executable will be called kissat.exe; otherwise (including other WSL) it's just kissat. You still need to copy this executable into LLS's solver directory, however:
$ cp build/kissat.exe ../logic-life-search/solvers/ $
You also need to tell LLS to use kissat as its default solver. Go to the file logic-life-search/settings.py and change the 'solver' line to read solver = "kissat". As of February 2023 this is the default setting in the logic-life-search repo.
Installing Lingeling
Download Lingeling from [2]
Click on "Expand" to the right to view the detailed instructions for installing lingeling.
Start by "cloning" the code so you'll have a full copy (don't worry, this'll only take a few seconds):
$ git clone https://github.com/arminbiere/lingeling.git Cloning into 'lingeling'... remote: Enumerating objects: 90, done. remote: Counting objects: 100% (11/11), done remote: Compressing objects: 100% (7/7), done. remote: Total 90 (delta 3), reused 9 (delta 3), pack-reused 79 Unpacking objects: 100% (90/90), done. $
Now enter Lingeling's directory, and run configure.sh:
$ cd lingeling $ ./configure.sh gcc -Wall -O3 -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLDRUPLIG -DNLGLYALSAT -DNLGLFILES -DNLGLDEMA $
Now run make to build Lingeling. There may be some warnings; ignore these, they're Mostly Harmless™.
$ make
gcc -Wall -O3 -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLDRUPLIG -DNLGLYALSAT -DNLGLFILES -DNLGLDEMA -c lglib.c
lglib.c: In function ‘lglstampall’:
lglib.c:19156:2: warning: this ‘if’ clause does not guard... [-Wmisleading-indentation]
if (rootsonly) noimpls++; goto CONTINUE;
^~
lglib.c:19156:28: note: ...this statement, but the latter is misleadingly indented as if it is guarded by the ‘if’
if (rootsonly) noimpls++; goto CONTINUE;
^~~~
rm -f lglcflags.h
echo '#define LGL_CC "gcc (GCC) 6.4.0"' >> lglcflags.h
echo '#define LGL_CFLAGS "-Wall -O3 -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLDRUPLIG -DNLGLYALSAT -DNLGLFILES -DNLGLDEMA"' >> lglcflags.h
rm -f lglcfg.h
./mkconfig.sh > lglcfg.h
gcc -Wall -O3 -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLDRUPLIG -DNLGLYALSAT -DNLGLFILES -DNLGLDEMA -c lglbnr.c
gcc -Wall -O3 -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLDRUPLIG -DNLGLYALSAT -DNLGLFILES -DNLGLDEMA -c lgldimacs.c
gcc -Wall -O3 -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLDRUPLIG -DNLGLYALSAT -DNLGLFILES -DNLGLDEMA -c lglopts.c
ar rc liblgl.a lglib.o lglbnr.o lgldimacs.o lglopts.o
ranlib liblgl.a
gcc -Wall -O3 -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLDRUPLIG -DNLGLYALSAT -DNLGLFILES -DNLGLDEMA -c lglmain.c
gcc -Wall -O3 -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLDRUPLIG -DNLGLYALSAT -DNLGLFILES -DNLGLDEMA -o lingeling lglmain.o -L. -llgl -lm
gcc -Wall -O3 -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLDRUPLIG -DNLGLYALSAT -DNLGLFILES -DNLGLDEMA -c plingeling.c
gcc -Wall -O3 -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLDRUPLIG -DNLGLYALSAT -DNLGLFILES -DNLGLDEMA -pthread -o plingeling plingeling.o -L. -llgl -lm
gcc -Wall -O3 -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLDRUPLIG -DNLGLYALSAT -DNLGLFILES -DNLGLDEMA -c ilingeling.c
gcc -Wall -O3 -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLDRUPLIG -DNLGLYALSAT -DNLGLFILES -DNLGLDEMA -pthread -o ilingeling ilingeling.o -L. -llgl -lm
gcc -Wall -O3 -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLDRUPLIG -DNLGLYALSAT -DNLGLFILES -DNLGLDEMA -c treengeling.c
treengeling.c: In function ‘mysrand’:
treengeling.c:1381:3: warning: this ‘if’ clause does not guard... [-Wmisleading-indentation]
if (!z) z = ~z; if (!w) w = ~w;
^~
treengeling.c:1381:19: note: ...this statement, but the latter is misleadingly indented as if it is guarded by the ‘if’
if (!z) z = ~z; if (!w) w = ~w;
^~
gcc -Wall -O3 -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLDRUPLIG -DNLGLYALSAT -DNLGLFILES -DNLGLDEMA -pthread -o treengeling treengeling.o -L. -llgl -lm
gcc -Wall -O3 -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLDRUPLIG -DNLGLYALSAT -DNLGLFILES -DNLGLDEMA -c lglmbt.c
gcc -Wall -O3 -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLDRUPLIG -DNLGLYALSAT -DNLGLFILES -DNLGLDEMA -o lglmbt lglmbt.o -L. -llgl -lm
gcc -Wall -O3 -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLDRUPLIG -DNLGLYALSAT -DNLGLFILES -DNLGLDEMA -c lgluntrace.c
gcc -Wall -O3 -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLDRUPLIG -DNLGLYALSAT -DNLGLFILES -DNLGLDEMA -o lgluntrace lgluntrace.o -L. -llgl -lm
gcc -Wall -O3 -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLDRUPLIG -DNLGLYALSAT -DNLGLFILES -DNLGLDEMA -c lglddtrace.c
gcc -Wall -O3 -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLDRUPLIG -DNLGLYALSAT -DNLGLFILES -DNLGLDEMA -o lglddtrace lglddtrace.o -L. -llgl -lm
$
That's it, Lingeling is built. If you're on Windows/Cygwin, the executable will be called lingeling.exe; otherwise (including other WSL) it's just lingeling. You still need to copy this executable into LLS's solver directory, however:
$ cp lingeling.exe ../logic-life-search/solvers/ $
You also need to tell LLS to use lingeling as its default solver. Go to the file logic-life-search/settings.py and change the 'solver' line to read solver = "lingeling".
First steps
Finding 25P3H1V0.2
For our first test, let's find 25P3H1V0.1,[1] a small c/3 spaceship originally found by David Bell in 1992.
Enter LLS's directory if necessary, and run the following:
$ python lls -c -b 16 6 -s p3 x0 y1 Getting search pattern... Done Preprocessing... Done Number of undetermined cells: 272 Number of variables: 369 Number of clauses: 34412 Active width: 16 Active height: 6 Active duration: 4 Solving... Done Time taken: 1.7274296283721924 seconds x = 18, y = 8, rule = B3/S23 bbbbbbbbbbbbbbbbbb$ bbobbbbbbbbbbbbbbb$ bobbbobbbobbbbbobb$ bbooobbbobbobobbob$ bbboboobbbbooboobb$ bbbbbbboooboobobbb$ bbbbbbbbbbbbbbbbbb$ bbbbbbbbbbbbbbbbbb! $
LLS converted our request to a problem the SAT solver could solve, and it gave us the answer in less than 2 seconds. Impressive! Here's our result:
| 25P3H1V0.1 (click above to open LifeViewer) |
But what did we request? Let's take a look at the options we passed to LLS:
- -c: tells LLS to look for a changing pattern, i.e. for the first two generations to be different.
- -b 16 6: tells LLS to create a blank search pattern with a size of 16×6. Without this, we'd have to have told LLS explicitly what our pattern should look like.
- -s: tells LLS to look for a pattern with a particular symmetry:
- p3 the pattern repeats itself with period 3,
- x0: moving by 0 cells horizontally in each full period,
- y1: and moving by 1 cell vertically in each full period.
There's a lot more options to LLS; run ./lls -h to see them all.
Finding Brain
Let's try hunting for a different spaceship, Brain.[2] Run the following:
$ python lls -c -b 17 12 -s p3 x0 y1 -s "D2|" Getting search pattern... Done Preprocessing... Done Number of undetermined cells: 315 Number of variables: 424 Number of clauses: 43369 Active width: 17 Active height: 12 Active duration: 4 Solving... Done Time taken: 57.500898599624634 seconds x = 19, y = 14, rule = B3/S23 bbbbbbbbbbbbbbbbbbb$ bbobbbbbbbbbbbbbobb$ bbobbbbooboobbbbobb$ bbboobbobbbobboobbb$ bbbooobbobobbooobbb$ bbbooboboboboboobbb$ bbbbobobobobobobbbb$ bbbbbbobobobobbbbbb$ bbobooboobooboobobb$ bobobobbbbbbbobobob$ boboboobbbbboobobob$ bbooobbbbbbbbbooobb$ bbbbbbbbbbbbbbbbbbb$ bbbbbbbbbbbbbbbbbbb! $
57 seconds — not bad! Here's our catch:
| Brain (click above to open LifeViewer) |
We already know the -c, -b and -s p3 x0 y1 options from above. But there's one new one:
- -s "D2|": tells LLS to look for patterns with an additional symmetry. We passed "D2|", meaning we're interested in patterns that are mirror-symmetric about a vertical axis. The quotes around D2| are necessary to keep the shell from interpreting the pipe symbol, |, as a special character, and instead pass it to LLS unchanged.
Specifying a symmetry made finding Brain that much faster.
Finding an alien (2,1)c/3 spaceship
LLS can search different rules. It's not limited to semi-totalistic rules either, and in fact you don't even need to specify the exact rule you're interested in. To demonstrate this, let's find a small alien spaceship moving at a speed of (2,1)c/3:[3]
$ python lls -s p3 x2 y1 -b 6 6 -r pB1-c2345678/S012345678 -p ">0" -p "<=5" Getting search pattern... Done Preprocessing... Done Number of undetermined cells: 86 Number of variables: 306 Number of clauses: 38100 Active width: 6 Active height: 6 Active duration: 4 Solving... Done Time taken: 0.20017600059509277 seconds x = 8, y = 8, rule = B2-en3ejr4ant/S01c2-en3ey5ae bbbbbbbb$ bbbbbbbb$ bbbbobbb$ bbbbobbb$ bbbbobbb$ bobobbbb$ bbbbbbbb$ bbbbbbbb!
What did we find this time? Let us take a look:
| An alien (2,1)c/3 ship. (click above to open LifeViewer) |
Most of the options passed to LLS are familiar by now, but two are new:
- -r pB1-c2345678/S012345678: tells LLS what birth/survival conditions we'll allow in our target rules. In pB1-c2345678/S012345678, the leading p tells LLS that the following is a partial specification, rather than a complete one. The trailing string, B1-c2345678/S012345678, describes the rulespace we'd like to be considered. Here, B1-c rules out the "B1c" subcondition. B1e, B2 to B8, and S0 to S8 are all allowed. Refer to Hensel notation for an overview over the various subconditions allowed; for an easy-to-use script for converting a given range of rules to the notation required by -r, see § Finding the right parameter to pass to -r.
- -p ">0": tells LLS that the first generation of the pattern found must contain at least one live cell. We're not interested in empty solutions. Likewise -p "<=5" tells LLS that the first generation of the pattern found must contain at most five live cells.
The last option -p "<=5" is important; without it, the SAT solver (and, by extension, LLS) might find a different pattern than the one above. There are many solutions satisfying the constraints we imposed, and only the first solution identified will be reported.
Success -- now what?
Let's assume that you have run your own search, and found something new and exciting. What now? You may want to report your discovery; perhaps it's known, perhaps not. Here are some good places to do so: The Catagolue object identification page (paste in your RLE to see whether it's already been discovered in any censuses or has a name or article)
- Spaceship Discussion Thread (discussion thread) at the ConwayLife.com forums
- Oscillator Discussion Thread (discussion thread) at the ConwayLife.com forums
- Thread for your unsure discoveries (discussion thread) at the ConwayLife.com forums
There's one thing you should (probably) not do, and that's start a LifeWiki article on your discovery. If it's notable, chances are good someone else will.
How do I...?
This section collects helpful hints and tips on how to accomplish common tasks.
Finding the right parameter to pass to -r
LLS's -r option requires the target rulespace to be passed in what has been dubbed "Macbi partial" notation. Converting a pair of given "minimum" and "maximum" rules to this notation is not entirely straightforward; Rhombic has made available a pair of scripts (to be run inside and outside of Golly, otherwise functionally equivalent) to perform the necessary conversion.[4]
Suppose that you want to search any rules falling into the rulespace demarcated by B3/S2-i34q (tlife) and B35e8/S2-i34ceq6i7e8. Running Rhombic's script and entering both values yields pB3aceijknqry5-acijknqry8/S2acekn-i3aceijknqry4q-aijknrtwyz6-acekn7-c8, so this is the option you should pass to -r when running LLS to perform your desired search.
Troubleshooting
This section collects common and not-so-common problems you may run into, and suggestions on what might have gone wrong.
Unsatisfiable
Problem: LLS says the search is unsatisfiable, i.e. has no solution.
Bounding box too small
Possible explanation: the bounding box you specified was too small to accommodate the full evolution of the final pattern. For example:
$ python lls -r B2en3ij4a5e7e8/S1c2cek3-a4aiqw5aky -b 10 10 -s p55 x9 y0 -p ">0" Getting search pattern... Done Preprocessing... Done Number of undetermined cells: 540 Number of variables: 541 Number of clauses: 4260 Active width: 1 Active height: 10 Active duration: 54 Solving... Done Time taken: 0.004628658294677734 seconds Unsatisfiable $
We asked for a deplacement of x9 while also requiring the entire pattern to fit into a 10×10 bounding box (-b 10 10), and LLS and the SAT solver quickly determined that there was no way that a period-55 (-p 55) pattern meeting both these criteria could possibly exist.
Solution: Passing a larger bounding box should help.
Notes
References
- ↑ Tom Rokicki (January 28, 2018). Re: Logic Life Search (discussion thread) at the ConwayLife.com forums
- ↑ Adam P. Goucher (January 28, 2018). Re: Logic Life Search (discussion thread) at the ConwayLife.com forums
- ↑ Oscar Cunningham (January 29, 2018). Re: Logic Life Search (discussion thread) at the ConwayLife.com forums
- ↑ Rhombic (February 5, 2018). Re: Logic Life Search (discussion thread) at the ConwayLife.com forums
External links
- Logic Life Search on GitLab
- Logic Life Search (discussion thread) at the ConwayLife.com forums
- SAT solvers:
- Kissat
- CaDiCaL
- Lingeling (404's, see archive.org)
| |||||||||||||||||