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 gcc-core, git, gzip, make, python2, and tar are all selected.
3. If prompted, confirm that you also want to install any required prerequisities.

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.

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.

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; at the time of this writing, that's lingeling-bbc-9230380-160707.tar.gz.

Next, extract the file you downloaded:

$ 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 your request to a problem Lingeling could solve, and Lingeling did so in less than 3 seconds. Impressive! Here's your 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 TRACKLOOP 3 0 1/3 AUTOSTART THUMBLAUNCH THUMBSIZE 2 GPS 3 ]]

25P3H1V0.2 (click above to open LifeViewer)

But what did you request? Let's take a look at the options you 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 explicitely 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 TRACKLOOP 3 0 1/3 AUTOSTART THUMBLAUNCH THUMBSIZE 2 GPS 3 ]]

25P3H1V0.2 (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: 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.

Troubleshooting

to be written...

External links

• Logic Life Search on GitHub

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