Tutorials/LLS: Difference between revisions

Latest revision as of 16:35, 25 September 2026

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.

1. Start by installing WSL (Windows Subsystem for Linux) by running the following in your command prompt (the installation can take several minutes):

wsl --install

2. Once WSL is installed, open WSL and create a user account with a username and password, and confirm the prompt regarding collection of platform metrics.

3. Update the package list using the following command:

$ sudo apt update

4. Install the following packages using the following command:

$ sudo apt install -y build-essential git gzip python3 tar

If you already have WSL 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:

$ 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:

x = 18, y = 8, rule = B3/S23
bbbbbbbbbbbbbbbbbb$
bbobbbbbbbbbbbbbbb$
bobbbobbbobbbbbobb$
bbooobbbobbobobbob$
bbboboobbbbooboobb$
bbbbbbboooboobobbb$
bbbbbbbbbbbbbbbbbb$
bbbbbbbbbbbbbbbbbb!
#C [[ THUMBSIZE 2 THEME 6 GRID GRIDMAJOR 0 SUPPRESS THUMBLAUNCH ]]
#C [[ THEME 6 GRID TRACKLOOP 3 0 1/3 AUTOSTART THUMBLAUNCH THUMBSIZE 2 GPS 3 ]]

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:

x = 19, y = 14, rule = B3/S23
bbbbbbbbbbbbbbbbbbb$
bbobbbbbbbbbbbbbobb$
bbobbbbooboobbbbobb$
bbboobbobbbobboobbb$
bbbooobbobobbooobbb$
bbbooboboboboboobbb$
bbbbobobobobobobbbb$
bbbbbbobobobobbbbbb$
bbobooboobooboobobb$
bobobobbbbbbbobobob$
boboboobbbbboobobob$
bbooobbbbbbbbbooobb$
bbbbbbbbbbbbbbbbbbb$
bbbbbbbbbbbbbbbbbbb!
#C [[ THUMBSIZE 2 THEME 6 GRID GRIDMAJOR 0 SUPPRESS THUMBLAUNCH ]]
#C [[ THEME 6 GRID TRACKLOOP 3 0 1/3 AUTOSTART THUMBLAUNCH THUMBSIZE 2 GPS 3 ]]

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:

x = 8, y = 8, rule = B2-en3ejr4ant/S01c2-en3ey5ae
bbbbbbbb$
bbbbbbbb$
bbbbobbb$
bbbbobbb$
bbbbobbb$
bobobbbb$
bbbbbbbb$
bbbbbbbb!
#C [[ THUMBSIZE 2 THEME 6 GRID GRIDMAJOR 0 SUPPRESS THUMBLAUNCH ]]
#C [[ THEME 6 GRID TRACKLOOP 3 2/3 1/3 AUTOSTART THUMBLAUNCH THUMBSIZE 2 GPS 3 ]]

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:

B1c

-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.

More complex tasks

Finding specific sequences

So we've used LLS to find a few spaceships, cool. But there's much more power to this program than that. Now we're gonna try to find a pattern that evolves in a certain way. Specifically, we're gonna use LLS to find an eater.

How do we do that? First, make a text file in your LLS folder. Name it whatever you want, but I would personally stick to naming it "eater".

Now paste all of this into the file:

0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0
0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0
0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0
0, 0, 0, a, b, c, d, e, 0, 0, 0, 0, 0, 0, 0
0, 0, 0, f, g, h, i, j, 0, 0, 0, 0, 0, 0, 0
0, 0, 0, k, l, n, m, o, 0, 0, 0, 0, 0, 0, 0
0, 0, 0, p, q, r, s, t, 0, 0, 0, 0, 0, 0, 0
0, 0, 0, u, v, w, x, y, 0, 0, 0, 0, 0, 0, 0
0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0

0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 1, 0, 0, 0
0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0
0, 0, 0, a, b, c, d, e, 0, 0, 1, 0, 0, 0, 0
0, 0, 0, f, g, h, i, j, 0, 0, 0, 0, 0, 0, 0
0, 0, 0, k, l, n, m, o, 0, 0, 0, 0, 0, 0, 0
0, 0, 0, p, q, r, s, t, 0, 0, 0, 0, 0, 0, 0
0, 0, 0, u, v, w, x, y, 0, 0, 0, 0, 0, 0, 0
0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0

0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
0, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
0, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
0, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
0, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
0, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
0, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
0, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
0, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0

0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
0, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
0, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
0, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
0, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
0, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
0, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
0, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
0, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0

0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
0, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
0, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
0, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
0, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
0, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
0, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
0, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
0, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0

0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
0, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
0, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
0, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
0, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
0, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
0, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
0, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
0, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0

0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
0, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
0, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
0, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
0, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
0, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
0, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
0, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
0, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0

0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
0, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
0, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
0, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
0, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
0, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
0, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
0, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
0, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0

0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
0, 0, 0, a, b, c, d, e, 0, 0, 0, 0, 0, 0, 0
0, 0, 0, f, g, h, i, j, 0, 0, 0, 0, 0, 0, 0
0, 0, 0, k, l, n, m, o, 0, 0, 0, 0, 0, 0, 0
0, 0, 0, p, q, r, s, t, 0, 0, 0, 0, 0, 0, 0
0, 0, 0, u, v, w, x, y, 0, 0, 0, 0, 0, 0, 0
0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0

But wait, before we do that, what does all of this actually mean?

Each separated array of characters represents what we want to happen on a specific generation, so the first array represents generation 0, the second generation 1, etc. There are 3 different characters used here, representing what states we want the cells to be.

0 marks a dead cell, 1 marks a live cell
An asterisk (*) marks a cell that can be in either state
The letters (and anything else besides 0, 1, and *) represent variables. Variables are cells that must be in the same state on all generations they appear on.

So can you decipher what exactly we're asking LLS to do?

We are looking for a sequence that goes as follows:

A glider moves towards a square of cells that stay in the same state for two generations
When the glider and cells collide, it results in chaos that isn't easy to predict, so cells can be in any state in the immediate area. This array is repeated for several generations, just in case.
On the final generation, the cells from the start must be in the same state they were in the beginning.

Now, save the text file, run LLS simply with the file name as the only parameter

python lls (file name).txt

And it will spit out a pattern that evolves off of the conditions we gave it. Shortly after, you should see this as a result:

x = 17, y = 12, rule = B3/S23
bbbbbbbbbbbbbbbbb$
bbbbbbbbbbbbbbbbb$
bbbbbbbbbbbobbbbb$
bbbbbbbbbbobbbbbb$
bbbbbbbbbbooobbbb$
bbbbbbbbbbbbbbbbb$
bbbbbbboobbbbbbbb$
bbbbbbobobbbbbbbb$
bbbbbbobbbbbbbbbb$
bbbbboobbbbbbbbbb$
bbbbbbbbbbbbbbbbb$
bbbbbbbbbbbbbbbbb!

And if by looking at the RLE given to us in a program, we can see that LLS gave us a glider and... Eater 1!

x = 8, y = 8, rule = B3/S23
6bo$5bo$5b3o2$2b2o$bobo$bo$2o!
#C [[ THUMBSIZE 2 THEME 6 GRID GRIDMAJOR 0 SUPPRESS THUMBLAUNCH ]]

(click above to open LifeViewer)

So now you know how to use a series of conditions like this to find a complex sequence. With this knowledge, you can find hasslers, reflectors, predecessors, patterns that emit specific objects, etc. And on the topic of predecessors...

Predecessor searches (rewinding)

Another thing that LLS is very good at is searching for predecessors. Suppose you have a pattern for which no predecessor is known, e.g.,

x = 16, y = 16, rule = B3/S23
o3bo2b2o2b5o$o3bobo2bo3bo$2o2bobo2bo3bo$obobobo2bo3bo$o2b2obo2bo3bo$o
3bobo2bo3bo$o3bo2b2o4bo3$3o2b2o2b3obobo$o3bo2bobo3bobo$o3bo2bobo3bobo$
3obo2bob3o2b2o$o3b4o3bo2bo$o3bo2bo3bo2bo$b2obo2bob3o2bo!
#C [[ THUMBSIZE 2 THEME 6 GRID GRIDMAJOR 0 SUPPRESS THUMBLAUNCH ]]

sample 16x16 pattern for which a predecessor is wanted
(click above to open LifeViewer)

The basic steps for using LLS to find predecessors are laid out in a 2022 forum post by Macbi.^[4] First we can find out whether the target pattern has any patterns that fit into the same 16x16 box. Create a file called (say) 16x16-predecessor-search.txt, as follows:

0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0
0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0
0,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
0,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
0,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
0,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
0,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
0,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
0,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
0,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
0,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
0,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
0,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
0,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
0,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
0,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
0,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
0,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0
0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0

0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0
0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0
0,0,1,0,0,0,1,0,0,1,1,0,0,1,1,1,1,1,0,0
0,0,1,0,0,0,1,0,1,0,0,1,0,0,0,1,0,0,0,0
0,0,1,1,0,0,1,0,1,0,0,1,0,0,0,1,0,0,0,0
0,0,1,0,1,0,1,0,1,0,0,1,0,0,0,1,0,0,0,0
0,0,1,0,0,1,1,0,1,0,0,1,0,0,0,1,0,0,0,0
0,0,1,0,0,0,1,0,1,0,0,1,0,0,0,1,0,0,0,0
0,0,1,0,0,0,1,0,0,1,1,0,0,0,0,1,0,0,0,0
0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0
0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0
0,0,1,1,1,0,0,1,1,0,0,1,1,1,0,1,0,1,0,0
0,0,1,0,0,0,1,0,0,1,0,1,0,0,0,1,0,1,0,0
0,0,1,0,0,0,1,0,0,1,0,1,0,0,0,1,0,1,0,0
0,0,1,1,1,0,1,0,0,1,0,1,1,1,0,0,1,1,0,0
0,0,1,0,0,0,1,1,1,1,0,0,0,1,0,0,1,0,0,0
0,0,1,0,0,0,1,0,0,1,0,0,0,1,0,0,1,0,0,0
0,0,0,1,1,0,1,0,0,1,0,1,1,1,0,0,1,0,0,0
0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0
0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0

Then run LLS:

python lls 16x16-predecessor-search.txt

This particular search quickly comes back with UNSATISFIABLE, so there are no 16x16 predecessors of this 16x16 pattern. We'll have to extend the boundaries a little.

For this example, let's also extend the search so that it finds a 2-generation predecessor. Here's a sample revised input file:

0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0
0,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,*,0,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0
0,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0

0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0
0,0,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0,0
0,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
0,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
0,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
0,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
0,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
0,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
0,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
0,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
0,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
0,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
0,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
0,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
0,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
0,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
0,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
0,0,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0,0
0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0
0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0

0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0
0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0
0,0,0,1,0,0,0,1,0,0,1,1,0,0,1,1,1,1,1,0,0,0
0,0,0,1,0,0,0,1,0,1,0,0,1,0,0,0,1,0,0,0,0,0
0,0,0,1,1,0,0,1,0,1,0,0,1,0,0,0,1,0,0,0,0,0
0,0,0,1,0,1,0,1,0,1,0,0,1,0,0,0,1,0,0,0,0,0
0,0,0,1,0,0,1,1,0,1,0,0,1,0,0,0,1,0,0,0,0,0
0,0,0,1,0,0,0,1,0,1,0,0,1,0,0,0,1,0,0,0,0,0
0,0,0,1,0,0,0,1,0,0,1,1,0,0,0,0,1,0,0,0,0,0
0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0
0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0
0,0,0,1,1,1,0,0,1,1,0,0,1,1,1,0,1,0,1,0,0,0
0,0,0,1,0,0,0,1,0,0,1,0,1,0,0,0,1,0,1,0,0,0
0,0,0,1,0,0,0,1,0,0,1,0,1,0,0,0,1,0,1,0,0,0
0,0,0,1,1,1,0,1,0,0,1,0,1,1,1,0,0,1,1,0,0,0
0,0,0,1,0,0,0,1,1,1,1,0,0,0,1,0,0,1,0,0,0,0
0,0,0,1,0,0,0,1,0,0,1,0,0,0,1,0,0,1,0,0,0,0
0,0,0,0,1,1,0,1,0,0,1,0,1,1,1,0,0,1,0,0,0,0
0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0
0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0

In about a second, this search will return a valid 2-tick predecessor of the target pattern:

x = 20, y = 18, rule = B3/S23
2bo2bobobobo2bobobo$o3bob3o2bo2bobo$ob2obobo6b2obo$6bobobo2bo2bo$ob2o
2bo2bob3o2b4o$o4b2o2b2o4bobo$4b3obobo2bo$2bo6bo3b2o$o2bo3b3o2bo2b2o$o
3b2o3b3o7bo$3bob2o3b2o2b2obobo$bob4o2bo4b3o$2b2o4bo3bobo$2bo3bo2bo3bo
2b2obo$5bo6bob3o$2bob3ob4obobobobo$12bo$bobobo5bo2b2ob2o!
#C [[ THUMBSIZE 2 THEME 6 GRID GRIDMAJOR 0 SUPPRESS THUMBLAUNCH ]]

sample 16x16 pattern for which a predecessor is wanted
(click above to open LifeViewer)

Notice the "0" toward the center of the "minus-two" generation's target pattern, in the input file above -- and also the extra "0"s in the corners. Replace the central "0" with a "1" and a different predecessor will be generated. When rewinding patterns through multiple generations, it's often useful to experiment with additional constraints like this, to make sure that there are multiple possible choices of ancestor and reduce the likelihood of arriving at a Garden of Eden dead end.

A 16x16 pattern's predecessor seems to have a tendency to be larger than it is, by about one cell on each side. That's a very rough average, though, not necessarily true in any specific case! Larger patterns may have to add two rows or columns of cells along each edge to enable a solution to be found.

It's an open question whether there are workable ways to constrain predecessors in such a way that their predecessors will be easier to find.

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.^[5]

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

↑ If you're interested in doing so, refer to Git's documentation. The tutorial is a good place to start.
↑ Despite the name, this is a local command that does not interact with the remote repository on GitLab.

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
↑ Oscar Cunningham (February 18, 2022). Re: Algorithm for reversing the GoL rules (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)

[1] If you're interested in doing so, refer to Git's documentation. The tutorial is a good place to start.

[2] Despite the name, this is a local command that does not interact with the remote repository on GitLab.

[post55778-3] Tom Rokicki (January 28, 2018). Re: Logic Life Search (discussion thread) at the ConwayLife.com forums

[post55792-4] Adam P. Goucher (January 28, 2018). Re: Logic Life Search (discussion thread) at the ConwayLife.com forums

[post55864-5] Oscar Cunningham (January 29, 2018). Re: Logic Life Search (discussion thread) at the ConwayLife.com forums

[post141799-6] Oscar Cunningham (February 18, 2022). Re: Algorithm for reversing the GoL rules (discussion thread) at the ConwayLife.com forums

[post56139-7] Rhombic (February 5, 2018). Re: Logic Life Search (discussion thread) at the ConwayLife.com forums

[note 1]

[note 2]

[1]

[2]

[3]

[4]

[5]

Tutorials/LLS: Difference between revisions

Latest revision as of 16:35, 25 September 2026

Contents

Installation

Prerequisites

Installing LLS

Staying up-to-date

Using the development version

Installing a SAT solver

Installing kissat

Installing Lingeling

First steps

Finding 25P3H1V0.2

Finding Brain

Finding an alien (2,1)c/3 spaceship

More complex tasks

Finding specific sequences

Predecessor searches (rewinding)

Success -- now what?

How do I...?

Finding the right parameter to pass to `-r`

Troubleshooting

Unsatisfiable

Bounding box too small

Notes

References

External links

Navigation menu

@@ Line 1: / Line 1: @@
 So you've decided to search for patterns using [[Oscar Cunningham]]'s [[Logic Life Search]] tool. Excellent!
-==Installation==
+== Installation ==
-===Prerequisites===
+=== Prerequisites ===
 Are you a Windows user? If so, you'll need a Unix-like environment.
-# Start by installing [http://cygwin.com/ Cygwin].
+. Start by installing WSL (Windows Subsystem for Linux) by running the following in your command prompt (the installation can take several minutes):
-# When prompted to choose which packages to install, make sure <tt>gcc-core</tt>, <tt>git</tt>, <tt>gzip</tt>, <tt>make</tt>, <tt>python2</tt>, and <tt>tar</tt> are all selected.
+ wsl --install
-# If prompted, confirm that you also want to install any required prerequisities.
+. Once WSL is installed, open WSL and create a user account with a username and password, and confirm the prompt regarding collection of platform metrics.
-===Installing LLS===
+. Update the package list using the following command:
-You can now install LLS itself. The easiest way to do this is using a shell (i.e. command line); you can also download a ZIP file and unpack it using your favorite archiver, but you'll be using the shell to run LLS anyway, so you might as well get used to it.
+ $ sudo apt update
+. Install the following packages using the following command:
+ $ sudo apt install -y build-essential git gzip python3 tar
+If you already have WSL 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 [https://gitlab.com/OscarCunningham/logic-life-search the LLS homepage], clicking the download button and selecting 'zip' and then unzipping this file to create the <tt>logic-life-search-master</tt> directory, which you can place anywhere convenient on your machine.
+If you prefer, you can use the [https://git-scm.com/ Git] version control system to download LLS and keep it updated. LLS is published on [https://en.wikipedia.org/wiki/GitLab GitLab]. Don't worry, you won't have to learn how to use Git,{{refn|group=note|If you're interested in doing so, refer to Git's documentation. The [https://git-scm.com/docs/gittutorial tutorial] is a good place to start.}}, 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):
 <pre>
-$ git clone https://github.com/OscarCunningham/logic-life-search.git
+$ git clone https://gitlab.com/OscarCunningham/logic-life-search.git
 Cloning into 'logic-life-search'...
 remote: Counting objects: 73, done.
@@ Line 25: / Line 34: @@
 </pre>
-This'll create a subdirectory called "logic-life-search" containing LLS. No further compilation is required.
+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.
-===Installing a SAT solver===
+=== Staying up-to-date ===
-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 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):
-LLS currently supports three SAT solvers: MiniSAT, Glucose and Lingeling. We'll focus on Lingeling in this tutorial, as it appears to work best across different platforms, including Windows/Cygwin.
+<pre>
+$ 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.
+$
+</pre>
+=== 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:{{refn|group=note|Despite the name, this is a local command that does not interact with the remote repository on GitLab.}}
+On May 15, 2022, commonly-used features were [https://conwaylife.com/forums/viewtopic.php?p=145609#p145609 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.
-====Installing Lingeling====
+<pre>
-Download Lingeling from [http://fmv.jku.at/lingeling/ its website]. You'll want the latest version; at the time of this writing, that's [http://fmv.jku.at/lingeling/lingeling-bbc-9230380-160707.tar.gz lingeling-bbc-9230380-160707.tar.gz].
+$ git checkout develop
+Switched to branch 'develop'
+Your branch is up to date with 'origin/develop'.
+$
+</pre>
-Next, extract the file you downloaded:
+To switch back to the stable "master" branch again, simply use "git checkout" again:
 <pre>
-$ tar xvfz lingeling-bbc-9230380-160707.tar.gz
+$ git checkout master
-lingeling-bbc-9230380-160707/
+Switched to branch 'master'
-lingeling-bbc-9230380-160707/lglib.c
+Your branch is up to date with 'origin/master'.
-lingeling-bbc-9230380-160707/mkconfig.sh
+$
-lingeling-bbc-9230380-160707/lgloptl.h
+</pre>
-lingeling-bbc-9230380-160707/configure.sh
-lingeling-bbc-9230380-160707/VERSION
+=== Installing a SAT solver ===
-lingeling-bbc-9230380-160707/makefile.in
+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.
-lingeling-bbc-9230380-160707/lglopts.c
-lingeling-bbc-9230380-160707/lgldimacs.c
+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 [https://github.com/arminbiere/kissat kissat].
-lingeling-bbc-9230380-160707/treengeling.c
-lingeling-bbc-9230380-160707/lglmbt.c
+==== Installing kissat ====
-lingeling-bbc-9230380-160707/lgluntrace.c
+Download kissat from [https://github.com/arminbiere/kissat]
-lingeling-bbc-9230380-160707/lglopts.h
+<div class="mw-collapsible mw-collapsed">
-lingeling-bbc-9230380-160707/COPYING
+Click on "Expand" to the right to view the detailed instructions for installing kissat.
-lingeling-bbc-9230380-160707/lglib.h
+<div class="mw-collapsible-content">
-lingeling-bbc-9230380-160707/ilingeling.c
+Start by "cloning" the code so you'll have a full copy (don't worry, this'll only take a few seconds):
-lingeling-bbc-9230380-160707/lglddtrace.c
-lingeling-bbc-9230380-160707/README
+<pre>$ git clone https://github.com/arminbiere/kissat.git
-lingeling-bbc-9230380-160707/lglbnr.c
+Cloning into 'kissat'...
-lingeling-bbc-9230380-160707/lglconst.h
+remote: Enumerating objects: 993, done.
-lingeling-bbc-9230380-160707/NEWS
+remote: Counting objects: 100% (121/121), done.
-lingeling-bbc-9230380-160707/lgldimacs.h
+remote: Compressing objects: 100% (55/55), done.
-lingeling-bbc-9230380-160707/plingeling.c
+remote: Total 993 (delta 86), reused 66 (delta 66), pack-reused 872
-lingeling-bbc-9230380-160707/blimc.c
+Receiving objects: 100% (993/993), 707.04 KiB | 2.87 MiB/s, done.
-lingeling-bbc-9230380-160707/lglmain.c
+Resolving deltas: 100% (443/443), done.</pre>
+Now enter kissat's directory:
+<pre>$ cd kissat
+</pre>
+Now run <tt>./configure && make test</tt> to build kissat. There may be some warnings; ignore these, they're Mostly Harmless&trade;.
+<pre>
+$ ./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.</pre>
+That's it, kissat is built. If you're on Windows/Cygwin, the executable will be called <tt>kissat.exe</tt>; otherwise (including other WSL) it's just <tt>kissat</tt>. You still need to copy this executable into LLS's solver directory, however:
+<pre>
+$ cp build/kissat.exe ../logic-life-search/solvers/
+$
+</pre>
+You also need to tell LLS to use kissat as its default solver. Go to the file <tt>logic-life-search/settings.py</tt> and change the 'solver' line to read <tt>solver = "kissat"</tt>.  As of February 2023 this is the default setting in the logic-life-search repo.
+</div>
+</div>
+==== Installing Lingeling ====
+Download Lingeling from [https://github.com/arminbiere/lingeling]
+<div class="mw-collapsible mw-collapsed">
+Click on "Expand" to the right to view the detailed instructions for installing lingeling.
+<div class="mw-collapsible-content">
+Start by "cloning" the code so you'll have a full copy (don't worry, this'll only take a few seconds):
+<pre>
+$ 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.
 $
 </pre>
@@ Line 70: / Line 159: @@
 <pre>
-$ cd lingeling-bbc-9230380-160707
+$ cd lingeling
 $ ./configure.sh
 gcc -Wall -O3 -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLDRUPLIG -DNLGLYALSAT -DNLGLFILES -DNLGLDEMA
@@ Line 122: / Line 211: @@
 </pre>
-That's it, Lingeling is built. If you're on Windows/Cygwin, the executable will be called <tt>lingeling.exe</tt>; otherwise it's just <tt>lingeling</tt>. You still need to copy this executable into LLS's solver directory, however:
+That's it, Lingeling is built. If you're on Windows/Cygwin, the executable will be called <tt>lingeling.exe</tt>; otherwise (including other WSL) it's just <tt>lingeling</tt>. You still need to copy this executable into LLS's solver directory, however:
 <pre>
@@ Line 129: / Line 218: @@
 </pre>
-==First steps==
+You also need to tell LLS to use lingeling as its default solver. Go to the file <tt>logic-life-search/settings.py</tt> and change the 'solver' line to read <tt>solver = "lingeling"</tt>.
+</div>
+</div>
-===Finding 25P3H1V0.2===
+== First steps ==
-For our first test, let's find [[25P3H1V0.2]], a small [[speed of light|c]]/3 [[spaceship]] originally found by [[David Bell]] in {{year|1992}}.
+=== Finding 25P3H1V0.2 ===
+For our first test, let's find [[25P3H1V0.1]],<ref name="post55778" /> a small [[speed of light|c]]/3 [[spaceship]] originally found by [[David Bell]] in {{year|1992}}.
 Enter LLS's directory if necessary, and run the following:
 <pre>
-$ ./lls -S lingeling -m -b 16 6 -p 3 -x 0 -y 1
+$ python lls -c -b 16 6 -s p3 x0 y1
 Getting search pattern...
 Done
@@ Line 145: / Line 237: @@
 Done
-Number of undetermined cells: 270
+Number of undetermined cells: 272
-Number of variables: 364
+Number of variables: 369
-Number of clauses: 34177
+Number of clauses: 34412
 Active width: 16
@@ Line 156: / Line 248: @@
 Done
-Time taken: 2.46514105797 seconds
+Time taken: 1.7274296283721924 seconds
 x = 18, y = 8, rule = B3/S23
 bbbbbbbbbbbbbbbbbb$
-bbbbbbbbbbbbbobbob$
+bbobbbbbbbbbbbbbbb$
-bobboboobbbobboobb$
+bobbbobbbobbbbbobb$
-bboobbbbobbooboobb$
+bbooobbbobbobobbob$
-bboobooobooobbbbbb$
+bbboboobbbbooboobb$
-bbbbbbbbbobbbbbbbb$
+bbbbbbboooboobobbb$
 bbbbbbbbbbbbbbbbbb$
 bbbbbbbbbbbbbbbbbb!
@@ Line 171: / Line 263: @@
 </pre>
-LLS converted your request to a problem Lingeling could solve, and Lingeling did so in less than 3 seconds. Impressive! Here's your result:
+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:
 {{EmbedViewer
-|caption      = [[25P3H1V0.2]]
+|caption      = [[25P3H1V0.1]]
 |position     = center
 |viewerconfig = #C [[ THEME 6 GRID TRACKLOOP 3 0 1/3 AUTOSTART THUMBLAUNCH THUMBSIZE 2 GPS 3 ]]
 |rle          = x = 18, y = 8, rule = B3/S23
 bbbbbbbbbbbbbbbbbb$
-bbbbbbbbbbbbbobbob$
+bbobbbbbbbbbbbbbbb$
-bobboboobbbobboobb$
+bobbbobbbobbbbbobb$
-bboobbbbobbooboobb$
+bbooobbbobbobobbob$
-bboobooobooobbbbbb$
+bbboboobbbbooboobb$
-bbbbbbbbbobbbbbbbb$
+bbbbbbboooboobobbb$
 bbbbbbbbbbbbbbbbbb$
 bbbbbbbbbbbbbbbbbb!
 }}
-But what ''did'' you request? Let's take a look at the options you passed to LLS:
+But what ''did'' we request? Let's take a look at the options we passed to LLS:
-* <tt>-S lingeling</tt>: tells LLS to use Lingeling as its SAT solver. The default solver to use is Glucose, but we installed Lingeling and would like to use that.
+* <tt>-c</tt>: tells LLS to look for a changing pattern, i.e. for the first two generations to be different.
-* <tt>-m</tt>: tells LLS to look for a moving pattern, i.e. for the first two generations to be different.
+* <tt>-b 16 6</tt>: tells LLS to create a blank search pattern with a size of 16&times;6. Without this, we'd have to have told LLS explicitly what our pattern should look like.
-* <tt>-b 16 6</tt>: tells LLS to create a blank search pattern with a size of 16&times;6. Without this, we'd have to have told LLS explicitely what our pattern should look like.
+* <tt>-s</tt>: tells LLS to look for a pattern with a particular symmetry:
-* <tt>-p 3</tt>: tells LLS to look for a [[period]] 3 pattern.
+** <tt>p3</tt> the pattern repeats itself with [[period]] 3,
-* <tt>-x 0</tt>: tells LLS to look for a pattern moving by 0 cells horizontally in each full period.
+** <tt>x0</tt>: moving by 0 cells horizontally in each full period,
-* <tt>-y 1</tt>: tells LLS to look for a pattern moving by 1 cell vertically in each full period.
+** <tt>y1</tt>: and moving by 1 cell vertically in each full period.
 There's a lot more options to LLS; run <tt>./lls -h</tt> to see them all.
-===Finding Brain===
+=== Finding Brain ===
-Let's try hunting for a different spaceship, [[Brain]]. Run the following:
+Let's try hunting for a different spaceship, [[Brain]].<ref name="post55792" /> Run the following:
 <pre>
-$ ./lls -S lingeling -m -b 17 12 -s "D2|" -p 3 -x 0 -y 1
+$ python lls -c -b 17 12 -s p3 x0 y1 -s "D2|"
 Getting search pattern...
@@ Line 211: / Line 303: @@
 Done
-Number of undetermined cells: 314
+Number of undetermined cells: 315
-Number of variables: 516
+Number of variables: 424
-Number of clauses: 43417
+Number of clauses: 43369
 Active width: 17
@@ Line 222: / Line 314: @@
 Done
-Time taken: 40.4900970459 seconds
+Time taken: 57.500898599624634 seconds
 x = 19, y = 14, rule = B3/S23
 bbbbbbbbbbbbbbbbbbb$
-bbbbbbbooboobbbbbbb$
+bbobbbbbbbbbbbbbobb$
-booobobbbbbbbobooob$
+bbobbbbooboobbbbobb$
-bbbbbbbbobobbbbbbbb$
+bbboobbobbbobboobbb$
-bbbobbobobobobbobbb$
+bbbooobbobobbooobbb$
 bbbooboboboboboobbb$
+bbbbobobobobobobbbb$
 bbbbbbobobobobbbbbb$
-bbbbbobbobobbobbbbb$
+bbobooboobooboobobb$
-bobobbbooboobbbobob$
+bobobobbbbbbbobobob$
-bobbboobbbbboobbbob$
+boboboobbbbboobobob$
-bbooboobbbbbooboobb$
+bbooobbbbbbbbbooobb$
-bboobbbbbbbbbbboobb$
 bbbbbbbbbbbbbbbbbbb$
 bbbbbbbbbbbbbbbbbbb!
@@ Line 243: / Line 335: @@
 </pre>
 seconds &mdash; not bad! Here's our catch:
 {{EmbedViewer
@@ Line 251: / Line 343: @@
 |rle          = x = 19, y = 14, rule = B3/S23
 bbbbbbbbbbbbbbbbbbb$
-bbbbbbbooboobbbbbbb$
+bbobbbbbbbbbbbbbobb$
-booobobbbbbbbobooob$
+bbobbbbooboobbbbobb$
-bbbbbbbbobobbbbbbbb$
+bbboobbobbbobboobbb$
-bbbobbobobobobbobbb$
+bbbooobbobobbooobbb$
 bbbooboboboboboobbb$
+bbbbobobobobobobbbb$
 bbbbbbobobobobbbbbb$
-bbbbbobbobobbobbbbb$
+bbobooboobooboobobb$
-bobobbbooboobbbobob$
+bobobobbbbbbbobobob$
-bobbboobbbbboobbbob$
+boboboobbbbboobobob$
-bbooboobbbbbooboobb$
+bbooobbbbbbbbbooobb$
-bboobbbbbbbbbbboobb$
 bbbbbbbbbbbbbbbbbbb$
 bbbbbbbbbbbbbbbbbbb!
 }}
-We already know the <tt>-m</tt>, <tt>-b</tt>, <tt>-p</tt>, <tt>-x</tt>, and <tt>-y</tt> options from above. But there's one new one:
+We already know the <tt>-c</tt>, <tt>-b</tt> and <tt>-s p3 x0 y1</tt> options from above. But there's one new one:
-* <tt>-s "D2|"</tt>: tells LLS to look for patterns with a specific [[symmetry]]. We passed <tt>"D2|"</tt>, meaning we're interested in patterns that are mirror-symmetric about a vertical axis. The quotes around <tt>D2|</tt> are necessary to keep the shell from interpreting the pipe symbol, <tt>|</tt>, as a special character, and instead pass it to LLS unchanged.
+* <tt>-s "D2|"</tt>: tells LLS to look for patterns with an additional [[symmetry]]. We passed <tt>"D2|"</tt>, meaning we're interested in patterns that are mirror-symmetric about a vertical axis. The quotes around <tt>D2|</tt> are necessary to keep the shell from interpreting the pipe symbol, <tt>|</tt>, 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===
+=== Finding an alien (2,1)c/3 spaceship ===
-LLS can search different rules. It's not limited to [[Life-like cellular automaton|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]]:
+LLS can search different rules. It's not limited to [[Life-like cellular automaton|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)[[speed of light|c]]/3:<ref name="post55864 " />
 <pre>
-$ ./lls -S lingeling -p 3 -x 2 -y 1 -i -b 6 6 -r pB1-c2345678/S012345678 --force_at_most 5
+$ python lls -s p3 x2 y1 -b 6 6 -r pB1-c2345678/S012345678 -p ">0" -p "<=5"
 Getting search pattern...
@@ Line 284: / Line 376: @@
 Done
-Number of undetermined cells: 84
+Number of undetermined cells: 86
-Number of variables: 242
+Number of variables: 306
-Number of clauses: 36602
+Number of clauses: 38100
 Active width: 6
@@ Line 295: / Line 387: @@
 Done
-Time taken: 0.455801963806 seconds
+Time taken: 0.20017600059509277 seconds
-x = 8, y = 8, rule = B2-ei3jq4-aijnwz5-cejn6-c78/S12ck3-ekqr4-ejknr5ejkqy6cn78
+x = 8, y = 8, rule = B2-en3ejr4ant/S01c2-en3ey5ae
+bbbbbbbb$
 bbbbbbbb$
 bbbbobbb$
-bbobbbbb$
+bbbbobbb$
-bbboobbb$
+bbbbobbb$
-bbbbbbbb$
+bobobbbb$
-bobbbbbb$
 bbbbbbbb$
 bbbbbbbb!
@@ Line 311: / Line 403: @@
 {{EmbedViewer
-|caption      = An alien (2,1)c/3.
+|caption      = An alien (2,1)c/3 ship.
 |position     = center
 |viewerconfig = #C [[ THEME 6 GRID TRACKLOOP 3 2/3 1/3 AUTOSTART THUMBLAUNCH THUMBSIZE 2 GPS 3 ]]
-|rle          = x = 8, y = 8, rule = B2-ei3jq4-aijnwz5-cejn6-c78/S12ck3-ekqr4-ejknr5ejkqy6cn78
+|rle          = x = 8, y = 8, rule = B2-en3ejr4ant/S01c2-en3ey5ae
+bbbbbbbb$
 bbbbbbbb$
 bbbbobbb$
-bbobbbbb$
+bbbbobbb$
-bbboobbb$
+bbbbobbb$
-bbbbbbbb$
+bobobbbb$
-bobbbbbb$
 bbbbbbbb$
 bbbbbbbb!
 }}
-Most of the options passed to LLS are familiar by now, but three are new:
+Most of the options passed to LLS are familiar by now, but two are new:
 [[File:Neighborhood 1c.png|right|frame|<tt>B1c</tt>]]
-* <tt>-i</tt>: tells LLS that the first generation of the pattern found must contain at least one live cell. We're not interested in empty solutions.
+* <tt>-r pB1-c2345678/S012345678</tt>: tells LLS what birth/survival conditions we'll allow in our target rules. In <tt>pB1-c2345678/S012345678</tt>, the leading <tt>p</tt> tells LLS that the following is a partial specification, rather than a complete one. The trailing string, <tt>B1-c2345678/S012345678</tt>, describes the [[rulespace]] we'd like to be considered. Here, <tt>B1-c</tt> 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 <tt>-r</tt>, see [[Tutorials/LLS#Finding the right parameter to pass to -r|§ Finding the right parameter to pass to <tt>-r</tt>]].
-* <tt>-r pB1-c2345678/S012345678</tt>: tells LLS what birth/survival conditions we'll allow in our target rules. In <tt>pB1-c2345678/S012345678</tt>, the leading <tt>p</tt> tells LLS that the following is a partial specification, rather than a complete one. The trailing string, <tt>B1-c2345678/S012345678</tt>, describes the [[rulespace]] we'd like to be considered. Here, <tt>B1-c</tt> rules out  the "B1c" subcondition. B1e, B2 to B8, and S0 to S8 are all allowed.
+* <tt>-p ">0"</tt>: 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 <tt>-p "<=5"</Tt> tells LLS that the first generation of the pattern found must contain at most five live cells.
-* <tt>--force_at_most 5</Tt>: tells LLS that the first generation of the pattern found must contain at most five live cells.
+The last option <tt>-p "<=5"</Tt> 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.
+== More complex tasks ==
+=== Finding specific sequences ===
+So we've used LLS to find a few spaceships, cool. But there's much more power to this program than that. Now we're gonna try to find a pattern that evolves in a certain way. Specifically, we're gonna use LLS to find an [[eater]].
+How do we do that? First, make a text file in your LLS folder. Name it whatever you want, but I would personally stick to naming it "eater".
+Now paste all of this into the file:
+<pre>
+, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
+, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0
+, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0
+, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0
+, 0, 0, a, b, c, d, e, 0, 0, 0, 0, 0, 0, 0
+, 0, 0, f, g, h, i, j, 0, 0, 0, 0, 0, 0, 0
+, 0, 0, k, l, n, m, o, 0, 0, 0, 0, 0, 0, 0
+, 0, 0, p, q, r, s, t, 0, 0, 0, 0, 0, 0, 0
+, 0, 0, u, v, w, x, y, 0, 0, 0, 0, 0, 0, 0
+, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
+, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
+, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
+, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 1, 0, 0, 0
+, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0
+, 0, 0, a, b, c, d, e, 0, 0, 1, 0, 0, 0, 0
+, 0, 0, f, g, h, i, j, 0, 0, 0, 0, 0, 0, 0
+, 0, 0, k, l, n, m, o, 0, 0, 0, 0, 0, 0, 0
+, 0, 0, p, q, r, s, t, 0, 0, 0, 0, 0, 0, 0
+, 0, 0, u, v, w, x, y, 0, 0, 0, 0, 0, 0, 0
+, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
+, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
+, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
+, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
+, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
+, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
+, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
+, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
+, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
+, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
+, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
+, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
+, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
+, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
+, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
+, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
+, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
+, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
+, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
+, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
+, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
+, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
+, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
+, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
+, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
+, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
+, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
+, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
+, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
+, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
+, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
+, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
+, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
+, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
+, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
+, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
+, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
+, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
+, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
+, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
+, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
+, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
+, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
+, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
+, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
+, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
+, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
+, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
+, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
+, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
+, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
+, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
+, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
+, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
+, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
+, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
+, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
+, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
+, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
+, 0, *, *, *, *, *, *, *, *, *, *, 0, 0, 0
+, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
+, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
+, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
+, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
+, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
+, 0, 0, a, b, c, d, e, 0, 0, 0, 0, 0, 0, 0
+, 0, 0, f, g, h, i, j, 0, 0, 0, 0, 0, 0, 0
+, 0, 0, k, l, n, m, o, 0, 0, 0, 0, 0, 0, 0
+, 0, 0, p, q, r, s, t, 0, 0, 0, 0, 0, 0, 0
+, 0, 0, u, v, w, x, y, 0, 0, 0, 0, 0, 0, 0
+, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
+</pre>
+But wait, before we do that, what does all of this actually mean?
+Each separated array of characters represents what we want to happen on a specific [[generation]], so the first array represents generation 0, the second generation 1, etc. There are 3 different characters used here, representing what states we want the cells to be.
+* 0 marks a dead cell, 1 marks a live cell
+* An asterisk (*) marks a cell that can be in either state
+* The letters (and anything else besides 0, 1, and *) represent variables. Variables are cells that must be in the same state on all generations they appear on.
+So can you decipher what exactly we're asking LLS to do?
+We are looking for a sequence that goes as follows:
+* A [[glider]] moves towards a square of cells that stay in the same state for two generations
+* When the glider and cells collide, it results in chaos that isn't easy to predict, so cells can be in any state in the immediate area. This array is repeated for several generations, just in case.
+* On the final generation, the cells from the start must be in the same state they were in the beginning.
+Now, save the text file, run LLS simply with the file name as the only parameter
+<pre>
+python lls (file name).txt
+</pre>
+And it will spit out a pattern that evolves off of the conditions we gave it. Shortly after, you should see this as a result:
+<pre>
+x = 17, y = 12, rule = B3/S23
+bbbbbbbbbbbbbbbbb$
+bbbbbbbbbbbbbbbbb$
+bbbbbbbbbbbobbbbb$
+bbbbbbbbbbobbbbbb$
+bbbbbbbbbbooobbbb$
+bbbbbbbbbbbbbbbbb$
+bbbbbbboobbbbbbbb$
+bbbbbbobobbbbbbbb$
+bbbbbbobbbbbbbbbb$
+bbbbboobbbbbbbbbb$
+bbbbbbbbbbbbbbbbb$
+bbbbbbbbbbbbbbbbb!
+</pre>
+And if by looking at the RLE given to us in a program, we can see that LLS gave us a glider and... [[Eater 1]]!
+{{EmbedViewer
+|caption      =
+|position     = center
+|rle          = x = 8, y = 8, rule = B3/S23
+bo$5bo$5b3o2$2b2o$bobo$bo$2o!
+}}
+So now you know how to use a series of conditions like this to find a complex sequence. With this knowledge, you can find hasslers, reflectors, predecessors, patterns that emit specific objects, etc. And on the topic of predecessors...
+=== Predecessor searches (rewinding) ===
+Another thing that LLS is very good at is searching for predecessors. Suppose you have a pattern for which no predecessor is known, e.g.,
+{{EmbedViewer
+|caption      = sample 16x16 pattern for which a predecessor is wanted
+|position     = center
+|rle          = x = 16, y = 16, rule = B3/S23
+o3bo2b2o2b5o$o3bobo2bo3bo$2o2bobo2bo3bo$obobobo2bo3bo$o2b2obo2bo3bo$o
+bobo2bo3bo$o3bo2b2o4bo3$3o2b2o2b3obobo$o3bo2bobo3bobo$o3bo2bobo3bobo$
+obo2bob3o2b2o$o3b4o3bo2bo$o3bo2bo3bo2bo$b2obo2bob3o2bo!
+}}
+The basic steps for using LLS to find predecessors are laid out in a 2022 forum post by Macbi.<ref name="post141799" />
+First we can find out whether the target pattern has any patterns that fit into the same 16x16 box.  Create a file called (say) '''16x16-predecessor-search.txt''', as follows:
+<pre>0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0
+,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0
+,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
+,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
+,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
+,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
+,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
+,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
+,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
+,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
+,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
+,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
+,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
+,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
+,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
+,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
+,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
+,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
+,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0
+,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0
+,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0
+,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0
+,0,1,0,0,0,1,0,0,1,1,0,0,1,1,1,1,1,0,0
+,0,1,0,0,0,1,0,1,0,0,1,0,0,0,1,0,0,0,0
+,0,1,1,0,0,1,0,1,0,0,1,0,0,0,1,0,0,0,0
+,0,1,0,1,0,1,0,1,0,0,1,0,0,0,1,0,0,0,0
+,0,1,0,0,1,1,0,1,0,0,1,0,0,0,1,0,0,0,0
+,0,1,0,0,0,1,0,1,0,0,1,0,0,0,1,0,0,0,0
+,0,1,0,0,0,1,0,0,1,1,0,0,0,0,1,0,0,0,0
+,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0
+,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0
+,0,1,1,1,0,0,1,1,0,0,1,1,1,0,1,0,1,0,0
+,0,1,0,0,0,1,0,0,1,0,1,0,0,0,1,0,1,0,0
+,0,1,0,0,0,1,0,0,1,0,1,0,0,0,1,0,1,0,0
+,0,1,1,1,0,1,0,0,1,0,1,1,1,0,0,1,1,0,0
+,0,1,0,0,0,1,1,1,1,0,0,0,1,0,0,1,0,0,0
+,0,1,0,0,0,1,0,0,1,0,0,0,1,0,0,1,0,0,0
+,0,0,1,1,0,1,0,0,1,0,1,1,1,0,0,1,0,0,0
+,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0
+,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0
+</pre>
+Then run LLS:
+<pre>
+python lls 16x16-predecessor-search.txt
+</pre>
+This particular search quickly comes back with UNSATISFIABLE, so there are no 16x16 predecessors of this 16x16 pattern.  We'll have to extend the boundaries a little.
+For this example, let's also extend the search so that it finds a 2-generation predecessor.  Here's a sample revised input file:
+<pre>
+,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0
+,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
+,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0
+,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0
+,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0
+,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0
+,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0
+,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0
+,*,*,*,*,*,*,*,*,*,*,0,*,*,*,*,*,*,*,*,*,0
+,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0
+,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0
+,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0
+,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0
+,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0
+,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0
+,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0
+,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0
+,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0
+,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
+,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0
+,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0
+,0,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0,0
+,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
+,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
+,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
+,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
+,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
+,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
+,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
+,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
+,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
+,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
+,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
+,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
+,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
+,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
+,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0
+,0,0,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,*,0,0,0
+,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0
+,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0
+,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0
+,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0
+,0,0,1,0,0,0,1,0,0,1,1,0,0,1,1,1,1,1,0,0,0
+,0,0,1,0,0,0,1,0,1,0,0,1,0,0,0,1,0,0,0,0,0
+,0,0,1,1,0,0,1,0,1,0,0,1,0,0,0,1,0,0,0,0,0
+,0,0,1,0,1,0,1,0,1,0,0,1,0,0,0,1,0,0,0,0,0
+,0,0,1,0,0,1,1,0,1,0,0,1,0,0,0,1,0,0,0,0,0
+,0,0,1,0,0,0,1,0,1,0,0,1,0,0,0,1,0,0,0,0,0
+,0,0,1,0,0,0,1,0,0,1,1,0,0,0,0,1,0,0,0,0,0
+,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0
+,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0
+,0,0,1,1,1,0,0,1,1,0,0,1,1,1,0,1,0,1,0,0,0
+,0,0,1,0,0,0,1,0,0,1,0,1,0,0,0,1,0,1,0,0,0
+,0,0,1,0,0,0,1,0,0,1,0,1,0,0,0,1,0,1,0,0,0
+,0,0,1,1,1,0,1,0,0,1,0,1,1,1,0,0,1,1,0,0,0
+,0,0,1,0,0,0,1,1,1,1,0,0,0,1,0,0,1,0,0,0,0
+,0,0,1,0,0,0,1,0,0,1,0,0,0,1,0,0,1,0,0,0,0
+,0,0,0,1,1,0,1,0,0,1,0,1,1,1,0,0,1,0,0,0,0
+,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0
+,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0
+</pre>
+In about a second, this search will return a valid 2-tick predecessor of the target pattern:
+{{EmbedViewer
+|caption      = sample 16x16 pattern for which a predecessor is wanted
+|position     = center
+|rle          = x = 20, y = 18, rule = B3/S23
+bo2bobobobo2bobobo$o3bob3o2bo2bobo$ob2obobo6b2obo$6bobobo2bo2bo$ob2o
+bo2bob3o2b4o$o4b2o2b2o4bobo$4b3obobo2bo$2bo6bo3b2o$o2bo3b3o2bo2b2o$o
+b2o3b3o7bo$3bob2o3b2o2b2obobo$bob4o2bo4b3o$2b2o4bo3bobo$2bo3bo2bo3bo
+b2obo$5bo6bob3o$2bob3ob4obobobobo$12bo$bobobo5bo2b2ob2o!
+}}
+Notice the "0" toward the center of the "minus-two" generation's target pattern, in the input file above -- and also the extra "0"s in the corners. Replace the central "0" with a "1" and a different predecessor will be generated. When rewinding patterns through multiple generations, it's often useful to experiment with additional constraints like this, to make sure that there are multiple possible choices of ancestor and reduce the likelihood of arriving at a [[Garden of Eden]] dead end.
+A 16x16 pattern's predecessor seems to have a tendency to be larger than it is, by about one cell on each side. That's a very rough average, though, not necessarily true in any specific case! Larger patterns may have to add two rows or columns of cells along each edge to enable a solution to be found.
+It's an open question whether there are workable ways to constrain predecessors in such a way that ''their'' predecessors will be easier to find.
+== 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:
+{{cata|object|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)
+{{LinkForumThread|f=2|t=2031|title=Spaceship Discussion Thread}}
+{{LinkForumThread|f=2|t=1437|title=Oscillator Discussion Thread}}
+{{LinkForumThread|f=2|t=576|title=Thread for your unsure discoveries}}
+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 <tt>-r</tt>===
+LLS's <tt>-r</tt> 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.<ref name="post56139" />
+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 <tt>pB3aceijknqry5-acijknqry8/S2acekn-i3aceijknqry4q-aijknrtwyz6-acekn7-c8</tt>, so this is the option you should pass to <tt>-r</tt> 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:
+<pre>
+$ 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
+$
+</pre>
+We asked for a deplacement of <tt>x9</tt> while also requiring the entire pattern to fit into a 10&times;10 bounding box (<tt>-b 10 10</tt>), and LLS and the SAT solver quickly determined that there was no way that a period-55 (<tt>-p 55</tt>) pattern meeting both these criteria could possibly exist.
-The last option is important; without it, Lingeling (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.
+Solution: Passing a larger bounding box should help.
-==Troubleshooting==
+== Notes ==
+<references group="note" />
-:''to be written...''
+== References ==
+<references>
+<ref name="post55778">{{LinkForumThread
+|format     = ref
+|accessdate = January 30, 2018
+|date       = January 28, 2018
+|p          = 55778
+|title      = Re: Logic Life Search
+|author     = [[Tom Rokicki]]
+}}</ref>
+<ref name="post55792">{{LinkForumThread
+|format     = ref
+|accessdate = January 30, 2018
+|date       = January 28, 2018
+|p          = 55792
+|title      = Re: Logic Life Search
+|author     = [[Adam P. Goucher]]
+}}</ref>
+<ref name="post55864">{{LinkForumThread
+|format     = ref
+|accessdate = January 30, 2018
+|date       = January 29, 2018
+|p          = 55864
+|title      = Re: Logic Life Search
+|author     = [[Oscar Cunningham]]
+}}</ref>
+<ref name="post56139">{{LinkForumThread
+|format     = ref
+|accessdate = February 4, 2018
+|date       = February 5, 2018
+|p          = 56139
+|title      = Re: Logic Life Search
+|author     = [[Rhombic]]
+}}</ref>
+<ref name="post141799">{{LinkForumThread
+|format     = ref
+|date       = February 18, 2022
+|p          = 141799
+|title      = Re: Algorithm for reversing the GoL rules
+|author     = [[Oscar Cunningham]]
+}}</ref>
+</references>
-==External links==
+== External links ==
-* [https://github.com/OscarCunningham/logic-life-search Logic Life Search] on GitHub
+* [https://gitlab.com/OscarCunningham/logic-life-search Logic Life Search] on GitLab
 {{LinkForumThread|f=9|t=3247|title=Logic Life Search}}
 * SAT solvers:
-** [http://fmv.jku.at/lingeling/ Lingeling]
+** [https://github.com/arminbiere/kissat Kissat]
-** [http://www.labri.fr/perso/lsimon/glucose/ Glucose]
+** [https://github.com/arminbiere/cadical CaDiCaL]
-** [http://minisat.se/ MiniSAT]
+** [http://fmv.jku.at/lingeling/ Lingeling] (404's, see [https://web.archive.org/web/20221012181739/http://fmv.jku.at/lingeling archive.org])
-[[Category:Tutorials|LLS]]
+{{Tutorial}}