Logic Life Search

For scripts to aid with computation or simulation in cellular automata.
Post Reply
User avatar
Macbi
Posts: 903
Joined: March 29th, 2009, 4:58 am

Re: Logic Life Search

Post by Macbi » February 2nd, 2018, 5:51 pm

Saka wrote:What's preprocessing for? Most of my search time is spent on preprocessing which is annoying.
LLS makes certain deductions before handing the problem over to the SAT solver. The idea being to get the easy stuff out of the way and make sure that the SAT solver is only focused on the hardest bit of the problem. I'm now beginning to think this is stupid, since the SAT solver can probably make these deductions for itself anyway. But it's maybe worth running it before really hard proplems, just to make sure the SAT solver doesn't get tripped up on something easy.

So optimisation is now off by default but can be turned on via the --optimise flag. A tiny amount of optimisation is still done to save time by preventing the encoding of the transition rule for cells where it's redundant.

The bleeding-edge version of LLS should be available from the "develop" branch on GitHub.
Also is there a way to force a transition? I want to force B1e.
This would be pB01e2345678/S012345678. If you want to use it for the 5S project then you also want to ban B0 and B1c so use pB1e-c2345678/S012345678
EDIT:
Also, what does

Code: Select all

Solving...
x1P

mean?
No idea, that seems weird.
Rhombic wrote:Bellman-LLS
I had a look at the Bellman documentation and I'm still not much the wiser on how it works. As a corollary to that, I don't have any good ideas on how to merge the two.

I will say that Bellman seems to pick up a lot of its speed by having lots of different constraints that tell it when to end a search early. All of these constraints can (with various amounts of effort) be implemented in LLS. If you did this then they might become comparable.
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:
Ugh, sorry. This is caused by the fact that Windows stores newlines as "\r\n" (i.e. carriage-return newline) rather than "\n" as used on Linux and Mac. I thought I had anticipated this in advance and accounted for it, but I messed up. If you look closely at the LLS output you can see that LLS thinks that every row of the input pattern is supposed to be an entire generation. That's why it's UNSAT.

I think I've fixed this now, but who knows?
dvgrn wrote: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.
LLS views any combination of commas and spaces as a separator. [This means that if for some perverted reason you wanted to use "" as a variable name, you would have to represent it as "--".]

Stators

In other news, I implemented a new feature. Assume that the file "pattern.csv" contains the first generation of an oscillator given as a comma separated grid of 0s and 1s (with enough room in the grid for the entire evolution of the oscillator). Then the command

Code: Select all

./lls --stator pattern.csv
creates a search for other oscillators with the same rotor, but different stators. This can be used in combination with --force_at_most to optimise the population of the stator. For example I just reduced the population of one of the guns in the collection. (Cardinality constraints in LLS are still very slow for large numbers of variables, so this kind of thing takes a while.)

EDIT: I also made a Golly script that makes the csv out of the current selection:

Code: Select all

import golly as g

x_0, y_0, width, height = g.getselrect()
grid = [["0" for x in xrange(width)] for y in xrange(height)]
cells = g.getcells([x_0, y_0, width, height])
for i in xrange(len(cells)/2):
    grid[cells[2*i + 1] - y_0][cells[2*i] - x_0] = "1"
with open("pattern.csv", "w") as output_file:
    output_file.write("\n".join(",".join(row) for row in grid) + "\n")

AforAmpere
Posts: 1334
Joined: July 1st, 2016, 3:58 pm

Re: Logic Life Search

Post by AforAmpere » February 2nd, 2018, 6:06 pm

Have you updated B0 searches to alternate yet? Also, is there a way to force B0? I want to try searching for a (2,1)c/2.
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.

User avatar
Macbi
Posts: 903
Joined: March 29th, 2009, 4:58 am

Re: Logic Life Search

Post by Macbi » February 2nd, 2018, 6:22 pm

AforAmpere wrote:Have you updated B0 searches to alternate yet?
No
Also, is there a way to force B0? I want to try searching for a (2,1)c/2.
pB0c

User avatar
vyznev
Posts: 27
Joined: April 23rd, 2016, 4:08 am

Re: Logic Life Search

Post by vyznev » February 2nd, 2018, 8:35 pm

Macbi wrote:
AforAmpere wrote:Have you updated B0 searches to alternate yet?
No
I tried to implement this feature into LLS myself, but clearly I screwed up something and just ended up generating an unsatisfiable mess. :( So as a work-around, I made a script to generate LLS input files with strobing boundaries instead.

It actually has a couple of handy features that could be useful for non-B0 rules too, like automatically mirroring / rotating the last generation to search for glide-symmetric or rotating patterns. Maybe that could be a useful feature to add to LLS itself, too? ;)

I also wrote a quick little script to convert isotropic von Neumann rule strings to a format that LLS understands. Together, I managed to use the scripts to make LLS re-find this naturally occurring little 2c/4 in B024/S1V that I found quite I few years ago:

Code: Select all

x = 10, y = 12, rule = B01c2-ak3acjkr4-jnrty5acjkr6-ak7c8/S1e2ak3inqy4ny5e
bbbbbbbbbb$
bbbbbbbbbb$
bbbbbbbbbb$
bbbbbbbbbb$
bbbbbbbbbb$
bbbbbbbbbb$
bbbbbbobbb$
bbbbobobbb$
bbbbbbbbbb$
bbbbbbbbbb$
bbbbbbbbbb$
bbbbbbbbbb!
Now let's see if I can actually use this to find something new... :mrgreen:

Ps. Besides strobing backgrounds and glide symmetry, another feature that I'd kind of like to see in LLS would be exhaustive searching for all solutions. I believe that's something at least some SAT solvers can already do, and if not, it should be possible to kluge it: every time you find a solution, just append a constraint to the SAT solver input that says "nope, I don't want this solution" and restart the process. Repeat until the problem is unsatisfiable. Of course, it would be more efficient to let the SAT solver itself do this, so that it can reuse any clauses it has learned in previous searches.

User avatar
calcyman
Moderator
Posts: 2932
Joined: June 1st, 2009, 4:32 pm

Re: Logic Life Search

Post by calcyman » February 2nd, 2018, 9:42 pm

I really like this program.

Is there a way to separate out the following phases, so they could be run separately?
  • Problem construction: arguments --> (DIMACS file, saved_state)
  • SAT solving: DIMACS file --> DIMACS solution
  • Solution decoding: (DIMACS solution, saved_state) --> pattern RLE
I ask because I've now created a program along the lines I was describing, and it's capable of finding a satisfying assignment for the output of:

Code: Select all

python lls -M0 --save_dimacs -m -b 21 11 -s "D2|" -p 4 -x 0 -y 1
(that is to say, a c/4 orthogonal symmetric spaceship) within several minutes. But I have no way of recovering the pattern RLE from this solution!
What do you do with ill crystallographers? Take them to the mono-clinic!

rokicki
Posts: 80
Joined: August 6th, 2009, 12:26 pm

Re: Logic Life Search

Post by rokicki » February 2nd, 2018, 11:08 pm

I was going to suggest that the first w * h * g literals be reserved for the actual cell state, and
all the literals above this be used for the calculations.

This way we can run the Python script once to set up a "generic" w * h * g (with appropriate offset)
playing field, and generate a multi-megabyte CNF.

To insert initial conditions, we then just write a tiny CNF that sets up the appropriate cells with
their initial state. To read out the result we can directly interpret the result from the solution
file since we know which literal is which cell.

This is what I've been doing with my Perl scripts, and I've found it very workable. The SAT solvers
are *very* fast at parsing CNF and simplifying redundancies (much faster than Python or Perl can
write the CNF, certainly).

User avatar
Macbi
Posts: 903
Joined: March 29th, 2009, 4:58 am

Re: Logic Life Search

Post by Macbi » February 3rd, 2018, 7:39 am

vyznev wrote:
Macbi wrote:
AforAmpere wrote:Have you updated B0 searches to alternate yet?
No
I tried to implement this feature into LLS myself, but clearly I screwed up something and just ended up generating an unsatisfiable mess. :( So as a work-around, I made a script to generate LLS input files with strobing boundaries instead.
The script is great! Hopefully strobing will be implemented into LLS soon.
It actually has a couple of handy features that could be useful for non-B0 rules too, like automatically mirroring / rotating the last generation to search for glide-symmetric or rotating patterns. Maybe that could be a useful feature to add to LLS itself, too? ;)
Yeah I've been working on this. The bit I was stuck on was the user input. What exactly should people write when they want a glider-reflect spaceship whose axis is an offset diagonal (like the gilder)? I think I'll imitate your script. EDIT: To be more precise: I was thinking of it as translate and then reflect, but it's much easier to think of it as reflect and then translate.
I'll try to add the same functionality to LLS (or just merge your script in, if that's okay with you).
Ps. Besides strobing backgrounds and glide symmetry, another feature that I'd kind of like to see in LLS would be exhaustive searching for all solutions. I believe that's something at least some SAT solvers can already do, and if not, it should be possible to kluge it: every time you find a solution, just append a constraint to the SAT solver input that says "nope, I don't want this solution" and restart the process. Repeat until the problem is unsatisfiable.
This is already a thing: -n. You can follow -n by a number if you only want that many solutions.
Of course, it would be more efficient to let the SAT solver itself do this, so that it can reuse any clauses it has learned in previous searches.
You would think that SAT solvers would come with the option to do this, but they don't seem to. Maybe something about how they work precludes it.
calcyman wrote:Is there a way to separate out the following phases, so they could be run separately?
I have no way of recovering the pattern RLE from this solution!
I'd mostly been using --save_dimacs for benchmarking, so I never needed to substitute back in! :lol:

I've just added this: Run

Code: Select all

./lls -b4 -i -p4 -x1 -y1 --save_dimacs --save_state
to save the DIMACS file (as lls_dimacs.cnf) and the state (as lls_state.pkl) then solve the cnf and save your solution in a file with this format:

Code: Select all

s SATISFIABLE
v -1 2 -3 -4 -5 6 7 8 9 -10 -11 -12 -13 14 -15 16 -17 -18 19 20 -21 -22 23 -24 -25 -26 -27 -28 -29 -30 -31 32 -33 34 -35 36 -37 -38 39 40 -41 -42 -43 -44 -45 -46 47 -48 -49 -50 -51 52 53 -54 55 56 -57 0
Then run

Code: Select all

./lls --substitute_solution lls_state.pkl solution
Hopefully that should all work and will produce a nice rle.
I ask because I've now created a program along the lines I was describing
Wow! Fast work!

rokicki
Posts: 80
Joined: August 6th, 2009, 12:26 pm

Re: Logic Life Search

Post by rokicki » February 3rd, 2018, 1:14 pm

I know minisat has an incremental "patch" (it's very tiny) that supports the inccnf format.
This format would let you pull multiple solutions out easily with reuse of the learned
clauses. I've found I can get thousands of solutions a second out of it . . .

User avatar
Macbi
Posts: 903
Joined: March 29th, 2009, 4:58 am

Re: Logic Life Search

Post by Macbi » February 3rd, 2018, 1:36 pm

rokicki wrote:I know minisat has an incremental "patch" (it's very tiny) that supports the inccnf format.
This format would let you pull multiple solutions out easily with reuse of the learned
clauses. I've found I can get thousands of solutions a second out of it . . .
Interesting! But inconvenient to add to LLS at the moment. I'll put it on my todo list for a future version.

User avatar
Rhombic
Posts: 1072
Joined: June 1st, 2013, 5:41 pm

Re: Logic Life Search

Post by Rhombic » February 4th, 2018, 1:26 pm

I made a script (with walkthrough for Python beginners) in which you input the minimum birth conditions and then the maximum birth conditions and it gives you the Macbi partial rule (pB/S) as required in LLS.
It is independent from Golly but I realised halfway through so I'll upload both versions (to be run from Golly or from outside of Golly).
Inputs in B/S format (not B_S or bs or BS)
To run outside of Golly:

Code: Select all

# rangetopartial.py (Rhombic, Feb 2018)
#
# This script is a quick tool to change a minimum rule and a maximum rule defining a range of rules to a partial rule.
# Partial rules are generated in Macbi's partial rule notation as supported by LLS.
# Example: B3acein4a/S23 - B3-y46ce/S23 gives pB3acein-y4a6-aikn/S23.
# pB/S denotes a partial rule
# The script is easily modified for a Golly-independent version.
#
# Heavily commented, intended as a walkthrough for people new to Python.

def strdel(string,pos):
    return (string[:pos]+string[pos+1:]) # Works just like del but for strings.
def strappend(string,pos,what):
    SR=(string[:pos+1]+what+string[pos+1:]) # Inserts a string into a string
    a=""
    for k in SR:
        a+=k
    return a

must=raw_input("Minimum rule:  ")+"/" # That last slash will help us not get out of the string length later...
can=raw_input("Maximum rule:  ")+"/" #...because I like to copy/paste and it's shorter than saying "if within the length"
ntc=[]
result="pB" # We'll keep adding stuff to this until we get the full rule.
ntcvals=["c","ce","aceikn","aceijknqry","aceijknqrtwyz","aceijknqry","aceikn","ce","c"] # Cheat list :)
for i in xrange(9): # We format strings so that B3acei7/S2a becomes B3acei7ce/S2a which simplifies matters later
    if str(i) in must:
        if must.index(str(i))<must.index("/"):
            if must[must.index(str(i))+1] in "012345678/":
                must=strappend(must,must.index(str(i)),ntcvals[i])
    if str(i) in can:
        if can.index(str(i))<can.index("/"):
            if can[can.index(str(i))+1] in "012345678/":
                can=strappend(can,can.index(str(i)),ntcvals[i])
if must == can: # Range of 1: endemic patterns
    g.show(must)
    g.exit()
for birth in xrange(9):
    if str(birth) in must: # Is there a 3 at all in the string?
        if must.index(str(birth))<must.index("/"): # Within births?
            result=result+str(birth)
            pos=must.index(str(birth))
            for n in xrange(len(must)):
                if must[pos+n+1] in "012345678/": # How long until next number or change to survival
                    until=pos+n+1
                    break
                else:
                    pass        
            ntc[:]=must[pos:pos+n+1] # This gives "3acei" or "3-cqry" for instance
            if ntc[1]=="-":
                negated=ntc[2:]
                overall=ntcvals[birth] # Now, get the total string for a given neighbour number and delete negated ntconditions
                for Condition in xrange(len(negated)):
                    overall=strdel(overall,overall.index(negated[Condition])) # Delete a given negated condition
                result=result+overall
            else:
                stated=ntc[1:] # This is a list so...
                overall=""
                for k in stated:
                    overall+=k # Concatenate elements into a string
                result=result+overall
    if str(birth) in can: # Better do this for each birth immediately after the "must" so that it is already ordered
        if can.index(str(birth))<can.index("/"):
            if str(birth) not in must:
                result=result+str(birth)
            elif must.index(str(birth))>must.index("/"):
                result=result+str(birth)
            pos=can.index(str(birth))
            for n in xrange(len(can)):
                if can[pos+n+1] in "012345678/":
                    until=pos+n+1
                    break
                else:
                    pass        
            ntc[:]=can[pos:pos+n+1]
            if ntc[1]=="-": # Crucial point!!! Before, we wanted no negated conditions. Now we want no stated conditions.
                negated=ntc[1:]
                overall=""
                for k in negated:
                    overall+=k
                result=result+overall
            else:
                stated=ntc[1:]
                overall=ntcvals[birth]
                for Condition in xrange(len(stated)):
                    overall=strdel(overall,overall.index(stated[Condition])) # Now we delete the ones we do have leaving the ones we do not have.
                if len(overall)>0: # Only put a minus sign if needed
                    result=result+"-"+overall # As we do NOT have the leftover ones, then we write the minus sign
# Let's be EXTRA CHEEKY. Instead of going crazy indexing the survival conditions, let's get rid of the birth ones.
must=must[must.index("/")+1:]
can=can[can.index("/")+1:]
result=result+"/S"
for i in xrange(9): # We format strings just like before but for survival conditions
    if str(i) in must:
        if must[must.index(str(i))+1] in "012345678/":
            must=strappend(must,must.index(str(i)),ntcvals[i])
    if str(i) in can:
        if can[can.index(str(i))+1] in "012345678/":
            can=strappend(can,can.index(str(i)),ntcvals[i])
            
for survival in xrange(9):
    if str(survival) in must: # Is there a 3 at all in the string?
        result=result+str(survival)
        pos=must.index(str(survival))
        for n in xrange(len(must)):
            if must[pos+n+1] in "012345678/": # How long until next number or change to survival
                until=pos+n+1
                break
            else:
                pass        
        ntc[:]=must[pos:pos+n+1] # This gives "3acei" or "3-cqry" for instance
        if ntc[1]=="-":
            negated=ntc[2:]
            overall=ntcvals[survival] # Now, get the total string for a given neighbour number and delete negated ntconditions
            for Condition in xrange(len(negated)):
                overall=strdel(overall,overall.index(negated[Condition])) # Delete a given negated condition
            result=result+overall
        else:
            stated=ntc[1:] # This is a list so...
            overall=""
            for k in stated:
                overall+=k # Concatenate elements into a string
            result=result+overall
    if str(survival) in can: # Better do this for each survival immediately after the "must" so that it is already ordered
        if str(survival) not in must:
            result=result+str(survival)
        pos=can.index(str(survival))
        for n in xrange(len(can)):
            if can[pos+n+1] in "012345678/": # You see? Here we do not go out of range because there is a "/" at the end!
                until=pos+n+1
                break
            else:
                pass        
        ntc[:]=can[pos:pos+n+1]
        if ntc[1]=="-": # Crucial point!!! Before, we wanted no negated conditions. Now we want no stated conditions.
            negated=ntc[1:]
            overall=""
            for k in negated:
                overall+=k
            result=result+overall
        else:
            stated=ntc[1:]
            overall=ntcvals[survival]
            for Condition in xrange(len(stated)):
                overall=strdel(overall,overall.index(stated[Condition])) # Now we delete the ones we do have leaving the ones we do not have.
            if len(overall)>0: # Only put a minus sign if needed
                result=result+"-"+overall # As we do NOT have the leftover ones, then we write the minus sign
print result
In Golly:

Code: Select all

# rangetopartial.py (Rhombic, Feb 2018)
#
# This script is a quick tool to change a minimum rule and a maximum rule defining a range of rules to a partial rule.
# Partial rules are generated in Macbi's partial rule notation as supported by LLS.
# Example: B3acein4a/S23 - B3-y46ce/S23 gives pB3acein-y4a6-aikn/S23.
# pB/S denotes a partial rule
# The script is easily modified for a Golly-independent version.
#
# Heavily commented, intended as a walkthrough for people new to Python.

import golly as g

def strdel(string,pos):
    return (string[:pos]+string[pos+1:]) # Works just like del but for strings.
def strappend(string,pos,what):
    SR=(string[:pos+1]+what+string[pos+1:]) # Inserts a string into a string
    a=""
    for k in SR:
        a+=k
    return a

must=g.getstring("Minimum rule:","")+"/" # That last slash will help us not get out of the string length later...
can=g.getstring("Maximum rule:","")+"/" #...because I like to copy/paste and it's shorter than saying "if within the length"
ntc=[]
result="pB" # We'll keep adding stuff to this until we get the full rule.
ntcvals=["c","ce","aceikn","aceijknqry","aceijknqrtwyz","aceijknqry","aceikn","ce","c"] # Cheat list :)
for i in xrange(9): # We format strings so that B3acei7/S2a becomes B3acei7ce/S2a which simplifies matters later
    if str(i) in must:
        if must.index(str(i))<must.index("/"):
            if must[must.index(str(i))+1] in "012345678/":
                must=strappend(must,must.index(str(i)),ntcvals[i])
    if str(i) in can:
        if can.index(str(i))<can.index("/"):
            if can[can.index(str(i))+1] in "012345678/":
                can=strappend(can,can.index(str(i)),ntcvals[i])
if must == can: # Range of 1: endemic patterns
    g.show(must)
    g.exit()
for birth in xrange(9):
    if str(birth) in must: # Is there a 3 at all in the string?
        if must.index(str(birth))<must.index("/"): # Within births?
            result=result+str(birth)
            pos=must.index(str(birth))
            for n in xrange(len(must)):
                if must[pos+n+1] in "012345678/": # How long until next number or change to survival
                    until=pos+n+1
                    break
                else:
                    pass        
            ntc[:]=must[pos:pos+n+1] # This gives "3acei" or "3-cqry" for instance
            if ntc[1]=="-":
                negated=ntc[2:]
                overall=ntcvals[birth] # Now, get the total string for a given neighbour number and delete negated ntconditions
                for Condition in xrange(len(negated)):
                    overall=strdel(overall,overall.index(negated[Condition])) # Delete a given negated condition
                result=result+overall
            else:
                stated=ntc[1:] # This is a list so...
                overall=""
                for k in stated:
                    overall+=k # Concatenate elements into a string
                result=result+overall
    if str(birth) in can: # Better do this for each birth immediately after the "must" so that it is already ordered
        if can.index(str(birth))<can.index("/"):
            if str(birth) not in must:
                result=result+str(birth)
            elif must.index(str(birth))>must.index("/"):
                result=result+str(birth)
            pos=can.index(str(birth))
            for n in xrange(len(can)):
                if can[pos+n+1] in "012345678/":
                    until=pos+n+1
                    break
                else:
                    pass        
            ntc[:]=can[pos:pos+n+1]
            if ntc[1]=="-": # Crucial point!!! Before, we wanted no negated conditions. Now we want no stated conditions.
                negated=ntc[1:]
                overall=""
                for k in negated:
                    overall+=k
                result=result+overall
            else:
                stated=ntc[1:]
                overall=ntcvals[birth]
                for Condition in xrange(len(stated)):
                    overall=strdel(overall,overall.index(stated[Condition])) # Now we delete the ones we do have leaving the ones we do not have.
                if len(overall)>0: # Only put a minus sign if needed
                    result=result+"-"+overall # As we do NOT have the leftover ones, then we write the minus sign
# Let's be EXTRA CHEEKY. Instead of going crazy indexing the survival conditions, let's get rid of the birth ones.
must=must[must.index("/")+1:]
can=can[can.index("/")+1:]
result=result+"/S"
for i in xrange(9): # We format strings just like before but for survival conditions
    if str(i) in must:
        if must[must.index(str(i))+1] in "012345678/":
            must=strappend(must,must.index(str(i)),ntcvals[i])
    if str(i) in can:
        if can[can.index(str(i))+1] in "012345678/":
            can=strappend(can,can.index(str(i)),ntcvals[i])
            
for survival in xrange(9):
    if str(survival) in must: # Is there a 3 at all in the string?
        result=result+str(survival)
        pos=must.index(str(survival))
        for n in xrange(len(must)):
            if must[pos+n+1] in "012345678/": # How long until next number or change to survival
                until=pos+n+1
                break
            else:
                pass        
        ntc[:]=must[pos:pos+n+1] # This gives "3acei" or "3-cqry" for instance
        if ntc[1]=="-":
            negated=ntc[2:]
            overall=ntcvals[survival] # Now, get the total string for a given neighbour number and delete negated ntconditions
            for Condition in xrange(len(negated)):
                overall=strdel(overall,overall.index(negated[Condition])) # Delete a given negated condition
            result=result+overall
        else:
            stated=ntc[1:] # This is a list so...
            overall=""
            for k in stated:
                overall+=k # Concatenate elements into a string
            result=result+overall
    if str(survival) in can: # Better do this for each survival immediately after the "must" so that it is already ordered
        if str(survival) not in must:
            result=result+str(survival)
        pos=can.index(str(survival))
        for n in xrange(len(can)):
            if can[pos+n+1] in "012345678/": # You see? Here we do not go out of range because there is a "/" at the end!
                until=pos+n+1
                break
            else:
                pass        
        ntc[:]=can[pos:pos+n+1]
        if ntc[1]=="-": # Crucial point!!! Before, we wanted no negated conditions. Now we want no stated conditions.
            negated=ntc[1:]
            overall=""
            for k in negated:
                overall+=k
            result=result+overall
        else:
            stated=ntc[1:]
            overall=ntcvals[survival]
            for Condition in xrange(len(stated)):
                overall=strdel(overall,overall.index(stated[Condition])) # Now we delete the ones we do have leaving the ones we do not have.
            if len(overall)>0: # Only put a minus sign if needed
                result=result+"-"+overall # As we do NOT have the leftover ones, then we write the minus sign
g.show(result)
EDIT: sorted bug
Last edited by Rhombic on February 5th, 2018, 8:09 pm, edited 1 time in total.
SoL : FreeElectronics : DeadlyEnemies : 6a-ite : Rule X3VI
what is “sesame oil”?

User avatar
Rhombic
Posts: 1072
Joined: June 1st, 2013, 5:41 pm

Re: Logic Life Search

Post by Rhombic » February 5th, 2018, 11:42 am

I grafted the script from yesterday with allrules.py to give a script that yields the Macbi partial rule for a given pattern (and number of generations):

Code: Select all

# partialrule.py
# allrules x rangetopartial
# Gives the partial rule for a given pattern.
# Grafted by Rhombic (Feb 2018).

import golly as g
from glife import validint
from string import replace

Hensel = [
    ['0'],
    ['1c', '1e'],
    ['2a', '2c', '2e', '2i', '2k', '2n'],
    ['3a', '3c', '3e', '3i', '3j', '3k', '3n', '3q', '3r', '3y'],
    ['4a', '4c', '4e', '4i', '4j', '4k', '4n', '4q', '4r', '4t', '4w', '4y', '4z'],
    ['5a', '5c', '5e', '5i', '5j', '5k', '5n', '5q', '5r', '5y'],
    ['6a', '6c', '6e', '6i', '6k', '6n'],
    ['7c', '7e'],
    ['8']
]

# Python versions < 2.4 don't have "sorted" built-in
try:
    sorted
except NameError:
    def sorted(inlist):
        outlist = list(inlist)
        outlist.sort()
        return outlist

# --------------------------------------------------------------------

def chunks(l, n):
    for i in range(0, len(l), n):
        yield l[i:i+n]

# --------------------------------------------------------------------

def rulestringopt(a):
    result = ''
    context = ''
    lastnum = ''
    lastcontext = ''
    for i in a:
        if i in 'BS':
            context = i
            result += i
        elif i in '012345678':
            if (i == lastnum) and (lastcontext == context):
                pass
            else:
                lastcontext = context
                lastnum = i
                result += i
        else:
            result += i
    result = replace(result, '4aceijknqrtwyz', '4')
    result = replace(result, '3aceijknqry', '3')
    result = replace(result, '5aceijknqry', '5')
    result = replace(result, '2aceikn', '2')
    result = replace(result, '6aceikn', '6')
    result = replace(result, '1ce', '1')
    result = replace(result, '7ce', '7')
    return result

clist = []
rule = g.getrule().split(':')[0]

fuzzer = rule + '9'
oldrule = rule
rule = ''
context = ''
deletefrom = []
for i in fuzzer:
    if i == '-':
        deletefrom = [x[1] for x in Hensel[int(context)]]
    elif i in '0123456789/S':
        if deletefrom:
            rule += ''.join(deletefrom)
            deletefrom = []
        context = i
    if len(deletefrom) == 0:
        rule += i
    elif i in deletefrom:
        deletefrom.remove(i)
rule = rule.strip('9')

if not (rule[0] == 'B' and '/S' in rule):
    g.exit('Please set Golly to a Life-like rule.')

if g.empty():
    g.exit('The pattern is empty.')

s = g.getstring('Enter the period:', '', 'Rules calculator')
if not validint(s):
    g.exit('Bad number: %s' % s)

numsteps = int(s)
if numsteps < 1:
    g.exit('Period must be at least 1.')

g.select(g.getrect())
g.copy()
s = int(s)

for i in range(0,s):
    g.run(1)
    clist.append(list(chunks(g.getcells(g.getrect()), 2)))
    mcc = min(clist[i])
    clist[i] = [[x[0] - mcc[0], x[1] - mcc[1]] for x in clist[i]]

g.show('Processing...')

ruleArr = rule.split('/')
ruleArr[0] = ruleArr[0].lstrip('B')
ruleArr[1] = ruleArr[1].lstrip('S')

b_need = []
b_OK = []
s_need = []
s_OK = []

context = ''
fuzzed = ruleArr[0] + '9'
for i in fuzzed:
    if i in '0123456789':
        if len(context) == 1:
            b_need += Hensel[int(context)]
            b_OK += Hensel[int(context)]
        context = i
    elif context != '':
        b_need.append(context[0] + i)
        b_OK.append(context[0] + i)
        context += context[0]
context = ''
fuzzed = ruleArr[1] + '9'
for i in fuzzed:
    if i in '0123456789':
        if len(context) == 1:
            s_need += Hensel[int(context)]
            s_OK += Hensel[int(context)]
        context = i
    elif context != '':
        s_need.append(context[0] + i)
        s_OK.append(context[0] + i)
        context += context[0]

for i in [iter2 for iter1 in Hensel for iter2 in iter1]:
    if not i in b_OK:
        b_OK.append(i)
        execfor = 1
        # B0 and nontotalistic rulestrings are mutually exclusive
        try:
            g.setrule(rulestringopt('B' + ''.join(b_OK) + '/S' + ruleArr[1]))
        except:
            b_OK.remove(i)
            execfor = 0
        for j in range(0, s * execfor):
            g.run(1)
            try:
                dlist = list(chunks(g.getcells(g.getrect()), 2))
                mcc = min(dlist)
                dlist = [[x[0] - mcc[0], x[1] - mcc[1]] for x in dlist]
                if not(clist[j] == dlist):
                    b_OK.remove(i)
                    break
            except:
                b_OK.remove(i)
                break
        g.new('')
        g.paste(0, 0, 'or')
        g.select(g.getrect())
        b_OK.sort()

    if not i in s_OK:
        s_OK.append(i)
        execfor = 1
        # B0 and nontotalistic rulestrings are mutually exclusive
        try:
            g.setrule(rulestringopt('B' + ruleArr[0] + '/S' + ''.join(s_OK)))
        except:
            s_OK.remove(i)
            execfor = 0
        for j in range(0, s * execfor):
            g.run(1)
            try:
                dlist = list(chunks(g.getcells(g.getrect()), 2))
                mcc = min(dlist)
                dlist = [[x[0] - mcc[0], x[1] - mcc[1]] for x in dlist]
                if not(clist[j] == dlist):
                    s_OK.remove(i)
                    break
            except:
                s_OK.remove(i)
                break
        g.new('')
        g.paste(0, 0, 'or')
        g.select(g.getrect())
        s_OK.sort()

    if i in b_need:
        b_need.remove(i)
        g.setrule(rulestringopt('B' + ''.join(b_need) + '/S' + ruleArr[1]))
        for j in range(0, s):
            g.run(1)
            try:
                dlist = list(chunks(g.getcells(g.getrect()), 2))
                mcc = min(dlist)
                dlist = [[x[0] - mcc[0], x[1] - mcc[1]] for x in dlist]
                if not(clist[j] == dlist):
                    b_need.append(i)
                    break
            except:
                b_need.append(i)
                break
        g.new('')
        g.paste(0, 0, 'or')
        g.select(g.getrect())
        b_need.sort()

    if i in s_need:
        s_need.remove(i)
        g.setrule(rulestringopt('B' + ruleArr[0] + '/S' + ''.join(s_need)))
        for j in range(0, s):
            g.run(1)
            try:
                dlist = list(chunks(g.getcells(g.getrect()), 2))
                mcc = min(dlist)
                dlist = [[x[0] - mcc[0], x[1] - mcc[1]] for x in dlist]
                if not(clist[j] == dlist):
                    s_need.append(i)
                    break
            except:
                s_need.append(i)
                break
        g.new('')
        g.paste(0, 0, 'or')
        g.select(g.getrect())
        s_need.sort()

g.setrule(oldrule)
ruleres = 'B' + ''.join(sorted(b_need)) + '/S' + ''.join(sorted(s_need)) + \
    ' - B' + ''.join(sorted(b_OK)) + '/S' + ''.join(sorted(s_OK))
ruleres = rulestringopt(ruleres)
g.show(ruleres) 

def strdel(string,pos):
    return (string[:pos]+string[pos+1:]) # Works just like del but for strings.
def strappend(string,pos,what):
    SR=(string[:pos+1]+what+string[pos+1:]) # Inserts a string into a string
    a=""
    for k in SR:
        a+=k
    return a
# OPTIMISE RULES FIRST by setting and copying
must=rulestringopt('B' + ''.join(sorted(b_need)) + '/S' + ''.join(sorted(s_need)))+"/" # That last slash will help us not get out of the string length later...
can=rulestringopt('B' + ''.join(sorted(b_OK)) + '/S' + ''.join(sorted(s_OK)))+"/" #...because I like to copy/paste and it's shorter than saying "if within the length"
ntc=[]
result="pB" # We'll keep adding stuff to this until we get the full rule.
ntcvals=["c","ce","aceikn","aceijknqry","aceijknqrtwyz","aceijknqry","aceikn","ce","c"] # Cheat list :)
for i in xrange(9): # We format strings so that B3acei7/S2a becomes B3acei7ce/S2a which simplifies matters later
    if str(i) in must:
        if must.index(str(i))<must.index("/"):
            if must[must.index(str(i))+1] in "012345678/":
                must=strappend(must,must.index(str(i)),ntcvals[i])
    if str(i) in can:
        if can.index(str(i))<can.index("/"):
            if can[can.index(str(i))+1] in "012345678/":
                can=strappend(can,can.index(str(i)),ntcvals[i])
if must == can: # Range of 1: endemic patterns
    g.show(must)
    g.exit()
for birth in xrange(9):
    if str(birth) in must: # Is there a 3 at all in the string?
        if must.index(str(birth))<must.index("/"): # Within births?
            result=result+str(birth)
            pos=must.index(str(birth))
            for n in xrange(len(must)):
                if must[pos+n+1] in "012345678/": # How long until next number or change to survival
                    until=pos+n+1
                    break
                else:
                    pass        
            ntc[:]=must[pos:pos+n+1] # This gives "3acei" or "3-cqry" for instance
            if ntc[1]=="-":
                negated=ntc[2:]
                overall=ntcvals[birth] # Now, get the total string for a given neighbour number and delete negated ntconditions
                for Condition in xrange(len(negated)):
                    overall=strdel(overall,overall.index(negated[Condition])) # Delete a given negated condition
                result=result+overall
            else:
                stated=ntc[1:] # This is a list so...
                overall=""
                for k in stated:
                    overall+=k # Concatenate elements into a string
                result=result+overall
    if str(birth) in can: # Better do this for each birth immediately after the "must" so that it is already ordered
        if can.index(str(birth))<can.index("/"):
            if str(birth) not in must:
                result=result+str(birth)
            elif must.index(str(birth))>must.index("/"):
                result=result+str(birth)
            pos=can.index(str(birth))
            for n in xrange(len(can)):
                if can[pos+n+1] in "012345678/":
                    until=pos+n+1
                    break
                else:
                    pass        
            ntc[:]=can[pos:pos+n+1]
            if ntc[1]=="-": # Crucial point!!! Before, we wanted no negated conditions. Now we want no stated conditions.
                negated=ntc[1:]
                overall=""
                for k in negated:
                    overall+=k
                result=result+overall
            else:
                stated=ntc[1:]
                overall=ntcvals[birth]
                for Condition in xrange(len(stated)):
                    overall=strdel(overall,overall.index(stated[Condition])) # Now we delete the ones we do have leaving the ones we do not have.
                if len(overall)>0: # Only put a minus sign if needed
                    result=result+"-"+overall # As we do NOT have the leftover ones, then we write the minus sign
# Let's be EXTRA CHEEKY. Instead of going crazy indexing the survival conditions, let's get rid of the birth ones.
must=must[must.index("/")+1:]
can=can[can.index("/")+1:]
result=result+"/S"
for i in xrange(9): # We format strings just like before but for survival conditions
    if str(i) in must:
        if must[must.index(str(i))+1] in "012345678/":
            must=strappend(must,must.index(str(i)),ntcvals[i])
    if str(i) in can:
        if can[can.index(str(i))+1] in "012345678/":
            can=strappend(can,can.index(str(i)),ntcvals[i])
            
for survival in xrange(9):
    if str(survival) in must: # Is there a 3 at all in the string?
        result=result+str(survival)
        pos=must.index(str(survival))
        for n in xrange(len(must)):
            if must[pos+n+1] in "012345678/": # How long until next number or change to survival
                until=pos+n+1
                break
            else:
                pass        
        ntc[:]=must[pos:pos+n+1] # This gives "3acei" or "3-cqry" for instance
        if ntc[1]=="-":
            negated=ntc[2:]
            overall=ntcvals[survival] # Now, get the total string for a given neighbour number and delete negated ntconditions
            for Condition in xrange(len(negated)):
                overall=strdel(overall,overall.index(negated[Condition])) # Delete a given negated condition
            result=result+overall
        else:
            stated=ntc[1:] # This is a list so...
            overall=""
            for k in stated:
                overall+=k # Concatenate elements into a string
            result=result+overall
    if str(survival) in can: # Better do this for each survival immediately after the "must" so that it is already ordered
        if str(survival) not in must:
            result=result+str(survival)
        pos=can.index(str(survival))
        for n in xrange(len(can)):
            if can[pos+n+1] in "012345678/": # You see? Here we do not go out of range because there is a "/" at the end!
                until=pos+n+1
                break
            else:
                pass        
        ntc[:]=can[pos:pos+n+1]
        if ntc[1]=="-": # Crucial point!!! Before, we wanted no negated conditions. Now we want no stated conditions.
            negated=ntc[1:]
            overall=""
            for k in negated:
                overall+=k
            result=result+overall
        else:
            stated=ntc[1:]
            overall=ntcvals[survival]
            for Condition in xrange(len(stated)):
                overall=strdel(overall,overall.index(stated[Condition])) # Now we delete the ones we do have leaving the ones we do not have.
            if len(overall)>0: # Only put a minus sign if needed
                result=result+"-"+overall # As we do NOT have the leftover ones, then we write the minus sign
g.show(result)
# g.setclipstr(result)
This should help with selecting specific rulespaces.
Last edited by Rhombic on February 5th, 2018, 8:10 pm, edited 1 time in total.
SoL : FreeElectronics : DeadlyEnemies : 6a-ite : Rule X3VI
what is “sesame oil”?

rokicki
Posts: 80
Joined: August 6th, 2009, 12:26 pm

Re: Logic Life Search

Post by rokicki » February 5th, 2018, 2:35 pm

picosat has a --all option that finds all solutions, and picosat appears to perform reasonably well (definitely slower than minisat or glucose but not too far off, and the --all option quickly makes up for the delta when you want to see all the solutions).

Integrating usage of solvers with --all options should be quick.

wildmyron
Posts: 1542
Joined: August 9th, 2013, 12:45 am
Location: Western Australia

Re: Logic Life Search

Post by wildmyron » February 6th, 2018, 5:51 am

Thanks for pointing out the develop branch, and thank you also for the recent additions to lls. Having optimisation off has made it easier to correlate which variables correspond to which cells in the search pattern and so I've been able to try out a few ideas.

A very useful feature of WLS to reduce search times is to require at least one cell to be On in a given row or column. This means that searches don't repeat searching the partial solution space with extra blank rows padding the front of the search. For spaceship searches it is ideal to require an On cell in the front-most column (of Gen 0) that is allowed to have On cells (for spaceships with non-zero x displacement). JLS is missing this feature and so requires manual setting of a cell in the front column to prevent it from searching through solutions with large empty spaces. It is also possible to mitigate this issue in WLS by using a trying order which tries On cells first, but this often leads to much larger partials than necessary being searched through at the beginning of the search. Whichever trying order is used however, forcing a cell On in a column at the front restricts the search space without excluding possible solutions (although if other constraints are imposed then a solution may be missed).

With this idea in mind I tried a test with lls searching for the Turtle in CGoL. I used the following command to create a cnf file:

Code: Select all

$ python lls -r B3S23 -i -p3 -x0 -y1 -b w h -s "D2|" --dry_run --save_dimacs
where 'w' and 'h' are bbox parameters as listed in the table below. I then timed glucose-syrup-v4.0 with these files and also with modified cnf files. The modification I made was to replace the clause generated by the '-i' option with one which required a cell in the last row to be On. E.g for "-b 10 10" I used the clause "41 42 43 44 45 0".

Turtle search timing results (all times in s, average of 3 runs)

Code: Select all

bbox    |   default |   front row
10x10   |     0.8   |     0.7
10x20   |     3.5   |     1.3
10x30   |     4.8   |     1.8
10x40   |    27.7   |     2.4
12x10   |     3.2   |     1.0
12x20 * |     4.2   |    12.7 !
12x30 * |     6.9   |     2.4
12x40 * |   112     |     7.6
Test cases marked with * have at least one solution. I don't know why glucose tripped up on the modified 12x20 search, but the rest of the results show a promising improvement. Of course, this is a contrived test case, but I think it's worth adding a feature to lls to implement this kind of constraint.

I think it would be most useful for spaceship searches, but there's potentially also benefit for oscillator searches.
The 5S project (Smallest Spaceships Supporting Specific Speeds) is now maintained by AforAmpere. The latest collection is hosted on GitHub and contains well over 1,000,000 spaceships.

Semi-active here - recovering from a severe case of LWTDS.

User avatar
Macbi
Posts: 903
Joined: March 29th, 2009, 4:58 am

Re: Logic Life Search

Post by Macbi » February 6th, 2018, 6:48 am

rokicki wrote:picosat has a --all option that finds all solutions, and picosat appears to perform reasonably well (definitely slower than minisat or glucose but not too far off, and the --all option quickly makes up for the delta when you want to see all the solutions).
wildmyron wrote:A very useful feature of WLS to reduce search times is to require at least one cell to be On in a given row or column.
These are both great suggestions, thanks so much! I'll definitely implement them, but it might take a while. Are there any other features of WLS that LLS doesn't yet match?
wildmyron wrote:Having optimisation off has made it easier to correlate which variables correspond to which cells in the search pattern and so I've been able to try out a few ideas.
If you run LLS with --save_state it now saves a copy of which variables are being used for what, as a python pickle file. To see them run

Code: Select all

>python
>import pickle
>(grid, ignore_transition, rule, correspondence) = pickle.load(open("lls_state.pkl","r"))
then "grid" says which variables are in which cell, "ignore_transition" says whether LLS is ignoring the transition for that cell, "rule" specifies the rule and "correspondence" says which DIMACS variables are being used for which LLS variables.

wildmyron
Posts: 1542
Joined: August 9th, 2013, 12:45 am
Location: Western Australia

Re: Logic Life Search

Post by wildmyron » February 6th, 2018, 12:03 pm

Macbi wrote:<snip "all solutions" suggestion>
wildmyron wrote:A very useful feature of WLS to reduce search times is to require at least one cell to be On in a given row or column.
These are both great suggestions, thanks so much! I'll definitely implement them, but it might take a while.
Look forward to it, when you can.
Macbi wrote:Are there any other features of WLS that LLS doesn't yet match?
There are a few other constraints, similar to JLS' constraints on population in layers. They basically allow you to restrict the population in each row. I can't remember exactly what's in JLS and what's in WLS right now - I'll have a look tomorrow. I do think think these would be quite a bit more complicated to implement though. There's also Nicolay Beluchenko's version of WLS which implements a form of hashing of solutions so it doesn't output multiple copies of the same solution translated to different places in the grid. It is also able to automatically backtrack when a disconnected solution is found - so you don't get a result with lots of non-interacting parts. There's some discussion of that somewhere on the forum. I don't imagine that's at all amenable to being expressed as a logical formula though.
Macbi wrote:
wildmyron wrote:Having optimisation off has made it easier to correlate which variables correspond to which cells in the search pattern and so I've been able to try out a few ideas.
If you run LLS with --save_state it now saves a copy of which variables are being used for what, as a python pickle file. To see them run

Code: Select all

>python
>import pickle
>(grid, ignore_transition, rule, correspondence) = pickle.load(open("lls_state.pkl","r"))
then "grid" says which variables are in which cell, "ignore_transition" says whether LLS is ignoring the transition for that cell, "rule" specifies the rule and "correspondence" says which DIMACS variables are being used for which LLS variables.
Thanks. I've used the --save-state option and wondered about the objects stashed in there, but hadn't worked out what they corresponded to precisely yet. I've noticed that without optimisation the final search pattern is not output anywhere (even with -v3). This is what's stored in the "grid" variable I believe. I'll take a closer look at that. Thanks again.
The 5S project (Smallest Spaceships Supporting Specific Speeds) is now maintained by AforAmpere. The latest collection is hosted on GitHub and contains well over 1,000,000 spaceships.

Semi-active here - recovering from a severe case of LWTDS.

User avatar
Macbi
Posts: 903
Joined: March 29th, 2009, 4:58 am

Re: Logic Life Search

Post by Macbi » February 6th, 2018, 12:36 pm

wildmyron wrote:There are a few other constraints, similar to JLS' constraints on population in layers. They basically allow you to restrict the population in each row. I can't remember exactly what's in JLS and what's in WLS right now - I'll have a look tomorrow. I do think think these would be quite a bit more complicated to implement though.
This sounds doable, depending on the details.
There's also Nicolay Beluchenko's version of WLS which implements a form of hashing of solutions so it doesn't output multiple copies of the same solution translated to different places in the grid.
This is also super doable. At the moment once one solution is found I add a clause to rule it out. So instead I could just consider all its translations and add a clause for each of them.

There's also a more principled way of doing it where you add clauses at the start saying that any solution has to be lexicographically first amongst all of its translations, reflections, rotations and phases. This would not only cut down on repeated solutions, it would also speed up the search since the solver would effectively be searching a much smaller space (for example you might expect a search for a period 19 oscillator to become faster by a factor of (8 rotations and reflections * 19 phases) = 162). The problem is that LLS has to know all the possible transformations that could apply. So either the user has to laboriously spell them out, or LLS has to have some clever subroutine that spots them.
It is also able to automatically backtrack when a disconnected solution is found - so you don't get a result with lots of non-interacting parts. There's some discussion of that somewhere on the forum. I don't imagine that's at all amenable to being expressed as a logical formula though.
There's a polynomial-sized set of clauses here that capture the notion of connectedness. But I think in practice there would be too many of them to be practical. Maybe there's an obscure paper somewhere with a quick way to do it.
I've noticed that without optimisation the final search pattern is not output anywhere (even with -v3).
That's a bug and will be fixed.

User avatar
Rhombic
Posts: 1072
Joined: June 1st, 2013, 5:41 pm

Re: Logic Life Search

Post by Rhombic » February 7th, 2018, 7:13 am

How do you get the partial results from LLS? Are they saved somewhere?
SoL : FreeElectronics : DeadlyEnemies : 6a-ite : Rule X3VI
what is “sesame oil”?

User avatar
Macbi
Posts: 903
Joined: March 29th, 2009, 4:58 am

Re: Logic Life Search

Post by Macbi » February 7th, 2018, 7:17 am

Rhombic wrote:How do you get the partial results from LLS? Are they saved somewhere?
I don't know what you mean. LLS doesn't produce partial results.

I think in the 5S thread someone posted that they had found a partial with LLS, but they must have done a custom search which was actually designed to find the front of a ship.

wildmyron
Posts: 1542
Joined: August 9th, 2013, 12:45 am
Location: Western Australia

Re: Logic Life Search

Post by wildmyron » February 7th, 2018, 8:19 am

Macbi wrote:
Rhombic wrote:How do you get the partial results from LLS? Are they saved somewhere?
I don't know what you mean. LLS doesn't produce partial results.

I think in the 5S thread someone posted that they had found a partial with LLS, but they must have done a custom search which was actually designed to find the front of a ship.
That's correct. I used @vyznev's make_lls_grid.py script to generate a search pattern, then manually imposed bilateral symmetry and replaced two columns of 0 cells behind the pattern in each generation with *' cells. I then generated the dimacs file and added a clause to force a cell on in the front row of the pattern. This was necessary to get anything useful out of the SAT solver, without it I'd just get solutions with a single cell On. Then I ran the solver and used the substitute_solution option in LLS to get the result out.

I realise now I could have done something similar just with LLS, but it was more of an exploration of the idea and I wasn't sure exactly what the search pattern should look like when I started.
The 5S project (Smallest Spaceships Supporting Specific Speeds) is now maintained by AforAmpere. The latest collection is hosted on GitHub and contains well over 1,000,000 spaceships.

Semi-active here - recovering from a severe case of LWTDS.

User avatar
Majestas32
Posts: 549
Joined: November 20th, 2017, 12:22 pm
Location: 'Merica

Re: Logic Life Search

Post by Majestas32 » February 10th, 2018, 6:08 pm

So I have a search pattern "reflection" that is supposed to find a 2c/7 like this:

Code: Select all

0,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,1,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,0,0,0,0,0
0,0,0,1,0,1,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
But there is a clear example:

Code: Select all

x = 4, y = 1, rule = B2c3-e/S1e2-a3
2obo!
But LLS says

Code: Select all

$ ./lls -r pB2c-a345678/S012345678 reflection -S lingeling

Getting search pattern...
Done

Preprocessing...
    Unsatisfiability proved in preprocessing
Done

Time taken: 0 seconds

Unsatisfiable

What am I doing wrong?
Searching:
b2-a5k6n7cs12-i3ij4k5j8
b2-a3c7cs12-i

Currently looking for help searching these rules.

User avatar
Macbi
Posts: 903
Joined: March 29th, 2009, 4:58 am

Re: Logic Life Search

Post by Macbi » February 10th, 2018, 6:12 pm

Majestas32 wrote:So I have a search pattern "reflection" that is supposed to find a 2c/7 like this:

Code: Select all

0,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,1,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,0,0,0,0,0
0,0,0,1,0,1,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
But there is a clear example:

Code: Select all

x = 4, y = 1, rule = B2c3-e/S1e2-a3
2obo!
But LLS says

Code: Select all

$ ./lls -r pB2c-a345678/S012345678 reflection -S lingeling

Getting search pattern...
Done

Preprocessing...
    Unsatisfiability proved in preprocessing
Done

Time taken: 0 seconds

Unsatisfiable

What am I doing wrong?
Could you run it in -v3 mode and post the output?

User avatar
Majestas32
Posts: 549
Joined: November 20th, 2017, 12:22 pm
Location: 'Merica

Re: Logic Life Search

Post by Majestas32 » February 10th, 2018, 6:15 pm

Code: Select all

$ ./lls -r pB2c-a345678/S012345678 reflection -S lingeling -v3

Getting search pattern...
    Creating search pattern from file "reflection" ...
        Reading file "reflection" ...
        Done

        Parsing input pattern...
        Done

        Pattern parsed as:
        0,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,1,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,0,0,0,0,0

        0,0,0,1,0,1,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

    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


Searching:
b2-a5k6n7cs12-i3ij4k5j8
b2-a3c7cs12-i

Currently looking for help searching these rules.

User avatar
Macbi
Posts: 903
Joined: March 29th, 2009, 4:58 am

Re: Logic Life Search

Post by Macbi » February 10th, 2018, 6:23 pm

Majestas32 wrote:

Code: Select all

$ ./lls -r pB2c-a345678/S012345678 reflection -S lingeling -v3

Getting search pattern...
    Creating search pattern from file "reflection" ...
        Reading file "reflection" ...
        Done

        Parsing input pattern...
        Done

        Pattern parsed as:
        0,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,1,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,0,0,0,0,0

        0,0,0,1,0,1,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

    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


You've got the same problem that someone else had earlier in the thread of LLS reading files wrongly on Windows. You cam fix this by downloading the most recent version of LLS from the develop brach on GitHub.

User avatar
Majestas32
Posts: 549
Joined: November 20th, 2017, 12:22 pm
Location: 'Merica

Re: Logic Life Search

Post by Majestas32 » February 10th, 2018, 6:25 pm

Ahh
Searching:
b2-a5k6n7cs12-i3ij4k5j8
b2-a3c7cs12-i

Currently looking for help searching these rules.

User avatar
Rhombic
Posts: 1072
Joined: June 1st, 2013, 5:41 pm

Re: Logic Life Search

Post by Rhombic » February 27th, 2018, 7:42 am

LLS seems to struggle with the following input:

Code: Select all

0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 
0 0 0 0 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 1 1 1 1 1 0 0 0 0 0 
0 0 0 0 0 0 0 0 1 0 0 0 1 0 0 0 0 0 
0 0 0 0 0 0 0 1 1 0 1 0 1 1 0 0 0 0 
0 0 0 0 0 0 0 0 1 0 0 0 1 0 0 0 0 0 
0 0 0 0 0 0 0 0 1 1 1 1 1 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 1 0 0 0 0 0 0 0 0 0 
0 0 0 0 0 0 1 1 1 1 1 0 0 0 0 0 0 0 
0 0 0 0 0 0 1 0 0 0 1 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 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 0 0 
0 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 0 
0 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40 x41 x42 x43 x44 x45 0 
0 x46 x47 x48 x49 x50 x51 x52 x53 x54 x55 x56 x57 x58 x59 x60 x61 0 
0 x62 x63 x64 x65 x66 x67 x68 x69 x70 x71 x72 x73 x74 x75 x76 x77 0 
0 x78 x79 x80 x81 x82 x83 x84 x85 x86 x87 x88 x89 x90 x91 x92 x93 0 
0 0 x94 x95 x96 x97 x98 x99 x100 x101 x102 x103 x104 x105 x106 x107 0 0 
0 0 x108 x109 x110 x111 x112 x113 x114 x115 x116 x117 x118 x119 x120 x121 0 0 
0 0 x122 x123 x124 x125 x126 x127 x128 x129 x130 x131 x132 x133 x134 0 0 0 
0 0 0 x135 x136 x137 x138 x139 x140 x141 x142 x143 x144 x145 0 0 0 0 
0 0 0 0 0 x146 x147 x148 x149 x150 x151 x152 x153 0 0 0 0 0 
0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0

0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 
0 0 0 0 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 1 1 1 1 1 0 0 0 0 0 
0 0 0 0 0 0 0 0 1 0 0 0 1 0 0 0 0 0 
0 0 0 0 0 0 0 1 1 0 1 0 1 1 0 0 0 0 
0 0 0 0 0 0 0 0 1 0 0 0 1 0 0 0 0 0 
0 0 0 0 0 0 0 0 1 1 1 1 1 0 0 0 0 0 
0 0 0 0 0 0 0 1 0 0 1 0 0 0 0 0 0 0 
0 0 0 0 0 0 0 0 1 0 0 1 0 0 0 0 0 0 
0 0 0 0 0 0 1 1 1 1 1 0 0 0 0 0 0 0 
0 0 0 0 0 0 1 0 0 0 1 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 * * * * * * * * * * * * * * * * 0 
0 * * * * * * * * * * * * * * * * 0  
0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 

0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 
0 0 0 0 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 1 1 1 1 1 0 0 0 0 0 
0 0 0 0 0 0 0 0 1 0 0 0 1 0 0 0 0 0 
0 0 0 0 0 0 0 1 1 0 1 0 1 1 0 0 0 0 
0 0 0 0 0 0 0 0 1 0 0 0 1 0 0 0 0 0 
0 0 0 0 0 0 0 0 1 1 1 1 1 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 1 0 0 0 0 0 0 
0 0 0 0 0 0 1 1 1 1 1 0 0 0 0 0 0 0 
0 0 0 0 0 0 1 0 0 0 1 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 * * * * * * * * * * * * * * * * 0 
0 * * * * * * * * * * * * * * * * 0  
0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0

0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 
0 0 0 0 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 1 1 1 1 1 0 0 0 0 0 
0 0 0 0 0 0 0 0 1 0 0 0 1 0 0 0 0 0 
0 0 0 0 0 0 0 1 1 0 1 0 1 1 0 0 0 0 
0 0 0 0 0 0 0 0 1 0 0 0 1 0 0 0 0 0 
0 0 0 0 0 0 0 0 1 0 0 0 1 0 0 0 0 0 
0 0 0 0 0 0 0 0 0 1 1 1 0 0 0 0 0 0 
0 0 0 0 0 0 0 1 1 1 0 0 0 0 0 0 0 0 
0 0 0 0 0 0 1 0 0 0 1 0 0 0 0 0 0 0 
0 0 0 0 0 0 1 0 0 0 1 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 * * * * * * * * * * * * * * * * 0 
0 * * * * * * * * * * * * * * * * 0  
0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0

0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 
0 0 0 0 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 1 1 1 1 1 0 0 0 0 0 
0 0 0 0 0 0 0 0 1 0 0 0 1 0 0 0 0 0 
0 0 0 0 0 0 0 1 1 0 1 0 1 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 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 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 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 * * * * * * * * * * * * * * * * 0 
0 * * * * * * * * * * * * * * * * 0  
0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0

0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 
0 0 0 0 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 1 1 1 1 1 0 0 0 0 0 
0 0 0 0 0 0 0 0 1 0 0 0 1 0 0 0 0 0 
0 0 0 0 0 0 0 1 1 0 1 0 1 1 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 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 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 
0 0 0 0 0 0 0 1 1 1 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 * * * * * * * * * * * * * * * * 0 
0 * * * * * * * * * * * * * * * * 0  
0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0

0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 
0 0 0 0 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 1 1 1 1 1 0 0 0 0 0 
0 0 0 0 0 0 0 0 1 0 0 0 1 0 0 0 0 0 
0 0 0 0 0 0 0 1 1 0 0 0 1 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 0 0 0 0 0 0 0 0 0 0 0 0 
0 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 1 1 0 0 0 0 0 0 0 0 
0 0 0 0 0 0 0 1 0 1 0 0 0 0 0 0 0 0 
0 0 0 0 0 0 0 1 1 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 
0 * * * * * * * * * * * * * * * * 0  
0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0

0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 
0 0 0 0 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 1 1 1 1 1 0 0 0 0 0 
0 0 0 0 0 0 0 0 1 0 1 0 1 0 0 0 0 0 
0 0 0 0 0 0 0 1 1 0 0 0 1 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 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 1 1 1 0 0 0 0 0 0 0 0 
0 0 0 0 0 0 1 1 1 1 1 0 0 0 0 0 0 0 
0 0 0 0 0 0 0 1 1 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 * * * * * * * * * * * * * * * * 0 
0 * * * * * * * * * * * * * * * * 0  
0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0

0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 
0 0 0 0 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 1 1 0 1 1 0 0 0 0 0 
0 0 0 0 0 0 0 0 1 0 1 0 1 0 0 0 0 0 
0 0 0 0 0 0 0 1 1 0 0 0 1 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 0 0 0 0 0 0 0 0 0 0 0 0 
0 0 0 0 0 0 0 1 1 1 0 0 0 0 0 0 0 0 
0 0 0 0 0 0 1 1 0 1 1 0 0 0 0 0 0 0 
0 0 0 0 0 0 1 0 0 0 1 0 0 0 0 0 0 0 
0 0 0 0 0 0 1 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 * * * * * * * * * * * * * * * * 0  
0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0

0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 
0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 
0 0 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 1 0 0 0 0 0 
0 0 0 0 0 0 0 0 1 0 0 0 1 0 0 0 0 0 
0 0 0 0 0 0 0 1 1 0 0 0 1 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 0 0 1 0 0 0 0 0 0 0 0 0 
0 0 0 0 0 0 1 1 1 1 1 0 0 0 0 0 0 0 
0 0 0 0 0 0 1 0 0 0 1 0 0 0 0 0 0 0 
0 0 0 0 0 1 0 0 1 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  
0 * * * * * * * * * * * * * * * * 0 
0 * * * * * * * * * * * * * * * * 0 
0 * * * * * * * * * * * * * * * * 0 
0 * * * * * * * * * * * * * * * * 0 
0 * * * * * * * * * * * * * * * * 0 
0 * * * * * * * * * * * * * * * * 0  
0 * * * * * * * * * * * * * * * * 0 
0 * * * * * * * * * * * * * * * * 0 
0 * * * * * * * * * * * * * * * * 0  
0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0

0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 
0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 
0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 
0 0 0 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 1 0 0 0 0 0 0 
0 0 0 0 0 0 0 1 1 0 0 0 1 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 0 0 1 0 0 0 0 0 0 0 0 0 
0 0 0 0 0 0 1 1 1 1 1 0 0 0 0 0 0 0 
0 0 0 0 0 0 1 0 0 0 1 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 * * * * * * * * * * * * * * * * 0 
0 * * * * * * * * * * * * * * * * 0  
0 * * * * * * * * * * * * * * * * 0 
0 * * * * * * * * * * * * * * * * 0 
0 * * * * * * * * * * * * * * * * 0 
0 * * * * * * * * * * * * * * * * 0 
0 * * * * * * * * * * * * * * * * 0 
0 * * * * * * * * * * * * * * * * 0  
0 * * * * * * * * * * * * * * * * 0 
0 * * * * * * * * * * * * * * * * 0 
0 * * * * * * * * * * * * * * * * 0  
0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0

0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 
0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 
0 0 0 0 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 1 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 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 
0 0 0 0 0 0 1 1 1 1 1 0 0 0 0 0 0 0 
0 0 0 0 0 0 1 0 0 0 1 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 * * * * * * * * * * * * * * * * 0 
0 * * * * * * * * * * * * * * * * 0  
0 * * * * * * * * * * * * * * * * 0 
0 * * * * * * * * * * * * * * * * 0 
0 * * * * * * * * * * * * * * * * 0 
0 * * * * * * * * * * * * * * * * 0 
0 * * * * * * * * * * * * * * * * 0 
0 * * * * * * * * * * * * * * * * 0  
0 * * * * * * * * * * * * * * * * 0 
0 * * * * * * * * * * * * * * * * 0 
0 * * * * * * * * * * * * * * * * 0  
0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0

0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 
0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 
0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 
0 0 0 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 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 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 1 1 1 1 1 0 0 0 0 0 0 0 
0 0 0 0 0 0 1 0 0 0 1 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 * * * * * * * * * * * * * * * * 0 
0 * * * * * * * * * * * * * * * * 0 
0 * * * * * * * * * * * * * * * * 0  
0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0

0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 
0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 
0 0 0 0 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 1 1 1 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 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 
0 0 0 0 0 0 1 1 1 1 1 0 0 0 0 0 0 0 
0 0 0 0 0 0 1 0 0 0 1 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 * * * * * * * * * * * * * * * * 0 
0 * * * * * * * * * * * * * * * * 0 
0 * * * * * * * * * * * * * * * * 0  
0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0

0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 
0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 
0 0 0 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 1 1 0 0 0 0 0 0 
0 0 0 0 0 0 0 0 0 1 0 1 0 0 0 0 0 0 
0 0 0 0 0 0 0 0 0 1 1 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 0 0 0 0 1 0 0 0 0 0 0 0 0 0 
0 0 0 0 0 0 1 1 1 1 1 0 0 0 0 0 0 0 
0 0 0 0 0 0 1 0 0 0 1 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 * * * * * * * * * * * * * * * * 0 
0 * * * * * * * * * * * * * * * * 0 
0 * * * * * * * * * * * * * * * * 0  
0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0

0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 
0 0 0 0 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 1 1 1 0 0 0 0 0 0 
0 0 0 0 0 0 0 0 1 1 1 1 1 0 0 0 0 0 
0 0 0 0 0 0 0 0 0 1 1 1 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 1 0 0 0 0 0 0 0 0 0 
0 0 0 0 0 0 1 1 1 1 1 0 0 0 0 0 0 0 
0 0 0 0 0 0 1 0 0 0 1 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 * * * * * * * * * * * * * * * * 0 
0 * * * * * * * * * * * * * * * * 0 
0 * * * * * * * * * * * * * * * * 0  
0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0

0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 
0 0 0 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 1 1 0 0 0 0 0 0 
0 0 0 0 0 0 0 0 1 1 0 1 1 0 0 0 0 0 
0 0 0 0 0 0 0 0 1 0 0 0 1 0 0 0 0 0 
0 0 0 0 0 0 0 0 1 1 0 1 1 0 0 0 0 0 
0 0 0 0 0 0 0 0 0 1 1 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 1 0 0 0 0 0 0 0 0 0 
0 0 0 0 0 0 1 1 1 1 1 0 0 0 0 0 0 0 
0 0 0 0 0 0 1 0 0 0 1 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 * * * * * * * * * * * * * * * * 0 
0 * * * * * * * * * * * * * * * * 0 
0 * * * * * * * * * * * * * * * * 0  
0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0

0 0 0 0 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 1 1 1 1 1 0 0 0 0 0 
0 0 0 0 0 0 0 0 1 0 0 0 1 0 0 0 0 0 
0 0 0 0 0 0 0 1 1 0 1 0 1 1 0 0 0 0 
0 0 0 0 0 0 0 0 1 0 0 0 1 0 0 0 0 0 
0 0 0 0 0 0 0 0 1 1 1 1 1 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 1 0 0 0 0 0 0 0 0 0 
0 0 0 0 0 0 1 1 1 1 1 0 0 0 0 0 0 0 
0 0 0 0 0 0 1 0 0 0 1 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 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 0 0 
0 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 0 
0 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40 x41 x42 x43 x44 x45 0 
0 x46 x47 x48 x49 x50 x51 x52 x53 x54 x55 x56 x57 x58 x59 x60 x61 0 
0 x62 x63 x64 x65 x66 x67 x68 x69 x70 x71 x72 x73 x74 x75 x76 x77 0 
0 x78 x79 x80 x81 x82 x83 x84 x85 x86 x87 x88 x89 x90 x91 x92 x93 0 
0 0 x94 x95 x96 x97 x98 x99 x100 x101 x102 x103 x104 x105 x106 x107 0 0 
0 0 x108 x109 x110 x111 x112 x113 x114 x115 x116 x117 x118 x119 x120 x121 0 0 
0 0 x122 x123 x124 x125 x126 x127 x128 x129 x130 x131 x132 x133 x134 0 0 0 
0 0 0 x135 x136 x137 x138 x139 x140 x141 x142 x143 x144 x145 0 0 0 0 
0 0 0 0 0 x146 x147 x148 x149 x150 x151 x152 x153 0 0 0 0 0 
0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
as ./lls -S lingeling input -r B.../S...(Snowflakes)

I think it has something to do with the number of columns or something? For some reason it "proves" in the pre-processing that it is unsatisfiable - this would mean that the 1s and 0s I had written cannot evolve like that but they totally do in that rule.
SoL : FreeElectronics : DeadlyEnemies : 6a-ite : Rule X3VI
what is “sesame oil”?

Post Reply