ConwayLife.com

Posted: **January 28th, 2018, 5:40 pm**

What system do you run? I am trying to find out if any Windows users have compiled glucose.

Posted: **January 28th, 2018, 6:15 pm**

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

Posted: **January 28th, 2018, 6:38 pm**

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.

Posted: **January 28th, 2018, 9:53 pm**

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.

Posted: **January 29th, 2018, 2:17 am**

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__
    errread, errwrite)
  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.

Posted: **January 29th, 2018, 2:27 am**

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

print "Executing command ", command

right before

solver_process = subprocess.Popen(

Make sure to match indentation exactly.

Posted: **January 29th, 2018, 3:02 am**

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

Posted: **January 29th, 2018, 8:32 am**

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

Posted: **January 29th, 2018, 8:37 am**

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.

Posted: **January 29th, 2018, 9:23 am**

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

Posted: **January 29th, 2018, 9:45 am**

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.

Posted: **January 29th, 2018, 12:35 pm**

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!

Posted: **January 29th, 2018, 5:36 pm**

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.

Posted: **January 29th, 2018, 7:03 pm**

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: (70.19 KiB) Downloaded 271 times

Posted: **January 29th, 2018, 7:29 pm**

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?

Posted: **January 29th, 2018, 7:31 pm**

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.

Posted: **January 29th, 2018, 7:32 pm**

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.

Posted: **January 29th, 2018, 7:35 pm**

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?

Posted: **January 29th, 2018, 7:50 pm**

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

Posted: **January 29th, 2018, 7:54 pm**

It still could not find the file.

Posted: **January 29th, 2018, 7:58 pm**

Did you try running minisat separately?

Posted: **January 29th, 2018, 8:07 pm**

When I run it, it gives no output on the command line.

Posted: **January 29th, 2018, 8:22 pm**

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.

Posted: **January 29th, 2018, 8:27 pm**

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?

Posted: **January 29th, 2018, 8:36 pm**

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.

AforAmpere wrote:How did you download minisat Goldtiger?

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!

ConwayLife.com

Logic Life Search (LLS)

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

Re: Logic Life Search