## Logic Life Search

For scripts to aid with computation or simulation in cellular automata.
AforAmpere
Posts: 1049
Joined: July 1st, 2016, 3:58 pm

### Re: Logic Life Search

What system do you run? I am trying to find out if any Windows users have compiled glucose.
I and wildmyron manage the 5S project, which collects all known spaceship speeds in Isotropic Non-totalistic rules.

Things to work on:
- Find a (7,1)c/8 ship in a Non-totalistic rule
- Finish a rule with ships with period >= f_e_0(n) (in progress)

calcyman
Posts: 2096
Joined: June 1st, 2009, 4:32 pm

### Re: Logic Life Search

On Ubuntu, I can quickly find Brain using the --symmetry="D2|" flag:

Code: Select all

``````\$ python lls -m -b 17 12 --symmetry="D2|" -p 3 -x 0 -y 1 --parameters="-maxnbthreads=32"

Getting search pattern...
Done

Preprocessing...
Done

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

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

Solving...
Done

Time taken: 2.3035531044 seconds

x = 19, y = 14, rule = B3/S23
bbbbbbbbbbbbbbbbbbb\$
bbobbbbbbbbbbbbbobb\$
bbobbbbooboobbbbobb\$
bbboobbobbbobboobbb\$
bbbooobbobobbooobbb\$
bbbooboboboboboobbb\$
bbbbobobobobobobbbb\$
bbbbbbobobobobbbbbb\$
bbobooboobooboobobb\$
bobobobbbbbbbobobob\$
boboboobbbbboobobob\$
bbooobbbbbbbbbooobb\$
bbbbbbbbbbbbbbbbbbb\$
bbbbbbbbbbbbbbbbbbb!``````
On the other hand, a search for the symmetric c/4 orthogonal is taking hours.
What do you do with ill crystallographers? Take them to the mono-clinic!

Macbi
Posts: 699
Joined: March 29th, 2009, 4:58 am

### Re: Logic Life Search

rokicki wrote: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.
You can try it yourself by using the -M0 option. One test search you could try would be to rule out a knightship of whatever size you need to get a reasonable rumtime.

I technically don't have only 3-literal clauses, because I didn't do the thing Knuth does of breaking a 4-literal clause into two just for the sake of it. Surely if that helped then Glucose would do it automatically.
calcyman wrote:On the other hand, a search for the symmetric c/4 orthogonal is taking hours.
I don't really have any insight into why some searches go faster than others, other than low periods are much better than higher ones.

Also, I notice you're using loads of threads. At the current state of technology returns diminish quite quickly. So if you ever want to do lots of searches it will be faster to do them in parallel each with one core, than in series each with 32 cores.

On my own machine 8 threads doesn't seem much faster than one.

rokicki
Posts: 54
Joined: August 6th, 2009, 12:26 pm

### Re: Logic Life Search

Okay did some tests of knightship with different bounding box sizes, different
solvers, and -M0 and -M1.

Summary: sometimes minisat is faster, sometimes glucose. For a bounding
box of (20x6) glucose couldn't even prove it unsatisfiable, while minisat did
it in 29s (using -M1, the default). With -M0, the times were more consistent
between the two, but sometimes much faster, sometimes a bit slower.

All this really shows, at least for now, is that there's little hard-and-fast we
can say about the runtimes between these options. It's odd though that
glucose with 20/6 and -M1 just totally went bonkers, when minisat, or
either solver with -M0, had absolutely no trouble with 20/6.

Knight search: ./lls -i -p 6 -x 1 -y 2:
-M 1
6 6 minisat 6.4s (0.0s in solver)
6 6 glucose 6.4s (0.0s in solver)
6 15 minisat 45.2s (23.2s in solver)
6 15 glucose 66.8s (44.7s in solver)
20 6 minisat 29.0s (0.9s in solver)
20 6 glucose >420s (cancelled)
8 8 minisat 23.2s (7.8s in solver)
8 8 glucose 18.4s (3.7s in solver)
9 9 minisat 106.0s (85.9s in solver)
9 9 glucose 101.1s (39.5s in solver)

-M 0
6 6 minisat 7.2s (0.1s in solver)
6 6 glucose 7.5s (0.1s in solver)
6 15 minisat 25.9s (1.4s in solver)
6 15 glucose 26.1s (1.6s in solver)
20 6 minisat 31.7s (1.1s in solver)
20 6 glucose 33.5s (1.5s in solver)
8 8 minisat 22.8s (7.4s in solver)
8 8 glucose 20.4s (4.9s in solver)
9 9 minisat 160.4s (138.6s in solver)
9 9 glucose 65.3s (43.6 in solver)

I have more extensive results running; in these, glucose generally wins; it
is frequently slower than minisat, but at least for the things I've tried,
when it loses, it's closer than when minisat loses; all these results are with
-M0.

On the Briain search, -M0 beats -M1 handily.

Also, it would be nice to have an option to turn off the preprocessing; I
believe the SAT solvers do a much better job of this and do it more quickly.

Goldtiger997
Posts: 547
Joined: June 21st, 2016, 8:00 am
Location: 11.329903°N 142.199305°E

### Re: Logic Life Search

I am on Windows, using Cygwin. I have not been able to compile glucose-syrup after trying in many ways. So I tried using minisat, the alternative SAT solver that rokicki was comparing with glucose-syrup. I successfully turned it into an executable by downloading a pre-compiled binary from here and using these instructions.

The SAT solver itself worked, but then I got this error (running the example glider search):

Code: Select all

``````My-Username@My-IP ~
\$ cd logic-life-search

You-Will@Never-Know ~/logic-life-search
\$ ./lls test.txt -i

Getting search pattern...
Done

Preprocessing...
Done

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

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

Solving...
Traceback (most recent call last):
File "./lls", line 195, in <module>
indent = indent, verbosity = verbosity
File "/home/My-Username/logic-life-search/src/LLS.py", line 61, in preprocess_solve_and_postprocess
indent = indent, verbosity = verbosity
File "/home/My-Username/logic-life-search/src/LLS.py", line 175, in preprocess_and_solve
indent = indent, verbosity = verbosity)
File "/home/My-Username/logic-life-search/src/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 "/home/My-Username/logic-life-search/src/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 "/home/My-Username/logic-life-search/src/LLS_SAT_solvers.py", line 86, in use_solver
stdout=subprocess.PIPE, stdin=subprocess.PIPE, stderr=subprocess.PIPE)
File "/usr/lib/python2.7/subprocess.py", line 390, in __init__
File "/usr/lib/python2.7/subprocess.py", line 1025, in _execute_child
raise child_exception
OSError: [Errno 2] No such file or directory``````
Does anyone have any idea how to fix this?

P.S. Based on the results its found so far, the program seems really cool Macbi.

rokicki
Posts: 54
Joined: August 6th, 2009, 12:26 pm

### Re: Logic Life Search

Try -S yoursolvername

where your solvername is (for example) minisat.

The options are in LLS_SAT_solvers.py; you can add debugging prints to that
script if you need them to figure out what is going wrong. For instance, I

print "Executing command ", command

right before

solver_process = subprocess.Popen(

Make sure to match indentation exactly.

Goldtiger997
Posts: 547
Joined: June 21st, 2016, 8:00 am
Location: 11.329903°N 142.199305°E

### Re: Logic Life Search

Thanks rokicki, that seemed to work. However, now I get this message, which claims the glider does not exist:

Code: Select all

``````./lls -i test.txt

Getting search pattern...
Done

Preprocessing...
Done

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

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

Solving...
Done

Time taken: 0.0202569961548 seconds

Unsatisfiable``````
"Number of undetermined cells: 0" sounds quite suspicious.

Any ideas...

Macbi
Posts: 699
Joined: March 29th, 2009, 4:58 am

### Re: Logic Life Search

rokicki wrote:For a bounding
box of (20x6) glucose couldn't even prove it unsatisfiable, while minisat did
it in 29s (using -M1, the default).
I think you might have run into an error with glucose. Very occasionally, and only with easy problems, glucose will solve the problem and then continue to run. You'll be able to tell that this has happened because glucose won't be using as much CPU as it normally does. I'll send the glucose team an email about this.

On three successful runs I found that glucose averaged 1.334s and minisat 1.078s.

I've been trying to optimise LLS for the longest searches, the kind you might leave running overnight. So I haven't been counting the preprocessor time (since that will never be significant) and I've been running tests that take >1 minute. In this regard some of the results you've posted agree with me. The "-b 9 9" search was fastest with -M1 and glucose. But the "-b 6 15" search was faster with "-M0". It's mysterious.

I'll definitely add a command line option to stop preprocessing at some point. But for now you'll have to do it by editing the code. In LLS.py comment out the two lines that begin "search_pattern.optimise". Then add the line

Code: Select all

``clauses_copy = [[literal for literal in clause if literal != "0"] for clause in clauses_copy if "1" not in clause]``
to LLS_DIMACS.py just after the line "clauses_copy = copy.deepcopy(clauses)".

Macbi
Posts: 699
Joined: March 29th, 2009, 4:58 am

### Re: Logic Life Search

Goldtiger997 wrote:"Number of undetermined cells: 0" sounds quite suspicious.
That does sound quite suspicious. What's the contents of "test.txt"? Is it the example I gave above? Maybe I made a typo up there or something. You could try running "./lls -b 4 -i -p4 -x1 -y1" since that's a search for the glider that doesn't need a file. Also try running in -v3 mode to get a better idea of what LLS is doing.

EDIT: I tried the example I posted and it worked fine for me. It could also be a Windows problem, since Windows uses a different format for newlines in text files than Linux does. I thought I'd accounted for this, but maybe not.

Goldtiger997
Posts: 547
Joined: June 21st, 2016, 8:00 am
Location: 11.329903°N 142.199305°E

### Re: Logic Life Search

Macbi wrote:That does sound quite suspicious. What's the contents of "test.txt"? Is it the example I gave above? Maybe I made a typo up there or something. You could try running "./lls -b 4 -i -p4 -x1 -y1" since that's a search for the glider that doesn't need a file. Also try running in -v3 mode to get a better idea of what LLS is doing.

EDIT: I tried the example I posted and it worked fine for me. It could also be a Windows problem, since Windows uses a different format for newlines in text files than Linux does. I thought I'd accounted for this, but maybe not.
Thanks for your help Macbi. Yes you are right about the contents of "test.txt". Unfortunately, the other search for the glider didn't work either. Here is the output it generated with -v3:

Code: Select all

``````\$ ./lls -b 4 -i -p4 -x1 -y1 -v3

Getting search pattern...
Creating spaceship search pattern...
Pattern created:
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
0,*,*,*,*,0
0,*,*,*,*,0
0,*,*,*,*,0
0,0,0,0,0,0

Done

Standardising variable names...
Done

Done

Preprocessing...
Forcing pattern to move with speed (1, 1)c/4 ...
Done

Forcing at least one cell to be live in first generation...
Number of clauses used: 1
Done

Optimising search pattern...
Improving search pattern (Pass 1) ...
Improving grid...
Done

Improving clause list...
Tidying clauses...
Done

Removing duplicate clauses...
Done

Making deductions...
Done

Done

Done

Improving search pattern (Pass 2) ...
Improving grid...
Done

Improving clause list...
Tidying clauses...
Done

Removing duplicate clauses...
Done

Making deductions...
Done

Done

Done

Improving search pattern (Pass 3) ...
Improving grid...
Done

Done

Done

Enforcing evolution rule...
Method: 1
Number of clauses used: 14440
Done

Optimising search pattern...
Improving search pattern (Pass 1) ...
Improving clause list...
Tidying clauses...
Done

Removing duplicate clauses...
Done

Making deductions...
Done

Done

Done

Improving search pattern (Pass 2) ...
Improving clause list...
Tidying clauses...
Done

Removing duplicate clauses...
Done

Making deductions...
Done

Done

Done

Done

Search pattern optimised to:
Rule = B3/S23
0,   0,   0,   0,   0,   0
0,  c0,  c1,  c2,   0,   0
0,  c3,  c4,  c5,   0,   0
0,  c6,  c7,  c8,   0,   0
0,   0,   0,   0,   0,   0
0,   0,   0,   0,   0,   0

0',  0',  0,   0',  0',  0'
0', c9, c10, c11,   0',  0'
0, c12, c13, c14, c15,   0'
0',c16, c17, c18,   0',  0'
0',  0',c19,   0',  0',  0'
0',  0',  0',  0',  0',  0'

0',  0',  0,   0',  0',  0'
0',c20, c21, c22, c23,   0'
0, c24, c25, c26, c27,   0'
0',c28, c29, c30, c31,   0'
0',c32, c33, c34,   0',  0'
0',  0',  0',  0',  0',  0'

0',  0',  0,   0,   0',  0'
0',c35, c36, c37, c38,   0'
0, c39, c40, c41, c42,   0
0, c43, c44, c45, c46,   0'
0',c47, c48, c49, c50,   0'
0',  0',  0,   0',  0',  0'

0',  0',  0,   0,   0',  0'
0',  0,   0,   0,   0,   0'
0,   0,  c0,  c1,  c2,   0
0,   0,  c3,  c4,  c5,   0
0',  0,  c6,  c7,  c8,   0'
0',  0',  0,   0,   0',  0'

Converting to DIMACS format...
Subsituting in DIMACS variable names...
Done

Creating DIMACS string...
Done

Done

Done

Number of undetermined cells: 51
Number of variables: 51
Number of clauses: 3234

Active width: 4
Active height: 4
Active duration: 5

Solving...
Preparing SAT solver input...
Writing file "lls_dimacs.cnf" ...
Done

Done

Solving with "glucose-syrup" ... (Start time: Mon Jan 29 13:18:35 2018)
Done

Formatting SAT solver output...
SAT solver output:

Error (if any): ""
Time taken: 0.016294002533
Done

Removing DIMACS file...
Done

Done

Time taken: 0.016294002533 seconds

Unsatisfiable``````
I wonder if anyone else with windows/cygwin can reproduce the same results as me...

Macbi
Posts: 699
Joined: March 29th, 2009, 4:58 am

### Re: Logic Life Search

Didn't you say you were using minisat? But the command you mentioned doesn't have "-S minisat" and it says it's using glucose-syrup. (By the way the reason it's returning UNSAT is that it's not getting any output back from glucose-syrup. But it is apparently finding a glucose-syrup file.)

Maybe I have to add ".exe" to the possible solver names in the code? I'll try to get a Windows computer and play around with it.
Last edited by Macbi on January 29th, 2018, 3:12 pm, edited 1 time in total.

rokicki
Posts: 54
Joined: August 6th, 2009, 12:26 pm

### Re: Logic Life Search

Macbi wrote: I think you might have run into an error with glucose. Very occasionally, and only with easy problems, glucose will solve the problem and then continue to run. You'll be able to tell that this has happened because glucose won't be using as much CPU as it normally does. I'll send the glucose team an email about this.
Actually it did finish in about 9 minutes (I started it up again after I posted).

Thanks for the suggestions on modifications!

AforAmpere
Posts: 1049
Joined: July 1st, 2016, 3:58 pm

### Re: Logic Life Search

Goldtiger997 wrote: I wonder if anyone else with windows/cygwin can reproduce the same results as me...
Can you post the executable? That would help a lot, and I'll see if I get the same issue.
I and wildmyron manage the 5S project, which collects all known spaceship speeds in Isotropic Non-totalistic rules.

Things to work on:
- Find a (7,1)c/8 ship in a Non-totalistic rule
- Finish a rule with ships with period >= f_e_0(n) (in progress)

Goldtiger997
Posts: 547
Joined: June 21st, 2016, 8:00 am
Location: 11.329903°N 142.199305°E

### Re: Logic Life Search

Macbi wrote:Didn't you say you were using minisat? But the command you mentioned doesn't have "-S minisat" and it says it's using glucose-syrup. (By the way the reason it's returning UNSAT is that it's not getting any output back from glucose-syrup. But it is apparently finding a glucose-syrup file.)
I understand what was going wrong. Previously, by using "-S minisat", I got error, so I renamed minisat.exe to glucose-syrup.exe and the errors disappeared, But now looking at lines 75-80 of LLS_SAT_solvers.py, I see why it will not work with renaming:

Code: Select all

``````    if solver in ["minisat","MapleCOMSPS","MapleCOMSPS_LRB","riss"]:
command = [solver_path, file_name, "temp_SAT_solver_output"] + parameter_list
elif solver in ["lingeling","plingeling","treengeling"]:
command = [solver_path, file_name] + parameter_list
elif solver in ["glucose", "glucose-syrup"]:
command = [solver_path, file_name, "-model"] + parameter_list``````
However, by renaming it back to minisat, I get this new error, which involves temp_SAT_solver_output not being able to be found:

Code: Select all

``````Solving...
Traceback (most recent call last):
File "./lls", line 195, in <module>
indent = indent, verbosity = verbosity
File "/home/My Username/logic-life-search/src/LLS.py", line 61, in preprocess_solve_and_postprocess
indent = indent, verbosity = verbosity
File "/home/My Username/logic-life-search/src/LLS.py", line 175, in preprocess_and_solve
indent = indent, verbosity = verbosity)
File "/home/My Username/logic-life-search/src/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 "/home/My Username/logic-life-search/src/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 "/home/My Username/logic-life-search/src/LLS_SAT_solvers.py", line 115, in use_solver
solution = LLS_files.string_from_file("temp_SAT_solver_output", indent = indent + 1, verbosity = verbosity)
File "/home/My Username/logic-life-search/src/LLS_files.py", line 8, in string_from_file
with open(file_name, "r") as pattern_file:
IOError: [Errno 2] No such file or directory: 'temp_SAT_solver_output'``````
If no-one has any ideas, I might try lingeling.

Anyway, here you go AforAmpere:
minisat.zip

AforAmpere
Posts: 1049
Joined: July 1st, 2016, 3:58 pm

### Re: Logic Life Search

I got a weird effect, I managed to rename it so it would not give errors, like Goldtiger did, using the same .exe but when I do the same search rokicki did to find a C/3, it returns unsatisfiable:

Code: Select all

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

Getting search pattern...
Done

Preprocessing...
Done

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

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

Solving...
Done

Time taken: 0.0167660713196 seconds

Unsatisfiable
``````
Is this the same problem you had Goldtiger?
Last edited by AforAmpere on January 29th, 2018, 7:32 pm, edited 1 time in total.
I and wildmyron manage the 5S project, which collects all known spaceship speeds in Isotropic Non-totalistic rules.

Things to work on:
- Find a (7,1)c/8 ship in a Non-totalistic rule
- Finish a rule with ships with period >= f_e_0(n) (in progress)

Macbi
Posts: 699
Joined: March 29th, 2009, 4:58 am

### Re: Logic Life Search

Goldtiger997 wrote:I understand what was going wrong. Previously, by using "-S minisat", I got error, so I renamed minisat.exe to glucose-syrup.exe and the errors disappeared, But now looking at lines 75-80 of LLS_SAT_solvers.py, I see why it will not work with renaming:
Yes! Renaming the solver was a clever idea, but sadly they do input and output slightly differently so LLS has to treat them differently.
However, by renaming it back to minisat, I get this new error, which involves temp_SAT_solver_output not being able to be found:
Was a file called "temp_SAT_solver_output" actually created?

Also you could test if minisat is working by running LLS with the option "-save_dimacs test_dimacs.cnf" to produce a file "test_dimacs.cnf" of the kinds that SAT solvers operate on, and then running minisat directly on that file by running "./minisat[.exe?] test_dimacs.cnf test_output".

I'm thinking that the Windows version of minisat might be adding ".txt" to its output filenames, which is why LLS can't see them.

Macbi
Posts: 699
Joined: March 29th, 2009, 4:58 am

### Re: Logic Life Search

AforAmpere wrote:I got a weird effect, I managed to rename it so it would not give errors, like Goldtiger did, using the same .exe but when I do the same search rokicki did to find a C/3, it returns unsatisfiable
Renaming minisat to glucose-syrup totally won't work, they have different output formats.

AforAmpere
Posts: 1049
Joined: July 1st, 2016, 3:58 pm

### Re: Logic Life Search

If it is adding .txt to the file names, isn't there a fix for that that could be tried? What areas of code interpret the output?
I and wildmyron manage the 5S project, which collects all known spaceship speeds in Isotropic Non-totalistic rules.

Things to work on:
- Find a (7,1)c/8 ship in a Non-totalistic rule
- Finish a rule with ships with period >= f_e_0(n) (in progress)

Macbi
Posts: 699
Joined: March 29th, 2009, 4:58 am

### Re: Logic Life Search

AforAmpere wrote:If it is adding .txt to the file names, isn't there a fix for that that could be tried? What areas of code interpret the output?
You would just have to add ".txt" after the filename in the lines

Code: Select all

``solution = LLS_files.string_from_file("temp_SAT_solver_output", indent = indent + 1, verbosity = verbosity)``
and

Code: Select all

``os.remove("temp_SAT_solver_output")``
of LLS_SAT_solvers.py

AforAmpere
Posts: 1049
Joined: July 1st, 2016, 3:58 pm

### Re: Logic Life Search

It still could not find the file.
I and wildmyron manage the 5S project, which collects all known spaceship speeds in Isotropic Non-totalistic rules.

Things to work on:
- Find a (7,1)c/8 ship in a Non-totalistic rule
- Finish a rule with ships with period >= f_e_0(n) (in progress)

Macbi
Posts: 699
Joined: March 29th, 2009, 4:58 am

### Re: Logic Life Search

Did you try running minisat separately?

AforAmpere
Posts: 1049
Joined: July 1st, 2016, 3:58 pm

### Re: Logic Life Search

When I run it, it gives no output on the command line.
I and wildmyron manage the 5S project, which collects all known spaceship speeds in Isotropic Non-totalistic rules.

Things to work on:
- Find a (7,1)c/8 ship in a Non-totalistic rule
- Finish a rule with ships with period >= f_e_0(n) (in progress)

Macbi
Posts: 699
Joined: March 29th, 2009, 4:58 am

### Re: Logic Life Search

AforAmpere wrote:When I run it, it gives no output on the command line.
That makes it sound like minisat isn't working at all.

It's really super frustrating for me that the thing people are struggling with is the one thing that I can't help with. This seems like it's completely a problem with minisat and glucose. If anyone manages to get any SAT solver working on Windows I'll happily change the LLS code to accommodate it.

AforAmpere
Posts: 1049
Joined: July 1st, 2016, 3:58 pm

### Re: Logic Life Search

I am pretty sure minisat is not working on Windows with Cygwin. On the website for minisat, there is a precompiled binary for Windows and Cygwin, however, it may be possible that because the file downloads as a .14_cygwin file, because of the weird download format, that converting to a .exe causes an error. How did you download minisat Goldtiger?
I and wildmyron manage the 5S project, which collects all known spaceship speeds in Isotropic Non-totalistic rules.

Things to work on:
- Find a (7,1)c/8 ship in a Non-totalistic rule
- Finish a rule with ships with period >= f_e_0(n) (in progress)

Goldtiger997
Posts: 547
Joined: June 21st, 2016, 8:00 am
Location: 11.329903°N 142.199305°E

### Re: Logic Life Search

Success! I tried using lingeling and it worked! .

I cannot upload it here as the file size is too big, but I will explain how to compile it.
Download the first file here. Decompress it. Enter "./configure.sh". Enter "make". This should sucessfully compile lingeling (and also plingeling and treengeling), with several warnings.