Logic Life Search

Macbi · Post by **Macbi** » January 26th, 2018, 1:41 pm

Logic Life Search is available here.

There is a LifeWiki entry here and a tutorial here.

Macbi · Post by **Macbi** » January 26th, 2018, 1:42 pm

EDIT: These notes apply to LLS version 0. The most recent release is here: https://gitlab.com/OscarCunningham/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:

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

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

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'

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

Code: Select all

solver = "glucose-syrup"  # Default solver

in LLS_SAT_solvers.py to change the default. Thanks to Goldtiger997 for getting it to work.

Macbi · Post by **Macbi** » January 26th, 2018, 1:42 pm

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?

Post by **dvgrn** » January 26th, 2018, 3:29 pm

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.

Rhombic · Post by **Rhombic** » January 26th, 2018, 6:39 pm

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.

AforAmpere · Post by **AforAmpere** » January 26th, 2018, 6:57 pm

Can someone add the compiled glucose-syrup, mine won't compile with make, it gives errors:

Code: Select all

$ make
cd syrup/parallel; make r; cp glucose-syrup_release ../../bin/glucose-syrup
make[1]: Entering directory '/Python/logic-life-search-master/solvers/syrup/syrup/parallel'
Compiling: core/Solver.or
In 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 1
make[1]: Leaving directory '/Python/logic-life-search-master/solvers/syrup/syrup/parallel'
cp: cannot stat 'glucose-syrup_release': No such file or directory
make: *** [makefile:2: all] Error 1

praosylen · Post by **praosylen** » January 26th, 2018, 7:31 pm

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

Pardon me if I'm overlooking something obvious.
EDIT: Found a workaround, never mind.

77topaz · Post by **77topaz** » January 26th, 2018, 7:45 pm

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

praosylen · Post by **praosylen** » January 26th, 2018, 7:53 pm

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:
Code: Select all
./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.

AforAmpere · Post by **AforAmpere** » January 26th, 2018, 9:08 pm

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

BlinkerSpawn · Post by **BlinkerSpawn** » January 26th, 2018, 9:32 pm

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

Fairly certain "-r pB2ac/S" disallows everything that isn't B2, from looking at the descriptions.

Macbi · Post by **Macbi** » January 27th, 2018, 4:45 am

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

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

Code: Select all

-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

Code: Select all

-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

Code: Select all

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

Code: Select all

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

Rhombic · Post by **Rhombic** » January 27th, 2018, 9:26 am

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

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

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

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

Macbi · Post by **Macbi** » January 27th, 2018, 11:51 am

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.

AforAmpere · Post by **AforAmpere** » January 27th, 2018, 9:55 pm

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:

Code: Select all

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_exception
OSError: [Errno 8] Exec format error

I still can't get it to compile on Windows.

wildmyron · Post by **wildmyron** » January 27th, 2018, 10:46 pm

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.

AforAmpere · Post by **AforAmpere** » January 27th, 2018, 10:58 pm

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?

rokicki · Post by **rokicki** » January 28th, 2018, 3:46 pm

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

Macbi · Post by **Macbi** » January 28th, 2018, 3:55 pm

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

AforAmpere · Post by **AforAmpere** » January 28th, 2018, 3:58 pm

Are you on Windows rokicki? How did you get it to work, if so?

calcyman · Post by **calcyman** » January 28th, 2018, 4:06 pm

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.

AforAmpere · Post by **AforAmpere** » January 28th, 2018, 4:13 pm

EDIT, never mind. Has anyone compiled it with Cygwin yet? Nobody has actually said what operating system they are running.

Macbi · Post by **Macbi** » January 28th, 2018, 4:26 pm

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.

calcyman · Post by **calcyman** » January 28th, 2018, 4:29 pm

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.

rokicki · Post by **rokicki** » January 28th, 2018, 5:01 pm

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.

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 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 = 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, 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)
end
for y=0, h-1 do
   for x=0, w-1 do
      calc(x, y)
   end
end
for 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)))
end
for 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)))
end
for 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
   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, 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
   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

ConwayLife.com

Logic Life Search

Logic Life Search

Re: Logic Life Search

Re: Logic Life Search

Re: Logic Life Search

Re: Logic Life Search

Re: Logic Life Search

Re: Logic Life Search

Re: Logic Life Search

Re: Logic Life Search

Re: Logic Life Search

Re: Logic Life Search

Re: Logic Life Search

Re: Logic Life Search

Re: Logic Life Search

Re: Logic Life Search

Re: Logic Life Search

Re: Logic Life Search

Re: Logic Life Search

Re: Logic Life Search

Re: Logic Life Search

Re: Logic Life Search

Re: Logic Life Search

Re: Logic Life Search

Re: Logic Life Search

Re: Logic Life Search