ConwayLife.com

Posted: **January 30th, 2018, 7:41 am**

This search is supposed to look for 8c/10, but finds a 4c/5 instead. Is there some way to set the full period?

./lls -p 10 -x 8 -y 0 -i -b 10 14 -r pB2ac345678/S012345678 --force_at_most 5 -S lingeling

Posted: **January 30th, 2018, 8:03 am**

AforAmpere wrote:Is there some way to set the full period?

No :-(

I'll add this at some point.

(For oscillators you can do "-c 3 5" to force generations 3 and 5 to be different (for example). But I don't yet have this working with spaceships. This will probably come as an update adding support for all possible symmetries, such as glide reflect, rotation by 90 degrees, and so on. I hope that for each symmetry there will be an option to force it, and an option to ban it.)

There is some element of randomness to the SAT solvers. So you could try repeating the search, or using the -n option, to see if one of the results has the full period.

By the way you can use -h to see all of LLS's options.

Posted: **January 30th, 2018, 11:53 am**

Can you add a way to target rules with specifically B/S 0/8? Since you can't do that with -r p

Posted: **January 30th, 2018, 12:11 pm**

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

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.

Posted: **January 30th, 2018, 12:46 pm**

Posted: **January 30th, 2018, 12:47 pm**

Macbi wrote:
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
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.

Fairly certain you meant S8, and couldn't you just leave it out?

Posted: **January 30th, 2018, 12:51 pm**

BlinkerSpawn wrote:Fairly certain you meant S8, and couldn't you just leave it out?

Yes and yes. The important thing is to distinguish pB0 (B0 might be present) from pB0c (B0 must be present.

Posted: **January 30th, 2018, 1:36 pm**

Posted: **January 30th, 2018, 1:41 pm**

It appears I can't type today. I am on my phone though.

Posted: **January 30th, 2018, 4:38 pm**

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.

(@Macbi: great work, BTW, this is an excellent tool to have.)

Posted: **January 30th, 2018, 4:52 pm**

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.

Wow! Thanks, that's great! Especially the tutorial. I added some links to them to the first post.

Posted: **January 30th, 2018, 7:26 pm**

Running the search on the first page for the glider returns unsatisfiable with -i, but without it, it returns a blank pattern.

Posted: **January 31st, 2018, 10:59 pm**

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

It seems to give up. Is there something I've missed?
EDIT: Added the -m flag and it's still unsatisfiable

Posted: **February 1st, 2018, 12:30 am**

danny wrote:
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>
It seems to give up. Is there something I've missed?
EDIT: Added the -m flag and it's still 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.

--

@Macbi: Thank you for sharing this fantastic search program.

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 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.
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 had to make a slight change to lls to get it to recognize UNSAT output because of \r\n in the solver output:
I changed

Code: Select all

        if solution == "UNSATISFIABLE\n":
            solution = "UNSAT\n"

in LLS_SAT_solvers.py to

Code: Select all

        if solution[0:5] == "UNSAT":
            solution = "UNSAT\n"

Edit: I suppose 'if "UNSAT" in solution:' is a more reliable way of doing the test, but whichever is fine.

Edit 2: Updated zip file with copyright and licensing information.

Posted: **February 1st, 2018, 7:48 am**

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.

I've been looking into the methods used to solve large SAT problems in parallel, and the approach seems to be:

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.

where the third stage is the slow, parallelisable one.

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.

Posted: **February 1st, 2018, 9:58 am**

wildmyron wrote:@Macbi: Thank you for sharing this fantastic search program.

Thank you! I'm glad you like it.

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.

Thank you for this too. Hopefully it will make it easier for people to run LLS on Windows.

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

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

I had to make a slight change to lls to get it to recognize UNSAT output because of \r\n in the solver output:
I changed
Code: Select all
        if solution == "UNSATISFIABLE\n":
            solution = "UNSAT\n"
in LLS_SAT_solvers.py to
Code: Select all
        if solution[0:5] == "UNSAT":
            solution = "UNSAT\n"
Edit: I suppose 'if "UNSAT" in solution:' is a more reliable way of doing the test, but whichever is fine.

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 then

calcyman wrote:I've been looking into the methods used to solve large SAT problems in parallel, and the approach seems to be:

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.
where the third stage is the slow, parallelisable one.

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.

Wow! This sounds amazing. I hope it works out well.

Is it so state-of-the-art that no SAT solver already does this? You 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!

Posted: **February 1st, 2018, 2:07 pm**

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?

The solver treengling (based on lingeling) implements cube-and-conquer, but not as well as a roll-your-own combination of march_cc + iglucose.

You 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!

Marijn Heule used this in 2016 to solve the Boolean Pythagorean Triples problem: https://arxiv.org/abs/1605.00723

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.

Posted: **February 1st, 2018, 4:03 pm**

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.

We better start cooking up some huge problems then!

The first to spring to mind are knightships and p19 oscillators, but I've got the impression that programs like gfind are much better for those sorts of things than programs like WLS. So LLS probably isn't the right tool for the job.

Perhaps a 2c/3 signal turner like dvgrn has mentioned?

Posted: **February 2nd, 2018, 6:53 am**

New parameter for LLS

I sent you a PM about the possibility to include this idea, which would make LLS a great catalyst search engine. In fact, the same concept could also be coded into Bellman and would allow the discovery of thousands of new conduits.

I think LLS is a super-powerful tool - your last message was rather modest, in my opinion! You have created a great script, and with further optimisations, you can feed it so many different pattern-solving problems that it can tackle pretty much all CA questions!

All well thought-through problems with clever restrictions can be tackled easily. The only set of problems it cannot tackle is otherwise trivial-to-code unrestricted brute-force searches such as searchRules (the parent script of Rulesrc). However, since the input for these is pretty much random and there is no restriction on the evolution, it is not a major loss at all. LLS tackles the harder questions as guided by the user, even for OCA.

So the main thing, my first paragraph, but also making sure that LLS does not "specialise" in the sense that even if there are many ways to enter input, it should be just that: a door to introduce problems into a SAT solver. Optimising the different parameters you can use for searching allows it to perform well in many different tasks.

Towards hyphenated tools: the importance of Bellman-LLS

Bellman has very clever coding for catalyst searches, I have realised that beyond the heuristic approach there must be a way to hyphenate Bellman-LLS. Why would this be worth the effort? Because Bellman can determine suitability of starting patterns and what branches to search (better than LLS, if I understand the approaches correctly) while LLS is likely to find better solutions and to carry out the solution-finding phase better.
In other words, if Bellman realised that certain cells in the catalyst should be ON, then Bellman could run a couple LLS searches forcing those cells to be ON.
Coding this last bit is a massive challenge - we do not want to run superfluous LLS searches or those that take way too long! How do we decide when Bellman should consider a LLS search as suitable? However, if we managed to get through this first step, the resulting coupled program would be an amazing accomplishment.

Posted: **February 2nd, 2018, 7:00 am**

From 5S project thread:

Macbi wrote:
wildmyron wrote:For the record I also ran a few searches for 10c/11, the broadest of which was this one:
Code: Select all
python lls -r pB2a345678/S012345678 -i -p 11 -x 10 -y 0 -b 24 29 -s "D2-"
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.
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".

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.

I guess the primary cause of such high Mem usage is the sheer number of clauses, but Python isn't exactly known for being efficient storage of large lists of ints. I say this without having looked too hard at the relevant code, but it might pay to look at more efficient storage of the clauses (perhaps with numpy arrays), and whether you can get away without deep copying in some places.

I've managed to compile cryptominisat, but just using the default options it seems to come second best cf. glucose-syrup. There are a lot of options to tweak though.

P.S. I think the other Windows users didn't have the same UNSATISFIABLE issue as me because they've compiled with gcc in cygwin and so lingeling is using '\n' for EOL.

Posted: **February 2nd, 2018, 7:33 am**

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.

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.

My current working version of LLS doesn't create this copy and just creates the DIMACS output as a string, so the memory usage should be nearly halved. If I understand GitHub correctly you should be able to get this version from the "develop" branch.

In fact I don't think there's any real reason why LLS needs to store the list of clauses in RAM at all. They could go directly into the DIMACS output file. This would mean that we couldn't do any "optimisation" to the list of clauses, but I suspect that that isn't helping much anyway.

Posted: **February 2nd, 2018, 9:34 am**

What's preprocessing for? Most of my search time is spent on preprocessing which is annoying.

Also is there a way to force a transition? I want to force B1e.

EDIT:
Also, what does

Code: Select all

Solving...
x1P

mean?

Posted: **February 2nd, 2018, 11:22 am**

I was not going to post this problem so as not to clog the thread (because I'd consider this earlier post to be more important than any of my temporary input issues), but this happened:

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:

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

as it gets stopped in preprocessing as follows:

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

Why?

Posted: **February 2nd, 2018, 12:28 pm**

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?

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.

Other than that, T=7 is the same text as T=0, with one column of zeros shifted from the end to the beginning, the variable names are all unique as far as I can see, and the 11x10 area correctly allows for the loafer's trailing sparks on the left.

So it looks a lot like Macbi's original example for finding a glider -- I don't see an obvious problem with the setup. But I haven't spent the time to get LLS running on my system yet. What happens if you replace the "1"s with another variable? Do you get the expected empty pattern?

Posted: **February 2nd, 2018, 1:28 pm**

Saka wrote: Also is there a way to force a transition? I want to force B1e.

-r pB1e(other birth conditions)/(survival conditions)

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