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.Saka wrote:What's preprocessing for? Most of my search time is spent on preprocessing which is annoying.
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.
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/S012345678Also is there a way to force a transition? I want to force B1e.
No idea, that seems weird.
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.Rhombic wrote:Bellman-LLS
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.
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.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:
I think I've fixed this now, but who knows?
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 "--".]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.
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
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")