## Logic Life Search

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

### Re: Logic Life Search

What system do you run? I am trying to find out if any Windows users have compiled glucose.
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: 1017
Joined: July 1st, 2016, 3:58 pm

### Re: Logic Life Search

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

`\$ python lls -m -b 17 12 --symmetry="D2|" -p 3 -x 0 -y 1 --parameters="-maxnbthreads=32"Getting search pattern...DonePreprocessing...DoneNumber of undetermined cells: 314Number of variables: 516Number of clauses: 43417Active width: 17Active height: 12Active duration: 4Solving...DoneTime taken: 2.3035531044 secondsx = 19, y = 14, rule = B3/S23bbbbbbbbbbbbbbbbbbb\$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!

calcyman

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

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

Macbi

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

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

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

### 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):

`My-Username@My-IP ~\$ cd logic-life-searchYou-Will@Never-Know ~/logic-life-search\$ ./lls test.txt -iGetting search pattern...DonePreprocessing...DoneNumber of undetermined cells: 0Number of variables: 0Number of clauses: 1Active width: 0Active height: 0Active duration: 0Solving...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__    errread, errwrite)  File "/usr/lib/python2.7/subprocess.py", line 1025, in _execute_child    raise child_exceptionOSError: [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.

Goldtiger997

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

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

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

### Re: Logic Life Search

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

`./lls -i test.txtGetting search pattern...DonePreprocessing...DoneNumber of undetermined cells: 0Number of variables: 0Number of clauses: 1Active width: 0Active height: 0Active duration: 0Solving...DoneTime taken: 0.0202569961548 secondsUnsatisfiable`

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

Any ideas...

Goldtiger997

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

### 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
`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: 680
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.

Macbi

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

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

`\$ ./lls -b 4 -i -p4 -x1 -y1 -v3Getting 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...    DoneDonePreprocessing...    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    DoneDoneNumber of undetermined cells: 51Number of variables: 51Number of clauses: 3234Active width: 4Active height: 4Active duration: 5Solving...    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...    DoneDoneTime taken: 0.016294002533 secondsUnsatisfiable`

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

Goldtiger997

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

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

Macbi

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

### 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!
rokicki

Posts: 48
Joined: August 6th, 2009, 12:26 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.
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: 1017
Joined: July 1st, 2016, 3:58 pm

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

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

`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

Goldtiger997

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

### 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:
`\$ ./lls -m -b 16 6 -p 3 -x 0 -y 1Getting search pattern...DonePreprocessing...DoneNumber of undetermined cells: 270Number of variables: 364Number of clauses: 34177Active width: 16Active height: 6Active duration: 4Solving...DoneTime taken: 0.0167660713196 secondsUnsatisfiable`

Is this the same problem you had Goldtiger?
Last edited by AforAmpere on January 29th, 2018, 7:32 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: 1017
Joined: July 1st, 2016, 3:58 pm

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

Macbi

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

### 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?
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: 1017
Joined: July 1st, 2016, 3:58 pm

### 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
`solution = LLS_files.string_from_file("temp_SAT_solver_output", indent = indent + 1, verbosity = verbosity)`
and
`os.remove("temp_SAT_solver_output")`
of LLS_SAT_solvers.py

Macbi

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

### Re: Logic Life Search

It still could not find the 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: 1017
Joined: July 1st, 2016, 3:58 pm

### Re: Logic Life Search

Did you try running minisat separately?

Macbi

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

### Re: Logic Life Search

When I run it, it gives no output on the command line.
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: 1017
Joined: July 1st, 2016, 3:58 pm

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

Macbi

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

### 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?
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: 1017
Joined: July 1st, 2016, 3:58 pm

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

I actually can't remember. I see if I can work out what I did. It is entirely possible that my weird way of downloading it was the problem. Anyway, we have lingeling now!

Goldtiger997

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

PreviousNext