## Logic Life Search

For scripts to aid with computation or simulation in cellular automata.

### 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.
Last edited by Macbi on January 30th, 2018, 4:51 pm, edited 1 time in total.

Macbi

Posts: 665
Joined: March 29th, 2009, 4:58 am

### 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 non-totalistic 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 not-P" can never be true, but the formula "(P or Q) and (R or not-P)" 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 NP-hard, 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:
0 0 0 0 0 00 a b c 0 00 d e f 0 00 g h i 0 00 0 0 0 0 00 0 0 0 0 00 0 0 0 0 00 * * * * 00 * * * * 00 * * * * 00 * * * * 00 0 0 0 0 00 0 0 0 0 00 * * * * 00 * * * * 00 * * * * 00 * * * * 00 0 0 0 0 00 0 0 0 0 00 * * * * 00 * * * * 00 * * * * 00 * * * * 00 0 0 0 0 00 0 0 0 0 00 0 0 0 0 00 0 a b c 00 0 d e f 00 0 g h i 00 0 0 0 0 0

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:
• *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

In the example above, the variables in the first generation are repeated in the last generation but shifted. Hence the search is for a pattern that shifts down and across by 1 after 4 generations: it will find the glider.

[Actually it won't. If you were to run the command "./lls exapmle-pattern" 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 exapmle-pattern -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
The last of these can be useful to search for a bit of a pattern inside a larger pattern. For example
0,  0,  0,  0,  0,  00, x0, x4, x5, x6,  00, x1, x7, x8, x9,  00, x2,x10,x11,x12,  00, x3,x13,x14,  1,  00,  0,  0,  0,  0,  1'0,  0,  0,  0,  0,  00, x0, x4, x5, x6,  00, x1, x7, x8, x9,  00, x2,x10,x11,x12,  00, x3,x13,x14,  1,  00,  0,  0,  0,  0,  1'

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:
• -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 "pB3a-c/S23" allows any of the transitions from Life, except that 3a must be present and 3c must not.

How to install

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 glucose-syrup 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 wherever-you-put-glucose/parallel/ and run the command "make". If everything works this should create a bunch of files including one called "glucose-syrup". 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
solver = "glucose-syrup"  # Default solver
in LLS_SAT_solvers.py to change the default. Thanks to Goldtiger997 for getting it to work.
Last edited by Macbi on January 29th, 2018, 8:58 pm, edited 3 times in total.

Macbi

Posts: 665
Joined: March 29th, 2009, 4:58 am

### 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 glucose-syrup 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 against-the-grain 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 sort-of 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 "sat-life", 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 hyper-naive 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"

Here are some possible future features. Please shout out if any of them would be particularly useful to you:

• 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 speed-up by trying this, but I need to leave it running for longer.
• Support for strobing rules and other "backgrounds"
• Non-isotropic 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.

Macbi

Posts: 665
Joined: March 29th, 2009, 4:58 am

### Re: Logic Life Search

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

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.

Assuming I can get everything working on Windows, I'll post any helpful details that I figure out.

dvgrn
Moderator

Posts: 5629
Joined: May 17th, 2009, 11:00 pm

### Re: Logic Life Search

After seeing you have submitted absolutely amazing results in the OCA spaceship thread, I'm guessing that LLS now handles non-totalistic 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.
SoL : FreeElectronics : DeadlyEnemies : 6a-ite : Rule X3VI
what is “sesame oil”?

Rhombic

Posts: 1056
Joined: June 1st, 2013, 5:41 pm

### Re: Logic Life Search

Can someone add the compiled glucose-syrup, mine won't compile with make, it gives errors:
\$ makecd syrup/parallel; make r; cp glucose-syrup_release ../../bin/glucose-syrupmake[1]: Entering directory '/Python/logic-life-search-master/solvers/syrup/syrup/parallel'Compiling: core/Solver.orIn file included from /Python/logic-life-search-master/solvers/syrup/syrup/utils/Options.h:30:0,                 from /Python/logic-life-search-master/solvers/syrup/syrup/core/Solver.h:55,                 from /Python/logic-life-search-master/solvers/syrup/syrup/parallel/../core/Solver.cc:54:/Python/logic-life-search-master/solvers/syrup/syrup/utils/ParseUtils.h: In function ‘double Glucose::parseDouble(B&)’:/Python/logic-life-search-master/solvers/syrup/syrup/utils/ParseUtils.h:99:5: warning: this ‘while’ clause does not guard... [-Wmisleading-indentation]     while (*in >= '0' && *in <= '9')     ^~~~~/Python/logic-life-search-master/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/logic-life-search-master/solvers/syrup/syrup/parallel/../core/Solver.cc  In member function ‘void Glucose::Solver::write_char(unsigned char)’:/Python/logic-life-search-master/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/logic-life-search-master/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/logic-life-search-master/solvers/syrup/syrup/parallel/../core/Solver.cc:774:49: warning: comparison between signed and unsigned integer expressions [-Wsign-compare]                 if(chanseokStrategy && nblevels <= coLBDBound) {                                        ~~~~~~~~~^~~~~~~~~~~~~/Python/logic-life-search-master/solvers/syrup/syrup/parallel/../core/Solver.cc  In member function ‘void Glucose::Solver::adaptSolver()’:/Python/logic-life-search-master/solvers/syrup/syrup/parallel/../core/Solver.cc:1416:24: warning: comparison between signed and unsigned integer expressions [-Wsign-compare]             if(c.lbd() <= coLBDBound) {                ~~~~~~~~^~~~~~~~~~~~~/Python/logic-life-search-master/solvers/syrup/syrup/parallel/../core/Solver.cc  In member function ‘Glucose::lbool Glucose::Solver::search(int)’:/Python/logic-life-search-master/solvers/syrup/syrup/parallel/../core/Solver.cc:1562:49: warning: comparison between signed and unsigned integer expressions [-Wsign-compare]                 if(chanseokStrategy && nblevels <= coLBDBound) {                                        ~~~~~~~~~^~~~~~~~~~~~~make[1]: *** [/Python/logic-life-search-master/solvers/syrup/syrup/parallel/../mtl/template.mk:71: /Python/logic-life-search-master/solvers/syrup/syrup/parallel/../core/Solver.or] Error 1make[1]: Leaving directory '/Python/logic-life-search-master/solvers/syrup/syrup/parallel'cp: cannot stat 'glucose-syrup_release': No such file or directorymake: *** [makefile:2: all] Error 1
Things to work on:
- Find a (7,1)c/8 ship in a Non-totalistic rule (someone please search the rules)
- Find a C/10 in JustFriends
- Find a C/10 in Day and Night
AforAmpere

Posts: 999
Joined: July 1st, 2016, 3:58 pm

### 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:
./lls -b 8 8 -p 3 -x 2 -y 1 -i --force_at_most 5 -r pB2ac/S -v 3

Pardon me if I'm overlooking something obvious.
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

A for awesome

Posts: 1808
Joined: September 13th, 2014, 5:36 pm
Location: 0x-1

### Re: Logic Life Search

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:
./lls -b 8 8 -p 3 -x 2 -y 1 -i --force_at_most 5 -r pB2ac/S -v 3

Pardon me if I'm overlooking something obvious.

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.

77topaz

Posts: 1345
Joined: January 12th, 2018, 9:19 pm

### Re: Logic Life Search

77topaz wrote:
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:
./lls -b 8 8 -p 3 -x 2 -y 1 -i --force_at_most 5 -r pB2ac/S -v 3

Pardon me if I'm overlooking something obvious.

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.

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

A for awesome

Posts: 1808
Joined: September 13th, 2014, 5:36 pm
Location: 0x-1

### Re: Logic Life Search

Has anyone compiled this for Cygwin or Windows? If so, can you upload the compiled glucose-sugar file?
Things to work on:
- Find a (7,1)c/8 ship in a Non-totalistic rule (someone please search the rules)
- Find a C/10 in JustFriends
- Find a C/10 in Day and Night
AforAmpere

Posts: 999
Joined: July 1st, 2016, 3:58 pm

### Re: Logic Life Search

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:
./lls -b 8 8 -p 3 -x 2 -y 1 -i --force_at_most 5 -r pB2ac/S -v 3

Pardon me if I'm overlooking something obvious.

Fairly certain "-r pB2ac/S" disallows everything that isn't B2, from looking at the descriptions.
LifeWiki: Like Wikipedia but with more spaceships. [citation needed]

Posts: 1875
Joined: November 8th, 2014, 8:48 pm
Location: Getting a snacker from R-Bee's

### 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 non-totalistic 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:
./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.
BlinkerSpawn wrote:Fairly certain "-r pB2ac/S" disallows everything that isn't B2, from looking at the descriptions.

Right, LLS not only supports nontotalistic rules, it can search through multiple rules at once. Sort of like a combination of WLS and rulesrc.

To just search in a single rule, for example B2e3aceij5-ijr/S23-a4, you just use the command
-r B2e3aceij5-ijr/S23-a4

To search in multiple rules, you put a "p" at the front of the rule to indicate that the rule is only being "partially" specified. After that:
• 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.
Also if you just write "p" then it allows all of the rules.

So for example the command "-r pB34a/S2-c3a-c" 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
-r pB1-c2345678/S012345678
Maybe the regulars in that thread know some other transitions that can be ruled out, perhaps just for some particular speeds.

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
--force_at_least 30 0 1 2

You can also use negative numbers to refer to generations from the last one backwards. So if you want to search for patterns that die out, use
--force_at_most 0 -1

Also worth mentioning that the bounding box created by "-b" has to contain the entire evolution of the pattern, not just the first generation. So to find the glider you would need "-b 4 4" rather than "-b 3 3" because the glider travels 1 cell during its period.

AforAmpere wrote:Has anyone compiled this for Cygwin or Windows? If so, can you upload the compiled glucose-sugar file?

I don't have a Windows computer at all, sorry.

Macbi

Posts: 665
Joined: March 29th, 2009, 4:58 am

### Re: Logic Life Search

Can't seem to compile syrup (from syrup.zip)
Making dependenciesDepends on: simpCompiling: /LLS/solvers/syrup/parallel/Main.or/LLS/solvers/syrup/parallel/Main.cc:53:18: fatal error: zlib.h: No such file or                                                                                             directory

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
/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)
SoL : FreeElectronics : DeadlyEnemies : 6a-ite : Rule X3VI
what is “sesame oil”?

Rhombic

Posts: 1056
Joined: June 1st, 2013, 5:41 pm

### Re: Logic Life Search

Rhombic wrote:Can't seem to compile syrup (from syrup.zip)

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.

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 "glucose-syrup", 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 "glucose-syrup"). 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.

Macbi

Posts: 665
Joined: March 29th, 2009, 4:58 am

### 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:
Traceback (most recent call last):  File "./lls", line 199, in <module>    indent = indent, verbosity = verbosity  File "/Python/logic-life-search-master/LLS.py", line 61, in preprocess_solve_and_postprocess    indent = indent, verbosity = verbosity  File "/Python/logic-life-search-master/LLS.py", line 175, in preprocess_and_solve    indent = indent, verbosity = verbosity)  File "/Python/logic-life-search-master/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/logic-life-search-master/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/logic-life-search-master/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_exceptionOSError: [Errno 8] Exec format error

I still can't get it to compile on Windows.
Things to work on:
- Find a (7,1)c/8 ship in a Non-totalistic rule (someone please search the rules)
- Find a C/10 in JustFriends
- Find a C/10 in Day and Night
AforAmpere

Posts: 999
Joined: July 1st, 2016, 3:58 pm

### Re: Logic Life Search

That error message is basically saying that python got to the point of trying to execute the solver (glucose-syrup?), 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 glucose-syrup 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 47,000 spaceships. Tabulated pages up to period 160 are available on the LifeWiki.
wildmyron

Posts: 1115
Joined: August 9th, 2013, 12:45 am

### 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?
Things to work on:
- Find a (7,1)c/8 ship in a Non-totalistic rule (someone please search the rules)
- Find a C/10 in JustFriends
- Find a C/10 in Day and Night
AforAmpere

Posts: 999
Joined: July 1st, 2016, 3:58 pm

### Re: Logic Life Search

Here's a just slightly more complex command line that returns a c/3 spaceship in under 10 seconds.

./lls -m -b 16 6 -p 3 -x 0 -y 1
rokicki

Posts: 48
Joined: August 6th, 2009, 12:26 pm

### Re: Logic Life Search

rokicki wrote:Here's a just slightly more complex command line that returns a c/3 spaceship in under 10 seconds.

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

I'm glad some people have got it working!

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.

Macbi

Posts: 665
Joined: March 29th, 2009, 4:58 am

### Re: Logic Life Search

Are you on Windows rokicki? How did you get it to work, if so?
Things to work on:
- Find a (7,1)c/8 ship in a Non-totalistic rule (someone please search the rules)
- Find a C/10 in JustFriends
- Find a C/10 in Day and Night
AforAmpere

Posts: 999
Joined: July 1st, 2016, 3:58 pm

### 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 mono-clinic!

calcyman

Posts: 2028
Joined: June 1st, 2009, 4:32 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.
Things to work on:
- Find a (7,1)c/8 ship in a Non-totalistic rule (someone please search the rules)
- Find a C/10 in JustFriends
- Find a C/10 in Day and Night
AforAmpere

Posts: 999
Joined: July 1st, 2016, 3:58 pm

### Re: Logic Life Search

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.

I fixed it. I think.

Macbi

Posts: 665
Joined: March 29th, 2009, 4:58 am

### Re: Logic Life Search

Macbi wrote:
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.

I fixed it. I think.

Thanks, it works now.
What do you do with ill crystallographers? Take them to the mono-clinic!

calcyman

Posts: 2028
Joined: June 1st, 2009, 4:32 pm

### 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 3-literal 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.

local g = golly()local FALSE = 1000000000local TRUE = -FALSElocal a = {}g.show("Getting pattern from Golly . . .")g.update()local r = g.getrect()local w = r[3] + 2local h = r[4] + 2local cells = g.getcells(r)local oncells = {}for ci=1,#cells,2 do   oncells[(cells[ci]-r[1]+1) .. " " .. (cells[ci+1]-r[2]+1)] = 1endg.show("Writing DIMACS-format 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 = 1local outputbase = 1 + w * hlocal nextvar = 1 + 2 * w * hfunction input(x, y)   if x < 0 or y < 0 or x >= w or y >= h then      return FALSE   else      return x + y * w + inputbase   endendfunction output(x, y)   if x < 0 or y < 0 or x >= w or y >= h then      return FALSE   else      return x + y * w + outputbase   endendfunction inputassum(x, y)   local t = input(x, y)   if t == FALSE then      return {FALSE, 0, 0}   else      return {t, 1, 1}   endendfunction 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]   endendfunction n(v)   return - vendfunction truity(v)   return v == TRUEendfunction notfalsity(v)   return v ~= FALSE and v ~= 0endfunction 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")   endendfunction 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 rendfunction sum(a, b)   return sum4(a, b, 0, 0)endlocal 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]endfunction 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]endfunction 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]endfunction 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, y-1)   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)endfor y=0, h-1 do   for x=0, w-1 do      calc(x, y)   endendfor x=0, w-3 do   emit(n(input(x, 0)), n(input(x+1, 0)), n(input(x+2, 0)))   emit(n(input(x, h-1)), n(input(x+1, h-1)), n(input(x+2, h-1)))endfor y=0, h-3 do   emit(n(input(0, y)), n(input(0, y+1)), n(input(0, y+2)))   emit(n(input(w-1, y)), n(input(w-1, y+1)), n(input(w-1, y+2)))endfor y=0, h-1 do   for x=0, w-1 do      if oncells[x .. " " .. y] then         F:write(" ", output(x, y), " 0\n")      else         F:write(" ", n(output(x, y)), " 0\n")      end   endendF: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 = falsefor 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, h-1 do         for x=0, w-1 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   endendif not sawresult then   g.show("No predecessor.")   g.update()else   g.setgen(-1+tonumber(g.getgen()))   g.show("Finished.")   g.update()end
rokicki

Posts: 48
Joined: August 6th, 2009, 12:26 pm

Next