Logic Life Search
Logic Life Search
Logic Life Search is available here. It's currently on Version 0.
There is a LifeWiki entry here and a tutorial here.
There is a LifeWiki entry here and a tutorial here.
Last edited by Macbi on January 30th, 2018, 4:51 pm, edited 1 time in total.
Re: Logic Life Search
Here's a program I've been working on for a while. It's a search program along the same lines as lifesrc, WLS and JLS, but it works via a SAT solver (hence "Logic"). LLS itself (but not the SAT solver) is written in Python 2.X, so it should work on all operating systems. It supports all isotropic nontotalistic rules. It's currently a bit slower than WLS, but it's also more flexible.
What is a SAT solver anyway?
The problem "SAT", short for "satisfiability", is to determine whether or not a given logical formula can be made true by setting its inputs appropriately (and if so to give the appropriate inputs). For example the formula "P and notP" can never be true, but the formula "(P or Q) and (R or notP)" sometimes is true, for example when Q is false, P is true, and R is true.
For long formulas it can be very difficult to tell if they're satisfiable or not, even for a computer. In fact SAT has been proven to be NPhard, and hence there are likely some SAT problems that humanity will never be able to solve.
However, there are computer programs called "SAT solvers" that can be used to find solutions to SAT problems. They exploit the fact that the kind of problems that humans want to solve often have structure that makes them easier to understand. So SAT solvers will get stuck if you give them randomly generated formulas, but they are often incredibly fast if you give them nonrandom formulas generated from some application you actually care about.
In fact modern SAT solvers are now so fast that they can often provide good solutions to things that initially seem to have nothing to do with SAT. If you can convert the problem into a logical formula then you can apply a SAT solver, and SAT solvers are so good that this is often faster than attacking the problem directly. For example SAT solvers have been used to solve, sudoku, tiling puzzles, and are used in industrial applications such as circuit design and AI.
LLS is a program to that converts Game of Life searches to SAT problems, applies a SAT solver, and then converts the solution back to an RLE.
How to use LLS
After installation (see below), LLS is used from the command line. First you must create a text file containing the details of the search you want to run. For example the following search could be used to find the glider:
You can see that there are five generations separated by blank lines, and each generation is a rectangle of cells of the same width and height.
The possible entries are:
[Actually it won't. If you were to run the command "./lls exapmlepattern" it would probably return an empty pattern as the answer. This is totally reasonable since the empty pattern is also a solution to the problem specified. LLS's behaviour can be modified by command line options. The option "i" (for "inhabited") forces the population to be at least 1. The command "./lls exapmlepattern i" will find the glider.]
There are two other things that can be put in search patterns:
would find a way to terminate a diagonal line in a still life.
LLS treats every cell outside the grid as though it were 0'. I think this is a departure from WLS (which maybe treats them as though they were *' ?).
Note that cells are allowed to be separated either by spaces or commas, and hence search patterns can be created and edited in a spreadsheet program like Excel or LibreOffice and then saved as csv files.
The only other things you need to know is what the options are for LLS searches and what they do. This can be read about in LLS's help text, but I'll list some of them here as an advertisement:
The following instructions are for Linux. Windows is probably similar except perhaps try "gmake" instead of "make", and "python lls" instead of "./lls" to run it.
Go to the link above, click "Clone or download" then "Download ZIP". Unzip to wherever you want on your computer. Then download the SAT solver glucosesyrup from their site or (slightly more recent?) the version from the 2017 SAT competition (syrup.zip). Again, unzip it and put it anywhere you want.
Then you have to compile Glucose. I'll assume you already have GCC or similar. Open a command line in the directory whereveryouputglucose/parallel/ and run the command "make". If everything works this should create a bunch of files including one called "glucosesyrup". This is the SAT solver. Move it over to wherever you put LLS, and put it in the directory named "solvers". Finally, you will probably need to change the permissions on the file lls to make it executable.
(EDIT FOR WINDOWS USERS) The only SAT solver we've been able to get working on Windows is lingeling. Download it from here. Decompress it. Then at a command line opened in the lingeling folder enter "./configure.sh". Then enter "make". This should compile the code and produce three SAT solvers, lingeling, plingeling and treengeling. Drag whichever one you want to use (I think plingeling is the fastest) to the "solvers" folder as above. Then when you run LLS use the option "S plingeling". Or you can edit the line in LLS_SAT_solvers.py to change the default. Thanks to Goldtiger997 for getting it to work.
What is a SAT solver anyway?
The problem "SAT", short for "satisfiability", is to determine whether or not a given logical formula can be made true by setting its inputs appropriately (and if so to give the appropriate inputs). For example the formula "P and notP" can never be true, but the formula "(P or Q) and (R or notP)" sometimes is true, for example when Q is false, P is true, and R is true.
For long formulas it can be very difficult to tell if they're satisfiable or not, even for a computer. In fact SAT has been proven to be NPhard, and hence there are likely some SAT problems that humanity will never be able to solve.
However, there are computer programs called "SAT solvers" that can be used to find solutions to SAT problems. They exploit the fact that the kind of problems that humans want to solve often have structure that makes them easier to understand. So SAT solvers will get stuck if you give them randomly generated formulas, but they are often incredibly fast if you give them nonrandom formulas generated from some application you actually care about.
In fact modern SAT solvers are now so fast that they can often provide good solutions to things that initially seem to have nothing to do with SAT. If you can convert the problem into a logical formula then you can apply a SAT solver, and SAT solvers are so good that this is often faster than attacking the problem directly. For example SAT solvers have been used to solve, sudoku, tiling puzzles, and are used in industrial applications such as circuit design and AI.
LLS is a program to that converts Game of Life searches to SAT problems, applies a SAT solver, and then converts the solution back to an RLE.
How to use LLS
After installation (see below), LLS is used from the command line. First you must create a text file containing the details of the search you want to run. For example the following search could be used to find the glider:
Code: Select all
0 0 0 0 0 0
0 a b c 0 0
0 d e f 0 0
0 g h i 0 0
0 0 0 0 0 0
0 0 0 0 0 0
0 0 0 0 0 0
0 * * * * 0
0 * * * * 0
0 * * * * 0
0 * * * * 0
0 0 0 0 0 0
0 0 0 0 0 0
0 * * * * 0
0 * * * * 0
0 * * * * 0
0 * * * * 0
0 0 0 0 0 0
0 0 0 0 0 0
0 * * * * 0
0 * * * * 0
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 0
0 0 d e f 0
0 0 g h i 0
0 0 0 0 0 0
The possible entries are:
 *s can be anything
 0s must be dead, 1s must be alive
 Anything else is a variable name. They can be alive or dead but every occurrence of the variable must be the same
[Actually it won't. If you were to run the command "./lls exapmlepattern" it would probably return an empty pattern as the answer. This is totally reasonable since the empty pattern is also a solution to the problem specified. LLS's behaviour can be modified by command line options. The option "i" (for "inhabited") forces the population to be at least 1. The command "./lls exapmlepattern i" will find the glider.]
There are two other things that can be put in search patterns:
 A cell starting with a "" will be the opposite of whatever it would otherwise have been
 A cell ending in "'" (an apostrophe) won't be forced to obey the usual cellular automaton rule
Code: Select all
0, 0, 0, 0, 0, 0
0, x0, x4, x5, x6, 0
0, x1, x7, x8, x9, 0
0, x2,x10,x11,x12, 0
0, x3,x13,x14, 1, 0
0, 0, 0, 0, 0, 1'
0, 0, 0, 0, 0, 0
0, x0, x4, x5, x6, 0
0, x1, x7, x8, x9, 0
0, x2,x10,x11,x12, 0
0, x3,x13,x14, 1, 0
0, 0, 0, 0, 0, 1'
LLS treats every cell outside the grid as though it were 0'. I think this is a departure from WLS (which maybe treats them as though they were *' ?).
Note that cells are allowed to be separated either by spaces or commas, and hence search patterns can be created and edited in a spreadsheet program like Excel or LibreOffice and then saved as csv files.
The only other things you need to know is what the options are for LLS searches and what they do. This can be read about in LLS's help text, but I'll list some of them here as an advertisement:
 s, or symmetry followed by one of C1, C2, C4, D2, D2, D2/, D2\, D4+, D4x or D8 forces the pattern to have the given symmetry. (Note that you may have to escape the  and \ characters)
 p or period followed by a number forces the pattern to oscillate at that period
 x and y specify a translation to be applied each period, so that spaceships can be found
 Instead of giving a search pattern in a file, b creates a blank search pattern, with specified dimensions. This can be used with p, x and y to quickly find spaceships.
 i forces there to be at least 1 cell, m forces there to be movement
 o saves the output to a given file
 force_at_least and force_at_most allow the population to be bounded
 r or rule allows a rule to be specified in the usual format (Life is set as the default). You can also specify only a partial rule, by prefixing the rule with a "p". This makes LLS simultaneously search for a rule and pattern that fit your requirements (useful for the 5S project). For example "pB3ac/S23" allows any of the transitions from Life, except that 3a must be present and 3c must not.
The following instructions are for Linux. Windows is probably similar except perhaps try "gmake" instead of "make", and "python lls" instead of "./lls" to run it.
Go to the link above, click "Clone or download" then "Download ZIP". Unzip to wherever you want on your computer. Then download the SAT solver glucosesyrup from their site or (slightly more recent?) the version from the 2017 SAT competition (syrup.zip). Again, unzip it and put it anywhere you want.
Then you have to compile Glucose. I'll assume you already have GCC or similar. Open a command line in the directory whereveryouputglucose/parallel/ and run the command "make". If everything works this should create a bunch of files including one called "glucosesyrup". This is the SAT solver. Move it over to wherever you put LLS, and put it in the directory named "solvers". Finally, you will probably need to change the permissions on the file lls to make it executable.
(EDIT FOR WINDOWS USERS) The only SAT solver we've been able to get working on Windows is lingeling. Download it from here. Decompress it. Then at a command line opened in the lingeling folder enter "./configure.sh". Then enter "make". This should compile the code and produce three SAT solvers, lingeling, plingeling and treengeling. Drag whichever one you want to use (I think plingeling is the fastest) to the "solvers" folder as above. Then when you run LLS use the option "S plingeling". Or you can edit the line
Code: Select all
solver = "glucosesyrup" # Default solver
Last edited by Macbi on January 29th, 2018, 8:58 pm, edited 3 times in total.
Re: Logic Life Search
Version 0 notes
 A big "Thank You!" to the Glucose team (for making Glucose and putting up with my annoying emails) the MiniSAT team (which Glucose is based on) and Donald Knuth (whose book "The Art of Computer Science, Volume 4, Fascicle 6" taught me everything about SAT, and has a whole section on applying SAT to the Game of Life. Its exercises found many bugs in my code).
 LLS isn't completely polished yet, but I decided to release it since it's already useful.
 Please contact me with any bugs, typos or suggestions, even if they're extremely trivial. In fact, especially if they're extremely trivial.
 Also ask me for help if you can't get it running. I expect Windows could be more difficult than I made it seem above.
 Code contributions are welcome, although I have nearly zero idea of how github is supposed to work
 I chose to write in Python since I thought that would be easy for people who were already used to Python scripting for Golly.
 I'm quite new to Python (and programming) so apologies if the code isn't very Pythonic (or good)
 LLS often spend quite a lot of time preprocessing before giving the problem to the SAT solver. It essentially makes every deduction that can be made "locally", just looking at one cell and its parents. This is kind of silly since many of the deductions it's making could probably be made much faster by the SAT solver. But I decided that it was worth it anyway because:
 The preprocessing never takes too long, so it isn't going to make a big proportional difference except for searches that are very quick anyway.
 It's worth spending a polynomial amount of effort even if there's a 1% chance that we spot something the SAT solver doesn't and save it an exponential amount of effort.
 If you use the "v3" command and watch the simplifications happen you can sometimes learn something interesting about the problem.
 It's just feels embarrassing to hand the SAT solver a problem with lots of trivial redundancies in its specification
 I don't really have access to a Windows machine, so it would be useful if someone could run some comparisons to WLS. I think LLS will come out slower because I already tried some comparisons to JLS and they seemed about the same. One problem for which LLS was faster was verifying there are no p19 oscillators in a given bounding box.
 As SAT solving technology improves LLS will get faster without me having to do any additional work. In particular if someone develops SAT solver software for GPUs, TPUs, distributed networks or quantum computers, LLS should plug straight into it.
 For very trivial problems glucosesyrup can sometimes give weird output which LLS incorrectly interprets as "UNSAT" when in fact the problem is "SAT". This should be fixed soon, and I've never had it happen on a problem where I didn't actually already know the answer.
 For small bounding boxes, LLS is really quick to prove that there are no 2c/4 againstthegrain agar crawlers in the zebra stripes pattern (in particular it rejects them much faster than 2c/3 crawlers of the same size, even though higher periods should be harder). This sortof suggests that there might be some easy proof that such crawlers don't exist.
 It would be good if I could bundle a copy of glucose's code with LLS, and create a makefile that puts everything in the right place. I'll probably need some help to get this to work on Windows.
 If you try to read the code you'll notice there aren't many comments, but I've tried to be good with variable names. Good luck.
 I've programmed in compatibility with many SAT solvers, but glucose is the default because it was the fastest in testing.
 I chose the name "Logic Life Search" rather than "SAT Life Search" because Knuth already has a program called "satlife", and because I might try to use an SMT solver in the future.
 I tried both the "naive" and "sophisticated" schemes that Knuth gives in TAOCP for encoding the Life transition in conjunctive normal form, and the naive one was fast. So that's the default. All other CA rules are encoded in the hypernaive scheme where each transition is encoded by 512 clauses, one for each arrangement of parents.
 I should probably tidy up the files into a directory with a name like "lib"
 The constraints on population currently aren't implemented very well, and should be able to run much faster (both in preprocessing and solving)
 I'd like to have a more unified way of handling symmetries, to make it easier to search for agars, wicks, etc.
 Knuth gives a way of speeding up searches by forcing the answers to come out in a canonical form. This should definitely be implemented before trying to find a p19 oscillator.
 All SAT solvers have many parameters that can be "tuned" to improve their speed on your particular problems. There's a magical program called SMAC that does this automatically. I've gotten a small speedup by trying this, but I need to leave it running for longer.
 Support for strobing rules and other "backgrounds"
 Nonisotropic rules? They would be easy to add, but does anyone actually care?
 Ability to load WLS and JLS save files?
Last edited by Macbi on January 26th, 2018, 5:59 pm, edited 1 time in total.
Re: Logic Life Search
This looks awesome! I've been in need of a little help getting started on applying SAT searches to Life, so this is just what the doctor ordered.Macbi wrote:Here's a program I've been working on for a while. It's a search program along the same lines as lifesrc, WLS and JLS, but it works via a SAT solver (hence "Logic").
Assuming I can get everything working on Windows, I'll post any helpful details that I figure out.
Re: Logic Life Search
After seeing you have submitted absolutely amazing results in the OCA spaceship thread, I'm guessing that LLS now handles nontotalistic rules too.
I would like to know how to specify the rule and/or other parameters for a search.
Thank you very much for the brilliant script.
I would like to know how to specify the rule and/or other parameters for a search.
Thank you very much for the brilliant script.

 Posts: 1078
 Joined: July 1st, 2016, 3:58 pm
Re: Logic Life Search
Can someone add the compiled glucosesyrup, mine won't compile with make, it gives errors:
Code: Select all
$ make
cd syrup/parallel; make r; cp glucosesyrup_release ../../bin/glucosesyrup
make[1]: Entering directory '/Python/logiclifesearchmaster/solvers/syrup/syrup/parallel'
Compiling: core/Solver.or
In file included from /Python/logiclifesearchmaster/solvers/syrup/syrup/utils/Options.h:30:0,
from /Python/logiclifesearchmaster/solvers/syrup/syrup/core/Solver.h:55,
from /Python/logiclifesearchmaster/solvers/syrup/syrup/parallel/../core/Solver.cc:54:
/Python/logiclifesearchmaster/solvers/syrup/syrup/utils/ParseUtils.h: In function ‘double Glucose::parseDouble(B&)’:
/Python/logiclifesearchmaster/solvers/syrup/syrup/utils/ParseUtils.h:99:5: warning: this ‘while’ clause does not guard... [Wmisleadingindentation]
while (*in >= '0' && *in <= '9')
^~~~~
/Python/logiclifesearchmaster/solvers/syrup/syrup/utils/ParseUtils.h:103:2: note: ...this statement, but the latter is misleadingly indented as if it is guarded by the ‘while’
if (*in != 'e') printf("PARSE ERROR! Unexpected char: %c\n", *in),exit(3);
^~
/Python/logiclifesearchmaster/solvers/syrup/syrup/parallel/../core/Solver.cc In member function ‘void Glucose::Solver::write_char(unsigned char)’:
/Python/logiclifesearchmaster/solvers/syrup/syrup/parallel/../core/Solver.cc:326:47: error: ‘putc_unlocked’ was not declared in this scope
if(putc_unlocked((int) ch, certifiedOutput) == EOF)
^
/Python/logiclifesearchmaster/solvers/syrup/syrup/parallel/../core/Solver.cc In member function ‘void Glucose::Solver::analyze(Glucose::CRef, Glucose::vec<Glucose::Lit>&, Glucose::vec<Glucose::Lit>&, int&, unsigned int&, unsigned int&)’:
/Python/logiclifesearchmaster/solvers/syrup/syrup/parallel/../core/Solver.cc:774:49: warning: comparison between signed and unsigned integer expressions [Wsigncompare]
if(chanseokStrategy && nblevels <= coLBDBound) {
~~~~~~~~~^~~~~~~~~~~~~
/Python/logiclifesearchmaster/solvers/syrup/syrup/parallel/../core/Solver.cc In member function ‘void Glucose::Solver::adaptSolver()’:
/Python/logiclifesearchmaster/solvers/syrup/syrup/parallel/../core/Solver.cc:1416:24: warning: comparison between signed and unsigned integer expressions [Wsigncompare]
if(c.lbd() <= coLBDBound) {
~~~~~~~~^~~~~~~~~~~~~
/Python/logiclifesearchmaster/solvers/syrup/syrup/parallel/../core/Solver.cc In member function ‘Glucose::lbool Glucose::Solver::search(int)’:
/Python/logiclifesearchmaster/solvers/syrup/syrup/parallel/../core/Solver.cc:1562:49: warning: comparison between signed and unsigned integer expressions [Wsigncompare]
if(chanseokStrategy && nblevels <= coLBDBound) {
~~~~~~~~~^~~~~~~~~~~~~
make[1]: *** [/Python/logiclifesearchmaster/solvers/syrup/syrup/parallel/../mtl/template.mk:71: /Python/logiclifesearchmaster/solvers/syrup/syrup/parallel/../core/Solver.or] Error 1
make[1]: Leaving directory '/Python/logiclifesearchmaster/solvers/syrup/syrup/parallel'
cp: cannot stat 'glucosesyrup_release': No such file or directory
make: *** [makefile:2: all] Error 1
I and wildmyron manage the 5S project, which collects all known spaceship speeds in Isotropic Nontotalistic rules.
Things to work on:
 Find a (7,1)c/8 ship in a Nontotalistic rule
 Finish a rule with ships with period >= f_e_0(n) (in progress)
Things to work on:
 Find a (7,1)c/8 ship in a Nontotalistic rule
 Finish a rule with ships with period >= f_e_0(n) (in progress)
 A for awesome
 Posts: 1950
 Joined: September 13th, 2014, 5:36 pm
 Location: 0x1
 Contact:
Re: Logic Life Search
Do you know why this search input is returning unsatisfiable? I'm attempting to rediscover the 2c/3 you posted on the 5S thread:
Pardon me if I'm overlooking something obvious.
EDIT: Found a workaround, never mind.
Code: Select all
./lls b 8 8 p 3 x 2 y 1 i force_at_most 5 r pB2ac/S v 3
EDIT: Found a workaround, never mind.
Last edited by A for awesome on January 26th, 2018, 7:55 pm, edited 1 time in total.
x₁=ηx
V ⃰_η=c²√(Λη)
K=(Λu²)/2
Pₐ=1−1/(∫^∞_t₀(p(t)ˡ⁽ᵗ⁾)dt)
$$x_1=\eta x$$
$$V^*_\eta=c^2\sqrt{\Lambda\eta}$$
$$K=\frac{\Lambda u^2}2$$
$$P_a=1\frac1{\int^\infty_{t_0}p(t)^{l(t)}dt}$$
http://conwaylife.com/wiki/A_for_all
Aidan F. Pierce
V ⃰_η=c²√(Λη)
K=(Λu²)/2
Pₐ=1−1/(∫^∞_t₀(p(t)ˡ⁽ᵗ⁾)dt)
$$x_1=\eta x$$
$$V^*_\eta=c^2\sqrt{\Lambda\eta}$$
$$K=\frac{\Lambda u^2}2$$
$$P_a=1\frac1{\int^\infty_{t_0}p(t)^{l(t)}dt}$$
http://conwaylife.com/wiki/A_for_all
Aidan F. Pierce
Re: Logic Life Search
It might be that the force_at_most parameter is clashing with the phases of the (2,1)c/3 ship that have more than 5 cells? I'm not completely sure if the force_at_most parameter is supposed to apply to all phases or just the first one, though.A for awesome wrote:Do you know why this search input is returning unsatisfiable? I'm attempting to rediscover the 2c/3 you posted on the 5S thread:Pardon me if I'm overlooking something obvious.Code: Select all
./lls b 8 8 p 3 x 2 y 1 i force_at_most 5 r pB2ac/S v 3
 A for awesome
 Posts: 1950
 Joined: September 13th, 2014, 5:36 pm
 Location: 0x1
 Contact:
Re: Logic Life Search
It seems to imply just the first one... I'm leaning more toward it being an issue with the rule constraint, as inputting the rule from @Macbi's post outputs the spaceship.77topaz wrote:It might be that the force_at_most parameter is clashing with the phases of the (2,1)c/3 ship that have more than 5 cells? I'm not completely sure if the force_at_most parameter is supposed to apply to all phases or just the first one, though.A for awesome wrote:Do you know why this search input is returning unsatisfiable? I'm attempting to rediscover the 2c/3 you posted on the 5S thread:Pardon me if I'm overlooking something obvious.Code: Select all
./lls b 8 8 p 3 x 2 y 1 i force_at_most 5 r pB2ac/S v 3
EDIT: Found a workaround, never mind.
x₁=ηx
V ⃰_η=c²√(Λη)
K=(Λu²)/2
Pₐ=1−1/(∫^∞_t₀(p(t)ˡ⁽ᵗ⁾)dt)
$$x_1=\eta x$$
$$V^*_\eta=c^2\sqrt{\Lambda\eta}$$
$$K=\frac{\Lambda u^2}2$$
$$P_a=1\frac1{\int^\infty_{t_0}p(t)^{l(t)}dt}$$
http://conwaylife.com/wiki/A_for_all
Aidan F. Pierce
V ⃰_η=c²√(Λη)
K=(Λu²)/2
Pₐ=1−1/(∫^∞_t₀(p(t)ˡ⁽ᵗ⁾)dt)
$$x_1=\eta x$$
$$V^*_\eta=c^2\sqrt{\Lambda\eta}$$
$$K=\frac{\Lambda u^2}2$$
$$P_a=1\frac1{\int^\infty_{t_0}p(t)^{l(t)}dt}$$
http://conwaylife.com/wiki/A_for_all
Aidan F. Pierce

 Posts: 1078
 Joined: July 1st, 2016, 3:58 pm
Re: Logic Life Search
Has anyone compiled this for Cygwin or Windows? If so, can you upload the compiled glucosesugar file?
I and wildmyron manage the 5S project, which collects all known spaceship speeds in Isotropic Nontotalistic rules.
Things to work on:
 Find a (7,1)c/8 ship in a Nontotalistic rule
 Finish a rule with ships with period >= f_e_0(n) (in progress)
Things to work on:
 Find a (7,1)c/8 ship in a Nontotalistic rule
 Finish a rule with ships with period >= f_e_0(n) (in progress)
 BlinkerSpawn
 Posts: 1940
 Joined: November 8th, 2014, 8:48 pm
 Location: Getting a snacker from RBee's
Re: Logic Life Search
Fairly certain "r pB2ac/S" disallows everything that isn't B2, from looking at the descriptions.A for awesome wrote:Do you know why this search input is returning unsatisfiable? I'm attempting to rediscover the 2c/3 you posted on the 5S thread:Pardon me if I'm overlooking something obvious.Code: Select all
./lls b 8 8 p 3 x 2 y 1 i force_at_most 5 r pB2ac/S v 3
Re: Logic Life Search
Rhombic wrote:After seeing you have submitted absolutely amazing results in the OCA spaceship thread, I'm guessing that LLS now handles nontotalistic rules too.
A for awesome wrote:Do you know why this search input is returning unsatisfiable? I'm attempting to rediscover the 2c/3 you posted on the 5S thread:Code: Select all
./lls b 8 8 p 3 x 2 y 1 i force_at_most 5 r pB2ac/S v 3
77topaz wrote:It might be that the force_at_most parameter is clashing with the phases of the (2,1)c/3 ship that have more than 5 cells? I'm not completely sure if the force_at_most parameter is supposed to apply to all phases or just the first one, though.
Right, LLS not only supports nontotalistic rules, it can search through multiple rules at once. Sort of like a combination of WLS and rulesrc.BlinkerSpawn wrote:Fairly certain "r pB2ac/S" disallows everything that isn't B2, from looking at the descriptions.
To just search in a single rule, for example B2e3aceij5ijr/S23a4, you just use the command
Code: Select all
r B2e3aceij5ijr/S23a4
 If a number isn't present then none of those transitions are allowed.
 If a number is present without any letters after it then all of its transitions are allowed.
 If a number is present with some letters after it, followed by a minus sign, followed by some more letters, then the letters in the first group must be in the rule, the letters in the second group can't be in the rule, and any letters not mentioned can be in the rule or not.
So for example the command "r pB34a/S2c3ac" would search for rules in which any B3 transitions were allowed to be present or not, any B4 were allowed to be present or not except B4a has to be, any S2 transitions would be allowed or not except S2c can't be used, and all S3 transitions can be used or not except S3a must be present and S3c can't be. No other transitions would be allowed.
If anyone has suggestions for a better notation then I would love to hear them, but I think this one is fairly logical.
When I was looking for ships for the 5S project I knew that B0 wasn't allowed and I could see that 1c would explode any ships. But for all I knew the rest of the transitions could be useful. So I used
Code: Select all
r pB1c2345678/S012345678
The options "force_at_most" and "force_at_least" apply by default only to the first generation. But you can change which generations they apply to by writing a list of generations after them. They then apply to the total number of cells in all those generations. The generations are numbered from 0. So for example if you were searching for period 3 oscillators, and you wanted the average population to be at least 10, then you would use
Code: Select all
force_at_least 30 0 1 2
Code: Select all
force_at_most 0 1
I don't have a Windows computer at all, sorry.AforAmpere wrote:Has anyone compiled this for Cygwin or Windows? If so, can you upload the compiled glucosesugar file?
Re: Logic Life Search
Can't seem to compile syrup (from syrup.zip)
The thing is, in parallel, I have no zlib.h
EDIT: copied it and set the path to parallel/zlib.h, same with zconf.h... however, there is a further issue
Code: Select all
Making dependencies
Depends on: simp
Compiling: /LLS/solvers/syrup/parallel/Main.or
/LLS/solvers/syrup/parallel/Main.cc:53:18: fatal error: zlib.h: No such file or directory
EDIT: copied it and set the path to parallel/zlib.h, same with zconf.h... however, there is a further issue
Code: Select all
/LLS/solvers/syrup/parallel/../core/Solver.cc:326:47: error: ‘putc_unlocked’ was not declared in this scope
if(putc_unlocked((int) ch, certifiedOutput) == EOF)
Re: Logic Life Search
What operating system are you on? dvgrn said he was going to try getting it to work on Windows, so he might have a working copy soon.Rhombic wrote:Can't seem to compile syrup (from syrup.zip)
Also it looks like you downloaded the copy from the SAT competition. The one from their website is more "official" so it might work better. You could also try using the "simp" or "core" versions instead of "parallel", since "parallel" isn't much faster anyway. I think these produce a file called "glucose" rather than "glucosesyrup", so you would have to run LLS with the option "S glucose" to make it use that instead of the default (or you could just rename the solver to "glucosesyrup"). You could also try getting a completely different SAT solver, such as minisat.
I'm afraid I can't really help you with the particular error, since I don't know anything about makefiles or C++ (is that even what this is?).
Anyway this is really a Glucose problem rather than a LLS one. So if you're really stuck you could email the Glucose guys. Or just ask on some generic programming forum.

 Posts: 1078
 Joined: July 1st, 2016, 3:58 pm
Re: Logic Life Search
I don't know what this error message is prompting me to do, I tried running LLS with A for Awesome's file from a different OS and:
I still can't get it to compile on Windows.
Code: Select all
Traceback (most recent call last):
File "./lls", line 199, in <module>
indent = indent, verbosity = verbosity
File "/Python/logiclifesearchmaster/LLS.py", line 61, in preprocess_solve_and_postprocess
indent = indent, verbosity = verbosity
File "/Python/logiclifesearchmaster/LLS.py", line 175, in preprocess_and_solve
indent = indent, verbosity = verbosity)
File "/Python/logiclifesearchmaster/LLS.py", line 246, in solve
DIMACS_string, solver=solver, parameters=parameters, timeout=timeout, save_dimacs = save_dimacs, dry_run = dry_run, indent = indent + 1, verbosity = verbosity)
File "/Python/logiclifesearchmaster/LLS_SAT_solvers.py", line 48, in SAT_solve
solution, time_taken = use_solver(solver, dimacs_file, parameters = parameters, timeout = timeout, indent = indent, verbosity = verbosity)
File "/Python/logiclifesearchmaster/LLS_SAT_solvers.py", line 84, in use_solver
stdout=subprocess.PIPE, stdin=subprocess.PIPE, stderr=subprocess.PIPE)
File "/usr/lib/python2.7/subprocess.py", line 390, in __init__
errread, errwrite)
File "/usr/lib/python2.7/subprocess.py", line 1025, in _execute_child
raise child_exception
OSError: [Errno 8] Exec format error
I and wildmyron manage the 5S project, which collects all known spaceship speeds in Isotropic Nontotalistic rules.
Things to work on:
 Find a (7,1)c/8 ship in a Nontotalistic rule
 Finish a rule with ships with period >= f_e_0(n) (in progress)
Things to work on:
 Find a (7,1)c/8 ship in a Nontotalistic rule
 Finish a rule with ships with period >= f_e_0(n) (in progress)
Re: Logic Life Search
That error message is basically saying that python got to the point of trying to execute the solver (glucosesyrup?), but the file wasn't executable. Was it compiled with cygwin? Are you trying to run it from a cygwin shell? If yes to both, which versions of cygwin in both cases?
Edit: just saw A for Awesome's on a Mac. You can't run that compiled version of glucosesyrup on windows, even with cygwin.
Edit: just saw A for Awesome's on a Mac. You can't run that compiled version of glucosesyrup on windows, even with cygwin.
Last edited by wildmyron on January 27th, 2018, 10:59 pm, edited 1 time in total.
The latest version of the 5S Project contains over 226,000 spaceships. There is also a GitHub mirror of the collection. Tabulated pages up to period 160 (out of date) are available on the LifeWiki.

 Posts: 1078
 Joined: July 1st, 2016, 3:58 pm
Re: Logic Life Search
I am trying to run it from a Cygwin64 terminal, and A for Awesome's file is most likely not designed to be put into Cygwin.
EDIT, yeah, but I also can't seem to compile glucose anyway. I figured I'd try getting that to work, but it does not. What system do you run, and have you had any luck?
EDIT, yeah, but I also can't seem to compile glucose anyway. I figured I'd try getting that to work, but it does not. What system do you run, and have you had any luck?
I and wildmyron manage the 5S project, which collects all known spaceship speeds in Isotropic Nontotalistic rules.
Things to work on:
 Find a (7,1)c/8 ship in a Nontotalistic rule
 Finish a rule with ships with period >= f_e_0(n) (in progress)
Things to work on:
 Find a (7,1)c/8 ship in a Nontotalistic rule
 Finish a rule with ships with period >= f_e_0(n) (in progress)
Re: Logic Life Search
Here's a just slightly more complex command line that returns a c/3 spaceship in under 10 seconds.
Code: Select all
./lls m b 16 6 p 3 x 0 y 1
Re: Logic Life Search
I'm glad some people have got it working!rokicki wrote:Here's a just slightly more complex command line that returns a c/3 spaceship in under 10 seconds.
Code: Select all
./lls m b 16 6 p 3 x 0 y 1
I've found that i (at least one cell in first generation) is slightly faster than m (at least one change between first two generations) when looking for spaceships.

 Posts: 1078
 Joined: July 1st, 2016, 3:58 pm
Re: Logic Life Search
Are you on Windows rokicki? How did you get it to work, if so?
I and wildmyron manage the 5S project, which collects all known spaceship speeds in Isotropic Nontotalistic rules.
Things to work on:
 Find a (7,1)c/8 ship in a Nontotalistic rule
 Finish a rule with ships with period >= f_e_0(n) (in progress)
Things to work on:
 Find a (7,1)c/8 ship in a Nontotalistic rule
 Finish a rule with ships with period >= f_e_0(n) (in progress)
Re: Logic Life Search
You'll need to run git checkout cad98 since the latest version of the repo is missing all of the code which should be in src.
What do you do with ill crystallographers? Take them to the monoclinic!

 Posts: 1078
 Joined: July 1st, 2016, 3:58 pm
Re: Logic Life Search
EDIT, never mind. Has anyone compiled it with Cygwin yet? Nobody has actually said what operating system they are running.
Last edited by AforAmpere on January 28th, 2018, 4:29 pm, edited 1 time in total.
I and wildmyron manage the 5S project, which collects all known spaceship speeds in Isotropic Nontotalistic rules.
Things to work on:
 Find a (7,1)c/8 ship in a Nontotalistic rule
 Finish a rule with ships with period >= f_e_0(n) (in progress)
Things to work on:
 Find a (7,1)c/8 ship in a Nontotalistic rule
 Finish a rule with ships with period >= f_e_0(n) (in progress)
Re: Logic Life Search
I fixed it. I think.calcyman wrote:You'll need to run git checkout cad98 since the latest version of the repo is missing all of the code which should be in src.
Re: Logic Life Search
Thanks, it works now.Macbi wrote:I fixed it. I think.calcyman wrote:You'll need to run git checkout cad98 since the latest version of the repo is missing all of the code which should be in src.
What do you do with ill crystallographers? Take them to the monoclinic!
Re: Logic Life Search
I've been doing some experiments myself with similar things; this Lua script will run a pattern backwards one step in Golly if you have glucose installed (you have to adjust the glucose path towards the end of the lua script for now).
This is my first script ever in Lua so be gentle.
In my experiments the "Knuthian" encoding (using only 3literal clauses) has always been more efficient than the naive encoding, whether using minisat or glucose. I'd love to hear the examples that lead the original author to
decide the other direction.
Glucose does tend to be faster than minisat and minisat is a pain to compile.
This is my first script ever in Lua so be gentle.
In my experiments the "Knuthian" encoding (using only 3literal clauses) has always been more efficient than the naive encoding, whether using minisat or glucose. I'd love to hear the examples that lead the original author to
decide the other direction.
Glucose does tend to be faster than minisat and minisat is a pain to compile.
Code: Select all
local g = golly()
local FALSE = 1000000000
local TRUE = FALSE
local a = {}
g.show("Getting pattern from Golly . . .")
g.update()
local r = g.getrect()
local w = r[3] + 2
local h = r[4] + 2
local cells = g.getcells(r)
local oncells = {}
for ci=1,#cells,2 do
oncells[(cells[ci]r[1]+1) .. " " .. (cells[ci+1]r[2]+1)] = 1
end
g.show("Writing DIMACSformat CNF file . . .")
g.update()
local F = assert(io.open("t.cnf", "w"), "Can't write to t.cnf")
F:write("p cnf 1 1\n")
local inputbase = 1
local outputbase = 1 + w * h
local nextvar = 1 + 2 * w * h
function input(x, y)
if x < 0 or y < 0 or x >= w or y >= h then
return FALSE
else
return x + y * w + inputbase
end
end
function output(x, y)
if x < 0 or y < 0 or x >= w or y >= h then
return FALSE
else
return x + y * w + outputbase
end
end
function inputassum(x, y)
local t = input(x, y)
if t == FALSE then
return {FALSE, 0, 0}
else
return {t, 1, 1}
end
end
function getoff(a, v)
if v == 0 or v < a[2] then
return TRUE
elseif v > a[3] then
return FALSE
else
return a[1] + v  a[2]
end
end
function n(v)
return  v
end
function truity(v)
return v == TRUE
end
function notfalsity(v)
return v ~= FALSE and v ~= 0
end
function emit(a, b, c)
if not truity(a) and not truity(b) and not truity(c) then
if notfalsity(a) then F:write(" ", a) end
if notfalsity(b) then F:write(" ", b) end
if notfalsity(c) then F:write(" ", c) end
F:write(" 0\n")
end
end
function sum4(a, b, min, max)
if b[1] == FALSE then return a end
if a[1] == FALSE then return b end
if min == 0 then min = 1 end
if max == 0 then max = a[3] + b[3] end
local base = nextvar
nextvar = nextvar + max  min + 1
local r = {base, min, max}
for av=0, a[3] do
for bv=0, b[3] do
local s = av + bv
if s >= min and s <= max then
emit(n(getoff(a, av)), n(getoff(b, bv)), getoff(r, s))
end
end
end
for av=1, 1+a[3] do
for bv=1, 1+b[3] do
local s = av + bv  1
if s >= min and s <= max then
emit(getoff(a, av), getoff(b, bv), n(getoff(r, s)))
end
end
end
return r
end
function sum(a, b)
return sum4(a, b, 0, 0)
end
local cache = {}
function getv2(x, y)
local key = "v2 " .. x .. " " .. y
if cache[key] == nil then
cache[key] = sum(inputassum(x, y), inputassum(x, y+1))
end
return cache[key]
end
function geth2(x, y)
local key = "h2 " .. x .. " " .. y
if cache[key] == nil then
cache[key] = sum(inputassum(x, y), inputassum(x+1, y))
end
return cache[key]
end
function geth4(x, y)
local key = "h4 " .. x .. " " .. y
if cache[key] == nil then
cache[key] = sum(geth2(x, y), geth2(x, y+2))
end
return cache[key]
end
function calc(x, y)
local z0 = input(x, y)
local z1 = output(x, y)
local xd = x  x % 2
local yd = y  y % 2
local xo = 3 * x  2 * xd  1
local yo = 3 * y  2 * yd  1
local xm = 2 * x  xo
local h4 = geth4(xd, y1)
local v2 = getv2(xo, yd)
local s = sum4(h4, sum(v2, sum(inputassum(xm, y), inputassum(xo, yo))), 2, 4)
emit(n(getoff(s, 4)), 0, n(z1))
emit(getoff(s, 2), 0, n(z1))
emit(getoff(s, 3), z0, n(z1))
emit(n(getoff(s, 3)), getoff(s, 4), z1)
local xx = nextvar
nextvar = nextvar + 1
emit(n(getoff(s, 2)), getoff(s, 4), xx)
emit(n(xx), n(z0), z1)
end
for y=0, h1 do
for x=0, w1 do
calc(x, y)
end
end
for x=0, w3 do
emit(n(input(x, 0)), n(input(x+1, 0)), n(input(x+2, 0)))
emit(n(input(x, h1)), n(input(x+1, h1)), n(input(x+2, h1)))
end
for y=0, h3 do
emit(n(input(0, y)), n(input(0, y+1)), n(input(0, y+2)))
emit(n(input(w1, y)), n(input(w1, y+1)), n(input(w1, y+2)))
end
for y=0, h1 do
for x=0, w1 do
if oncells[x .. " " .. y] then
F:write(" ", output(x, y), " 0\n")
else
F:write(" ", n(output(x, y)), " 0\n")
end
end
end
F:close()
g.show("Running glucose . . .")
g.update()
os.execute("./glucose t.cnf t.res")
F = assert(io.open("t.res", "r"), "Can't read t.res")
local sawresult = false
for line in F:lines() do
if string.sub(line, 1, 3) ~= "UNS" then
g.show("Sending result back to Golly . . .")
g.update()
local toks = {}
for tok in line:gmatch("[^%s]+") do
table.insert(toks, tok)
end
for y=0, h1 do
for x=0, w1 do
if (tonumber(toks[input(x, y)]) < 0) then
g.setcell(x+r[1]1, y+r[2]1, 0)
else
g.setcell(x+r[1]1, y+r[2]1, 1)
end
end
end
sawresult = true
end
end
if not sawresult then
g.show("No predecessor.")
g.update()
else
g.setgen(1+tonumber(g.getgen()))
g.show("Finished.")
g.update()
end