amling questionable searches/ideas firehose

NooneAtAll3 · Post by **NooneAtAll3** » June 12th, 2026, 10:49 am

well, if your ultimate goal is unattainable yet, what if you limit the width?

Post by **Sokwe** » June 12th, 2026, 9:16 pm

NooneAtAll3 wrote: June 12th, 2026, 10:49 am well, if your ultimate goal is unattainable yet, what if you limit the width?

The problem, as I understand it, is that being a polyomino is a global constraint, but LLSSS only tends to work well with certain types of more local constraints. As Amling said, this is a task better suited for a SAT solver like LLS, and as NNlk05 mentioned, LLS has a --polyomino option that forces the first generation to be a polyomino.

I find it much easier to use LLS by setting up the search with JLS, but the .jdf (JLS state file) reader in LLS doesn't yet support moving patterns. I have therefore created a new branch on my fork of LLS with a very quick and dirty hack to allow setting up moving pattern searches in JLS to be run with LLS. You currently need to manually place a row or column of OFF cells (in all generation) at the front edges of the spaceship for each cell that the spaceship moves during its period, or you might get invalid results. It should be possible to use this to set up searches that can disprove the existence of polyomino spaceships for low periods, but I don't intend to try it right now.

amling · Post by **amling** » June 13th, 2026, 12:36 am

NooneAtAll3 wrote: June 12th, 2026, 10:49 am well, if your ultimate goal is unattainable yet, what if you limit the width?

As I've tried to say above, even the closest approximation I can imagine squeezing out is a ton of work. LLSSS's data model is intensely, intensely weird and no one ever seems to have any idea what is easy and what is hard for it. You mostly have to take my word.

The reason I'm so fixated on being exact and exhaustion is that I assume that if there were any other polyomino patterns (i.e. ships or oscillators), we would already know them. If this is correct there will be no positive results to find and so the only possible result is a negative one, and the only meaningful (as far as I'm concerned) negative result is an exhaustive one.

Sokwe wrote: June 12th, 2026, 9:16 pm LLS has a --polyomino option that forces the first generation to be a polyomino.

...

It should be possible to use this to set up searches that can disprove the existence of polyomino spaceships for low periods, but I don't intend to try it right now.

I don't know what LLS's --polyomino option does or doesn't do, but to disprove existence of polyomino oscillators or spaceships from considering only a finite patch I think you're going to need a weaker constraint, namely "is this a polyomino as-is" (what I would guess the option does) logically or-ed together with "do all polyomino islands reach the edge". I guess I'm gonna call this "almost polyomino" since I'm likely gonna need to say it a lot.

amling wrote: June 8th, 2026, 12:53 pm I would probably try a SAT solver approach, modeling some patch of a hypothetical pattern and forcing a cell on, but then also encoding and requiring "the first generation of the pattern can be completed into a polyomino (i.e. is a polyomino or all islands reach the edge)". Then increase patch size until you get a pattern, an UNSAT, or run out of computer.

I have given this one afternoon's worth of prototyping work with mixed results. I believe my implementation of the weaker "almost polyomino" global constraint is likely correct, but in the limited time I have given it to run so far it has not been able to exhaust much of anything. The only success is one of two phases of trying to show no c/2 polyomino ships. This input file, read as c/2 north, requiring "almost polyomino" in the 0th/first/left generation, gives UNSAT: