Page 3 of 13
Re: Logic Life Search
Posted: January 29th, 2018, 8:43 pm
by Macbi
Fantastic! If you want to change the default solver for your copy of LLS it's the line
Code: Select all
solver = "glucose-syrup" # Default solver
in LLS_SAT_solvers.py. I think I found plingeling was the fastest version, but you may want to test that.
Re: Logic Life Search
Posted: January 29th, 2018, 8:46 pm
by AforAmpere
Yes! Lingeling works! It did a search successfully, which is great.
Re: Logic Life Search
Posted: January 29th, 2018, 8:49 pm
by AforAmpere
What would be a search that finds the (2,1)c/3 you found, just to test?
Re: Logic Life Search
Posted: January 29th, 2018, 8:57 pm
by Goldtiger997
Macbi wrote:I think I found plingeling was the fastest version, but you may want to test that.
Okay I'll test that and report on the results I find.
AforAmpere wrote:What would be a search that finds the (2,1)c/3 you found, just to test?
I tried ./lls -p 3 -x 2 -y 1 -i -m -b 6 6 -r p, which does give a (2,1)c/3, but not the 5-cell one Macbi found.
Edit: This thread is getting pretty clogged up, so I'll just edit this in.
For the above search, lingeling took 0.302 seconds, plingeling took 0.799 seconds, and treengeling took 0.841 seconds.
Re: Logic Life Search
Posted: January 29th, 2018, 8:59 pm
by Majestas32
So how do you download this on windows? Either minisat or glucose is fine
Re: Logic Life Search
Posted: January 29th, 2018, 9:02 pm
by AforAmpere
Download lingeling and follow Goldtiger's instructions, it seems to be the only Cygwin compatible one.
Re: Logic Life Search
Posted: January 29th, 2018, 9:05 pm
by Macbi
AforAmpere wrote:What would be a search that finds the (2,1)c/3 you found, just to test?
Code: Select all
./lls -p 3 -x 2 -y 1 -i -b 6 6 -r pB1-c2345678/S012345678 --force_at_most 5
Goldtiger997 wrote:I tried ./lls -p 3 -x 2 -y 1 -i -m -b 6 6 -r p, which does give a (2,1)c/3, but not the 5-cell one Macbi found.
You don't need both -i and -m, by the way.
Re: Logic Life Search
Posted: January 29th, 2018, 9:13 pm
by Majestas32
Is the lingeling-bbc-9230380-160707.tar.gz version the right one?
Re: Logic Life Search
Posted: January 29th, 2018, 9:21 pm
by Macbi
Majestas32 wrote:Is the lingeling-bbc-9230380-160707.tar.gz version the right one?
It's the one I've been using.
Re: Logic Life Search
Posted: January 29th, 2018, 9:24 pm
by Majestas32
OK so then how do you decompress it
Re: Logic Life Search
Posted: January 29th, 2018, 9:26 pm
by AforAmpere
I used 7zip to decompress it, you do it twice, once on the .gz, and once on the tar.
Re: Logic Life Search
Posted: January 29th, 2018, 9:26 pm
by Majestas32
And then what do you do with it with Cygwin
Re: Logic Life Search
Posted: January 29th, 2018, 9:28 pm
by AforAmpere
Follow Goldtiger's instructions to compile, then put the compiled lingeling in the solvers folder in the LLS file.
Re: Logic Life Search
Posted: January 29th, 2018, 9:30 pm
by Majestas32
Ah. Ok. I suppose I should download the lls file then
Re: Logic Life Search
Posted: January 29th, 2018, 9:34 pm
by AforAmpere
Ignore this.
Re: Logic Life Search
Posted: January 29th, 2018, 9:39 pm
by Majestas32
So this is what the solvers folder should look like right?
Re: Logic Life Search
Posted: January 29th, 2018, 9:41 pm
by AforAmpere
No, just put the lingeling.exe or plingeling.exe in the solvers folder.
Re: Logic Life Search
Posted: January 29th, 2018, 9:42 pm
by Majestas32
lingeling.exe??? Is there supposed to be a lingeling.exe???
Re: Logic Life Search
Posted: January 29th, 2018, 9:56 pm
by AforAmpere
Majestas32 wrote:lingeling.exe??? Is there supposed to be a lingeling.exe???
Did you follow these instructions?
Goldtiger997 wrote: Enter "./configure.sh". Enter "make"
If you cd to your folder with lingeling, and do that, the .exe files should be made.
Re: Logic Life Search
Posted: January 29th, 2018, 10:23 pm
by Majestas32
So just cd lingeling-bbc-9230380-160707 or do I have to specify the full path?
Re: Logic Life Search
Posted: January 29th, 2018, 10:27 pm
by AforAmpere
Full path, in the Cygwin command line. Well, full path inside Cygwin. I did:
I had put LIngeling inside the Cygwin folder in a Python subfolder.
Re: Logic Life Search
Posted: January 29th, 2018, 10:28 pm
by Majestas32
Starting with C:\ ?
Re: Logic Life Search
Posted: January 29th, 2018, 10:30 pm
by AforAmpere
Just try putting the lingeling folder in your Cygwin folder, rename to just lingeling and do cd /lingeling, then follow the above instructions.
Re: Logic Life Search
Posted: January 30th, 2018, 12:49 am
by Majestas32
I get this error:
Code: Select all
Solving...
Traceback (most recent call last):
File "./lls", line 195, in <module>
indent = indent, verbosity = verbosity
File "/lls/src/LLS.py", line 61, in preprocess_solve_and_postprocess
indent = indent, verbosity = verbosity
File "/lls/src/LLS.py", line 175, in preprocess_and_solve
indent = indent, verbosity = verbosity)
File "/lls/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 "/lls/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 "/lls/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
Re: Logic Life Search
Posted: January 30th, 2018, 1:00 am
by Goldtiger997
Majestas32 wrote:I get this error:...
I had this problem before.
Either you run with "-S lingeling", or change your default solver by doing what Macbi suggested
here.
Hope it works now.