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.

1. Start by installing Cygwin
2. When prompted to choose which packages to install, make sure dos2unix, gcc-core, git, gzip, make, python2, and tar are all selected.
3. If prompted, confirm that you also want to install any required prerequisities.

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

LLS is published on GitHub, which uses Git as its version control system. Don't worry, you won't have to learn how to use Git,, but you'll be using a few commands to download LLS and keep it updated.

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

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://github.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:

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

Note that the development version has some differences with the regular "master" version. These differences are noted in the Development Version Differences section.

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

Installing Lingeling

Download Lingeling from its website. You'll want the latest version; as of June 2018, that's lingeling-bcj-78ebb86-180517.tar.gz.

Next, extract the file you downloaded (version may differ):

$ tar xvfz lingeling-bbc-9230380-160707.tar.gz
lingeling-bbc-9230380-160707/
lingeling-bbc-9230380-160707/lglib.c
lingeling-bbc-9230380-160707/mkconfig.sh
lingeling-bbc-9230380-160707/lgloptl.h
lingeling-bbc-9230380-160707/configure.sh
lingeling-bbc-9230380-160707/VERSION
lingeling-bbc-9230380-160707/makefile.in
lingeling-bbc-9230380-160707/lglopts.c
lingeling-bbc-9230380-160707/lgldimacs.c
lingeling-bbc-9230380-160707/treengeling.c
lingeling-bbc-9230380-160707/lglmbt.c
lingeling-bbc-9230380-160707/lgluntrace.c
lingeling-bbc-9230380-160707/lglopts.h
lingeling-bbc-9230380-160707/COPYING
lingeling-bbc-9230380-160707/lglib.h
lingeling-bbc-9230380-160707/ilingeling.c
lingeling-bbc-9230380-160707/lglddtrace.c
lingeling-bbc-9230380-160707/README
lingeling-bbc-9230380-160707/lglbnr.c
lingeling-bbc-9230380-160707/lglconst.h
lingeling-bbc-9230380-160707/NEWS
lingeling-bbc-9230380-160707/lgldimacs.h
lingeling-bbc-9230380-160707/plingeling.c
lingeling-bbc-9230380-160707/blimc.c
lingeling-bbc-9230380-160707/lglmain.c
$ 

Now enter Lingeling's directory, and run configure.sh:

$ cd lingeling-bbc-9230380-160707
$ ./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 it's just lingeling. You still need to copy this executable into LLS's solver directory, however:

$ cp lingeling.exe ../logic-life-search/solvers/
$ 

First steps

Finding 25P3H1V0.2

For our first test, let's find 25P3H1V0.2, a small c/3 spaceship originally found by David Bell in 1992.

Enter LLS's directory if necessary, and run the following:

$ ./lls -S lingeling -m -b 16 6 -p 3 -x 0 -y 1

Getting search pattern...
Done

Preprocessing...
Done

Number of undetermined cells: 270
Number of variables: 364
Number of clauses: 34177

Active width: 16
Active height: 6
Active duration: 4

Solving...
Done

Time taken: 2.46514105797 seconds

x = 18, y = 8, rule = B3/S23
bbbbbbbbbbbbbbbbbb$
bbbbbbbbbbbbbobbob$
bobboboobbbobboobb$
bboobbbbobbooboobb$
bboobooobooobbbbbb$
bbbbbbbbbobbbbbbbb$
bbbbbbbbbbbbbbbbbb$
bbbbbbbbbbbbbbbbbb!

$ 

LLS converted our request to a problem Lingeling could solve, and Lingeling did so in less than 3 seconds. Impressive! Here's our result:

x = 18, y = 8, rule = B3/S23 bbbbbbbbbbbbbbbbbb$ bbbbbbbbbbbbbobbob$ bobboboobbbobboobb$ bboobbbbobbooboobb$ bboobooobooobbbbbb$ bbbbbbbbbobbbbbbbb$ 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.2 (click above to open LifeViewer)

But what did we request? Let's take a look at the options we passed to LLS:

• -S lingeling: 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.
• -m: tells LLS to look for a moving 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.
• -p 3: tells LLS to look for a period 3 pattern.
• -x 0: tells LLS to look for a pattern moving by 0 cells horizontally in each full period.
• -y 1: tells LLS to look for a pattern 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. Run the following:

$ ./lls -S lingeling -m -b 17 12 -s "D2|" -p 3 -x 0 -y 1

Getting search pattern...
Done

Preprocessing...
Done

Number of undetermined cells: 314
Number of variables: 516
Number of clauses: 43417

Active width: 17
Active height: 12
Active duration: 4

Solving...
Done

Time taken: 40.4900970459 seconds

x = 19, y = 14, rule = B3/S23
bbbbbbbbbbbbbbbbbbb$
bbbbbbbooboobbbbbbb$
booobobbbbbbbobooob$
bbbbbbbbobobbbbbbbb$
bbbobbobobobobbobbb$
bbbooboboboboboobbb$
bbbbbbobobobobbbbbb$
bbbbbobbobobbobbbbb$
bobobbbooboobbbobob$
bobbboobbbbboobbbob$
bbooboobbbbbooboobb$
bboobbbbbbbbbbboobb$
bbbbbbbbbbbbbbbbbbb$
bbbbbbbbbbbbbbbbbbb!

$ 

40 seconds — not bad! Here's our catch:

x = 19, y = 14, rule = B3/S23 bbbbbbbbbbbbbbbbbbb$ bbbbbbbooboobbbbbbb$ booobobbbbbbbobooob$ bbbbbbbbobobbbbbbbb$ bbbobbobobobobbobbb$ bbbooboboboboboobbb$ bbbbbbobobobobbbbbb$ bbbbbobbobobbobbbbb$ bobobbbooboobbbobob$ bobbboobbbbboobbbob$ bbooboobbbbbooboobb$ bboobbbbbbbbbbboobb$ 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 -m, -b, -p, -x, and -y options from above. But there's one new one:

• -s "D2|": tells LLS to look for patterns with a specific 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:

$ ./lls -S lingeling -p 3 -x 2 -y 1 -i -b 6 6 -r pB1-c2345678/S012345678 --force_at_most 5

Getting search pattern...
Done

Preprocessing...
Done

Number of undetermined cells: 84
Number of variables: 242
Number of clauses: 36602

Active width: 6
Active height: 6
Active duration: 4

Solving...
Done

Time taken: 0.455801963806 seconds

x = 8, y = 8, rule = B2-ei3jq4-aijnwz5-cejn6-c78/S12ck3-ekqr4-ejknr5ejkqy6cn78
bbbbbbbb$
bbbbobbb$
bbobbbbb$
bbboobbb$
bbbbbbbb$
bobbbbbb$
bbbbbbbb$
bbbbbbbb!

What did we find this time? Let us take a look:

x = 8, y = 8, rule = B2-ei3jq4-aijnwz5-cejn6-c78/S12ck3-ekqr4-ejknr5ejkqy6cn78 bbbbbbbb$ bbbbobbb$ bbobbbbb$ bbboobbb$ bbbbbbbb$ bobbbbbb$ 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 three are new:

B1c

• -i: tells LLS that the first generation of the pattern found must contain at least one live cell. We're not interested in empty solutions.
• -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.
• --force_at_most 5: tells LLS that the first generation of the pattern found must contain at most five live cells.

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.

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:

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

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:

$ ./lls -S lingeling -r B2en3ij4a5e7e8/S1c2cek3-a4aiqw5aky -b 10 10 -p 55 -x 9 -y 0 -i

Getting search pattern...
Done

Preprocessing...
Done

Number of undetermined cells: 0
Number of variables: 0
Number of clauses: 1

Active width: 0
Active height: 0
Active duration: 0

Solving...
Done

Time taken: 0.0 seconds

Unsatisfiable

$ 

We asked for a deplacement of 9 -x 9 while also requiring the entire pattern to fit into a 10×10 bounding box (-b 10 10), and LLS and Lingeling 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.

Incompatible line-end characters

Possible explanation: you used an input text file created on Windows, which uses different line-end characters than what Unix-based tools expect. Windows uses \r\n; Unix uses just \n, and LLS is interpreting each line of your input file as representing an entire generation of the pattern.

Solution: this should be fixed in the "develop" branch of LLS; see § Using the development version for instructions on how to switch to that version. Alternatively, use the dos2unix tool to convert your input file to Unix line endings:

$ dos2unix.exe input.txt
dos2unix: converting file input.txt to Unix format...
$ 

Development Version Differences

The Development version of LLS has some differences with the regular version in it's commands. It might be a bit tricky to figure out how to use the development version, so here's a quick guide:

• Parameters for the search are now passed into the -s option, so for example, while in the regular version search parameters would be written, say, -p 4 -x 1 -y 2, in the development version, they would be written -s p4 x1 y2
  • Symmetries are also now in the -s option, so -p 4 -x 1 -y 0 -s "D2-" in the regular version would be -s p4 x1 y0 "D2-" in the development version.
• The -i option is gone. A replacement for it is the -c, which forces the first two generations of the pattern to be different. If you wish to tell LLS to make the first generation have at least one live cell, use -p ">1", which says "Make sure the population is greater than ( ">" ) one ( "1" ).
• The --force_at_most option is gone as well. Use the -p option.

External links

• Logic Life Search on GitHub

• Logic Life Search (discussion thread) at the ConwayLife.com forums
• SAT solvers:
  • Lingeling
  • Glucose
  • MiniSAT