Logic Life Search
-
- Posts: 1334
- 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 manage the 5S project, which collects all known spaceship speeds in Isotropic Non-totalistic rules. I also wrote EPE, a tool for searching in the INT rulespace.
Things to work on:
- Find (7,1)c/8 and 9c/10 ships in non-B0 INT.
- EPE improvements.
Things to work on:
- Find (7,1)c/8 and 9c/10 ships in non-B0 INT.
- EPE improvements.
Re: Logic Life Search
On Ubuntu, I can quickly find Brain using the --symmetry="D2|" flag:
On the other hand, a search for the symmetric c/4 orthogonal is taking hours.
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!
What do you do with ill crystallographers? Take them to the mono-clinic!
Re: Logic Life Search
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.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.
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.
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.calcyman wrote:On the other hand, a search for the symmetric c/4 orthogonal is taking hours.
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.
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.
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: 764
- Joined: June 21st, 2016, 8:00 am
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):
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.
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
P.S. Based on the results its found so far, the program seems really cool Macbi.
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
added:
print "Executing command ", command
right before
solver_process = subprocess.Popen(
Make sure to match indentation exactly.
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.
- Goldtiger997
- Posts: 764
- Joined: June 21st, 2016, 8:00 am
Re: Logic Life Search
Thanks rokicki, that seemed to work. However, now I get this message, which claims the glider does not exist:
"Number of undetermined cells: 0" sounds quite suspicious.
Any ideas...
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
Any ideas...
Re: Logic Life Search
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.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).
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]
Re: Logic Life Search
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.Goldtiger997 wrote:"Number of undetermined cells: 0" sounds quite suspicious.
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: 764
- Joined: June 21st, 2016, 8:00 am
Re: Logic Life Search
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: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.
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
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.
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.
Re: Logic Life Search
Actually it did finish in about 9 minutes (I started it up again after I posted).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.
Thanks for the suggestions on modifications!
-
- Posts: 1334
- Joined: July 1st, 2016, 3:58 pm
Re: Logic Life Search
Can you post the executable? That would help a lot, and I'll see if I get the same issue.Goldtiger997 wrote: I wonder if anyone else with windows/cygwin can reproduce the same results as me...
I manage the 5S project, which collects all known spaceship speeds in Isotropic Non-totalistic rules. I also wrote EPE, a tool for searching in the INT rulespace.
Things to work on:
- Find (7,1)c/8 and 9c/10 ships in non-B0 INT.
- EPE improvements.
Things to work on:
- Find (7,1)c/8 and 9c/10 ships in non-B0 INT.
- EPE improvements.
- Goldtiger997
- Posts: 764
- Joined: June 21st, 2016, 8:00 am
Re: Logic Life Search
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: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.)
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
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'
Anyway, here you go AforAmpere:
-
- Posts: 1334
- 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:
Is this the same problem you had Goldtiger?
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
Last edited by AforAmpere on January 29th, 2018, 7:32 pm, edited 1 time in total.
I manage the 5S project, which collects all known spaceship speeds in Isotropic Non-totalistic rules. I also wrote EPE, a tool for searching in the INT rulespace.
Things to work on:
- Find (7,1)c/8 and 9c/10 ships in non-B0 INT.
- EPE improvements.
Things to work on:
- Find (7,1)c/8 and 9c/10 ships in non-B0 INT.
- EPE improvements.
Re: Logic Life Search
Yes! Renaming the solver was a clever idea, but sadly they do input and output slightly differently so LLS has to treat them differently.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:
Was a file called "temp_SAT_solver_output" actually created?However, by renaming it back to minisat, I get this new error, which involves temp_SAT_solver_output not being able to be found:
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.
Re: Logic Life Search
Renaming minisat to glucose-syrup totally won't work, they have different output formats.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
-
- Posts: 1334
- 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 manage the 5S project, which collects all known spaceship speeds in Isotropic Non-totalistic rules. I also wrote EPE, a tool for searching in the INT rulespace.
Things to work on:
- Find (7,1)c/8 and 9c/10 ships in non-B0 INT.
- EPE improvements.
Things to work on:
- Find (7,1)c/8 and 9c/10 ships in non-B0 INT.
- EPE improvements.
Re: Logic Life Search
You would just have to add ".txt" after the filename in the linesAforAmpere 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?
Code: Select all
solution = LLS_files.string_from_file("temp_SAT_solver_output", indent = indent + 1, verbosity = verbosity)
Code: Select all
os.remove("temp_SAT_solver_output")
-
- Posts: 1334
- Joined: July 1st, 2016, 3:58 pm
Re: Logic Life Search
It still could not find the file.
I manage the 5S project, which collects all known spaceship speeds in Isotropic Non-totalistic rules. I also wrote EPE, a tool for searching in the INT rulespace.
Things to work on:
- Find (7,1)c/8 and 9c/10 ships in non-B0 INT.
- EPE improvements.
Things to work on:
- Find (7,1)c/8 and 9c/10 ships in non-B0 INT.
- EPE improvements.
Re: Logic Life Search
Did you try running minisat separately?
-
- Posts: 1334
- Joined: July 1st, 2016, 3:58 pm
Re: Logic Life Search
When I run it, it gives no output on the command line.
I manage the 5S project, which collects all known spaceship speeds in Isotropic Non-totalistic rules. I also wrote EPE, a tool for searching in the INT rulespace.
Things to work on:
- Find (7,1)c/8 and 9c/10 ships in non-B0 INT.
- EPE improvements.
Things to work on:
- Find (7,1)c/8 and 9c/10 ships in non-B0 INT.
- EPE improvements.
Re: Logic Life Search
That makes it sound like minisat isn't working at all.AforAmpere wrote:When I run it, it gives no output on the command line.
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.
-
- Posts: 1334
- 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 manage the 5S project, which collects all known spaceship speeds in Isotropic Non-totalistic rules. I also wrote EPE, a tool for searching in the INT rulespace.
Things to work on:
- Find (7,1)c/8 and 9c/10 ships in non-B0 INT.
- EPE improvements.
Things to work on:
- Find (7,1)c/8 and 9c/10 ships in non-B0 INT.
- EPE improvements.
- Goldtiger997
- Posts: 764
- Joined: June 21st, 2016, 8:00 am
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 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!AforAmpere wrote:How did you download minisat Goldtiger?