Code: Select all
./lls -p 10 -x 8 -y 0 -i -b 10 14 -r pB2ac345678/S012345678 --force_at_most 5 -S lingeling
Code: Select all
./lls -p 10 -x 8 -y 0 -i -b 10 14 -r pB2ac345678/S012345678 --force_at_most 5 -S lingeling
No :-(AforAmpere wrote:Is there some way to set the full period?
If I understand what you mean then in fact you already can. The 0/8 transitions have the letter "c" so for example pB0c12345678/S012345678-c forces B0 to be present and S0 not to be.Majestas32 wrote:Can you add a way to target rules with specifically B/S 0/8? Since you can't do that with -r p
Fairly certain you meant S8, and couldn't you just leave it out?Macbi wrote:If I understand what you mean then in fact you already can. The 0/8 transitions have the letter "c" so for example pB0c12345678/S012345678-c forces B0 to be present and S0 not to be.Majestas32 wrote:Can you add a way to target rules with specifically B/S 0/8? Since you can't do that with -r p
Yes and yes. The important thing is to distinguish pB0 (B0 might be present) from pB0c (B0 must be present.BlinkerSpawn wrote:Fairly certain you meant S8, and couldn't you just leave it out?
Wow! Thanks, that's great! Especially the tutorial. I added some links to them to the first post.Apple Bottom wrote:I've gone ahead and added a LifeWiki entry for LLS, as well as a tutorial containing some of the collected wisdom from this thread, as well as some examples, to help users get started (and familiar) with LLS.
Code: Select all
Dan@MINDRAY-GIAAK3B ~/lls
$ ./lls -S lingeling -r B2en3ij4a5e7e8/S1c2cek3-a4aiqw5aky -b 10 10 -p 55 -x 9 -y 0 -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...
Done
Time taken: 0.0 seconds
Unsatisfiable
The bounding box needs to big enough to cover the full evolution of the pattern. As the displacement is 9 this means there are only 1 or 2 columns left for the ship - which is very quickly found to not exist.danny wrote:It seems to give up. Is there something I've missed?Code: Select all
Dan@MINDRAY-GIAAK3B ~/lls $ ./lls -S lingeling -r B2en3ij4a5e7e8/S1c2cek3-a4aiqw5aky -b 10 10 -p 55 -x 9 -y 0 -i <snip output>
EDIT: Added the -m flag and it's still unsatisfiable
Code: Select all
if solution == "UNSATISFIABLE\n":
solution = "UNSAT\n"
Code: Select all
if solution[0:5] == "UNSAT":
solution = "UNSAT\n"
I've been looking into the methods used to solve large SAT problems in parallel, and the approach seems to be:Macbi wrote: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.
Thank you! I'm glad you like it.wildmyron wrote:@Macbi: Thank you for sharing this fantastic search program.
Thank you for this too. Hopefully it will make it easier for people to run LLS on Windows.After some misadventures with MSVC, I have managed to compile glucose-syrup natively on windows. Currently I've built the 4.0 version but I don't think it will take too much effort to build the 2017 competition version. I've attached a copy of the executable (and winpthreads dll which should go in the same folder). If there's interest I'll try to get the latest version compiled too.
I've found that glucose is very changeable on the 6 15 search. I just tried three times and got 14.5s, 2.2s and 27.4s. I don't know why exactly that search is so much worse than others.I haven't done much testing but I had roughly comparable performance to @rokicki's tests on the p6 knightship (with -M1) for the square bounding boxes, but strangely the 6 15 search took less than half the time.
I haven't tried cryptominisat (I focused on the solvers that did well in the SAT competition) but I did try using SMAC to tune the parameters for Glucose. I got a small speed up but nothing dramatic. I should try running it for longer though. I wish I had a second computer.Have you considered trying cryptominisat? I haven't been able to compile that one yet because, well, lets just say my MSVC is a bit old. It looks interesting in its ability to be trained on a large enough set of problems, so that it can guess at optimal parameters for the solver. This might be something doable for these search problems.
I hadn't thought of this! I'm surprised LLS still works with lingeling on Windows. I'll try to correct it. Something like 'if "UNSAT" in solution' does sound like the way to do it. I'll just have to be careful in case any of the solvers mention "UNSAT" in a comment. EDIT: Never mind, the comments have already been filtered out by thenI had to make a slight change to lls to get it to recognize UNSAT output because of \r\n in the solver output:
I changedin LLS_SAT_solvers.py toCode: Select all
if solution == "UNSATISFIABLE\n": solution = "UNSAT\n"
Edit: I suppose 'if "UNSAT" in solution:' is a more reliable way of doing the test, but whichever is fine.Code: Select all
if solution[0:5] == "UNSAT": solution = "UNSAT\n"
Wow! This sounds amazing. I hope it works out well.calcyman wrote:I've been looking into the methods used to solve large SAT problems in parallel, and the approach seems to be:
where the third stage is the slow, parallelisable one.
- Preprocess using lingeling -s to obtain a simplified set of clauses;
- Use the lookahead program march_cc to intelligently split the problem into disjoint 'cubes' of equal estimated difficulty;
- Independently attack each cube with an (ideally incremental) SAT solver. Cryptominisat, glucose and lingeling are all potential candidates.
I'll see whether I can make an adaptive program along these lines, where the third stage uses timing tests and grid searches over hyperparameters to determine which SAT solver and parameter choices work best for the problem at hand. This meta-solver could hopefully be used as a 'solver' for LLS.
The solver treengling (based on lingeling) implements cube-and-conquer, but not as well as a roll-your-own combination of march_cc + iglucose.Macbi wrote:Wow! This sounds amazing. I hope it works out well.
Is it so state-of-the-art that no SAT solver already does this?
Marijn Heule used this in 2016 to solve the Boolean Pythagorean Triples problem: https://arxiv.org/abs/1605.00723You would think that if this is the best way then it would have been used in the SAT competition. If not then maybe you can win this year!
We better start cooking up some huge problems then!calcyman wrote:I believe it's only the best way if you have a huge problem and want to distribute it over many machines, as was the case with the Boolean Pythagorean Triples problem.
Whilst I said preprocessing, the worst stage was either converting the search pattern to cnf, or perhaps exporting to dimacs (probably the former, but I'm not sure). I had specified -v3 and the search pattern had been displayed before Python's Mem usage jumped to over 3GB and the machine started swapping. There's only 4GB in this machine, not really enough these days, so on a decent machine I don't think this would have been an issue.Macbi wrote:I hadn't realised that RAM could become an issue. I'll see what I can do to cut down on it, but the answer might be "not much".wildmyron wrote:For the record I also ran a few searches for 10c/11, the broadest of which was this one:It took a lot longer than it needed to because I had insufficient RAM for the preprocessing step in Python, nevertheless it completed with no solution found.Code: Select all
python lls -r pB2a345678/S012345678 -i -p 11 -x 10 -y 0 -b 24 29 -s "D2-"
Yeah, the clause list is a list-of-lists-of-strings and can be really big. But the situation is twice as bad as it needs to be because I create a copy of the clause list to convert into the DIMACS format that the SAT solver needs. So presumably memory usage approximately doubles just as preprocessing finishes.wildmyron wrote:Whilst I said preprocessing, the worst stage was either converting the search pattern to cnf, or perhaps exporting to dimacs (probably the former, but I'm not sure). I had specified -v3 and the search pattern had been displayed before Python's Mem usage jumped to over 3GB and the machine started swapping. There's only 4GB in this machine, not really enough these days, so on a decent machine I don't think this would have been an issue.
Code: Select all
Solving...
x1P
Code: Select all
0,0,0,0,0,0,0,0,0,0,0,0,0
0,a,b,c,d,e,f,g,h,i,j,0,0
0,k,l,m,n,o,p,q,r,s,t,0,0
0,u,v,w,x,y,z,n1,n2,n3,1,0,0
0,n4,n5,n6,n7,n8,n9,m1,m2,m3,m4,0,0
0,m5,m6,m7,m8,m9,m0,i0,i1,i2,i3,0,0
0,i4,i5,i6,c0,c1,c2,c3,c4,c5,c6,0,0,
0,c7,c8,c9,c10,c11,c12,c13,c14,c15,c16,0,0
0,c17,c18,c19,c20,c21,c22,c23,c24,c25,c26,0,0
0,c27,c28,c29,c30,c31,c32,c33,c34,c35,c36,0,0
0,c37,c38,c39,c40,c41,c42,c43,c44,c45,c46,0,0
0,0,0,0,0,0,0,0,0,0,0,0,0
0,0,0,0,0,0,0,0,0,0,0,0,0
0,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,1,*,0
0,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,*,*,0
0,0,0,0,0,0,0,0,0,0,0,0,0
0,0,0,0,0,0,0,0,0,0,0,0,0
0,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,1,*,0
0,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,*,*,0
0,0,0,0,0,0,0,0,0,0,0,0,0
0,0,0,0,0,0,0,0,0,0,0,0,0
0,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,1,*,0
0,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,*,*,0
0,0,0,0,0,0,0,0,0,0,0,0,0
0,0,0,0,0,0,0,0,0,0,0,0,0
0,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,1,*,0
0,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,*,*,0
0,0,0,0,0,0,0,0,0,0,0,0,0
0,0,0,0,0,0,0,0,0,0,0,0,0
0,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,1,*,0
0,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,*,*,0
0,0,0,0,0,0,0,0,0,0,0,0,0
0,0,0,0,0,0,0,0,0,0,0,0,0
0,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,1,*,0
0,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,*,*,0
0,*,*,*,*,*,*,*,*,*,*,*,0
0,0,0,0,0,0,0,0,0,0,0,0,0
0,0,0,0,0,0,0,0,0,0,0,0,0
0,0,a,b,c,d,e,f,g,h,i,j,0
0,0,k,l,m,n,o,p,q,r,s,t,0
0,0,u,v,w,x,y,z,n1,n2,n3,1,0
0,0,n4,n5,n6,n7,n8,n9,m1,m2,m3,m4,0
0,0,m5,m6,m7,m8,m9,m0,i0,i1,i2,i3,0
0,0,i4,i5,i6,c0,c1,c2,c3,c4,c5,c6,0,
0,0,c7,c8,c9,c10,c11,c12,c13,c14,c15,c16,0
0,0,c17,c18,c19,c20,c21,c22,c23,c24,c25,c26,0
0,0,c27,c28,c29,c30,c31,c32,c33,c34,c35,c36,0
0,0,c37,c38,c39,c40,c41,c42,c43,c44,c45,c46,0
0,0,0,0,0,0,0,0,0,0,0,0,0
Code: Select all
$ ./lls -S lingeling loafer.txt -v3
Getting search pattern...
Creating search pattern from file "loafer.txt" ...
Reading file "loafer.txt" ...
Done
Parsing input pattern...
Done
Pattern parsed as:
0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
0, a, b, c, d, e, f, g, h, i, j, 0, 0
0, k, l, m, n, o, p, q, r, s, t, 0, 0
0, u, v, w, x, y, z, n1, n2, n3, 1, 0, 0
0, n4, n5, n6, n7, n8, n9, m1, m2, m3, m4, 0, 0
0, m5, m6, m7, m8, m9, m0, i0, i1, i2, i3, 0, 0
0, i4, i5, i6, c0, c1, c2, c3, c4, c5, c6, 0, 0
0, c7, c8, c9,c10,c11,c12,c13,c14,c15,c16, 0, 0
0,c17,c18,c19,c20,c21,c22,c23,c24,c25,c26, 0, 0
0,c27,c28,c29,c30,c31,c32,c33,c34,c35,c36, 0, 0
0,c37,c38,c39,c40,c41,c42,c43,c44,c45,c46, 0, 0
0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
0, *, *, *, *, *, *, *, *, *, *, *, 0
0, *, *, *, *, *, *, *, *, *, *, *, 0
0, *, *, *, *, *, *, *, *, *, 1, *, 0
0, *, *, *, *, *, *, *, *, *, *, *, 0
0, *, *, *, *, *, *, *, *, *, *, *, 0
0, *, *, *, *, *, *, *, *, *, *, *, 0
0, *, *, *, *, *, *, *, *, *, *, *, 0
0, *, *, *, *, *, *, *, *, *, *, *, 0
0, *, *, *, *, *, *, *, *, *, *, *, 0
0, *, *, *, *, *, *, *, *, *, *, *, 0
0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
0, *, *, *, *, *, *, *, *, *, *, *, 0
0, *, *, *, *, *, *, *, *, *, *, *, 0
0, *, *, *, *, *, *, *, *, *, 1, *, 0
0, *, *, *, *, *, *, *, *, *, *, *, 0
0, *, *, *, *, *, *, *, *, *, *, *, 0
0, *, *, *, *, *, *, *, *, *, *, *, 0
0, *, *, *, *, *, *, *, *, *, *, *, 0
0, *, *, *, *, *, *, *, *, *, *, *, 0
0, *, *, *, *, *, *, *, *, *, *, *, 0
0, *, *, *, *, *, *, *, *, *, *, *, 0
0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
0, *, *, *, *, *, *, *, *, *, *, *, 0
0, *, *, *, *, *, *, *, *, *, *, *, 0
0, *, *, *, *, *, *, *, *, *, 1, *, 0
0, *, *, *, *, *, *, *, *, *, *, *, 0
0, *, *, *, *, *, *, *, *, *, *, *, 0
0, *, *, *, *, *, *, *, *, *, *, *, 0
0, *, *, *, *, *, *, *, *, *, *, *, 0
0, *, *, *, *, *, *, *, *, *, *, *, 0
0, *, *, *, *, *, *, *, *, *, *, *, 0
0, *, *, *, *, *, *, *, *, *, *, *, 0
0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
0, *, *, *, *, *, *, *, *, *, *, *, 0
0, *, *, *, *, *, *, *, *, *, *, *, 0
0, *, *, *, *, *, *, *, *, *, 1, *, 0
0, *, *, *, *, *, *, *, *, *, *, *, 0
0, *, *, *, *, *, *, *, *, *, *, *, 0
0, *, *, *, *, *, *, *, *, *, *, *, 0
0, *, *, *, *, *, *, *, *, *, *, *, 0
0, *, *, *, *, *, *, *, *, *, *, *, 0
0, *, *, *, *, *, *, *, *, *, *, *, 0
0, *, *, *, *, *, *, *, *, *, *, *, 0
0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
0, *, *, *, *, *, *, *, *, *, *, *, 0
0, *, *, *, *, *, *, *, *, *, *, *, 0
0, *, *, *, *, *, *, *, *, *, 1, *, 0
0, *, *, *, *, *, *, *, *, *, *, *, 0
0, *, *, *, *, *, *, *, *, *, *, *, 0
0, *, *, *, *, *, *, *, *, *, *, *, 0
0, *, *, *, *, *, *, *, *, *, *, *, 0
0, *, *, *, *, *, *, *, *, *, *, *, 0
0, *, *, *, *, *, *, *, *, *, *, *, 0
0, *, *, *, *, *, *, *, *, *, *, *, 0
0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
0, *, *, *, *, *, *, *, *, *, *, *, 0
0, *, *, *, *, *, *, *, *, *, *, *, 0
0, *, *, *, *, *, *, *, *, *, 1, *, 0
0, *, *, *, *, *, *, *, *, *, *, *, 0
0, *, *, *, *, *, *, *, *, *, *, *, 0
0, *, *, *, *, *, *, *, *, *, *, *, 0
0, *, *, *, *, *, *, *, *, *, *, *, 0
0, *, *, *, *, *, *, *, *, *, *, *, 0
0, *, *, *, *, *, *, *, *, *, *, *, 0
0, *, *, *, *, *, *, *, *, *, *, *, 0
0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
0, 0, a, b, c, d, e, f, g, h, i, j, 0
0, 0, k, l, m, n, o, p, q, r, s, t, 0
0, 0, u, v, w, x, y, z, n1, n2, n3, 1, 0
0, 0, n4, n5, n6, n7, n8, n9, m1, m2, m3, m4, 0
0, 0, m5, m6, m7, m8, m9, m0, i0, i1, i2, i3, 0
0, 0, i4, i5, i6, c0, c1, c2, c3, c4, c5, c6, 0
0, 0, c7, c8, c9,c10,c11,c12,c13,c14,c15,c16, 0
0, 0,c17,c18,c19,c20,c21,c22,c23,c24,c25,c26, 0
0, 0,c27,c28,c29,c30,c31,c32,c33,c34,c35,c36, 0
0, 0,c37,c38,c39,c40,c41,c42,c43,c44,c45,c46, 0
0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
Done
Standardising variable names...
Done
Done
Preprocessing...
Optimising search pattern...
Improving search pattern (Pass 1) ...
Improving grid...
Unsatisfiability proved in preprocessing
Done
Time taken: 0 seconds
Unsatisfiable
The only odd thing I noticed on a quick scan through was an extra comma on the seventh line of the input, but that doesn't seem to have made any difference to the parsing code, at least according to the printout.Rhombic wrote:The following snippet is meant to be a crude search for a loafer. The fun bit is the forced live cell throughout every generation in row 4 (a stator cell). It is clearly self-contained yet LLS does not manage to run this...Why?
-r pB1e(other birth conditions)/(survival conditions)Saka wrote: Also is there a way to force a transition? I want to force B1e.