vyznev wrote:wildmyron wrote:I'm not sure I agree with you about what happens in long running searches though. The SAT solver has no concept of partial patterns and, as I understand it, takes a much more global approach to finding a solution which satisfies the problem, or finding a contradiction which rules out the existence of a solution.

Well, sorta. Unless LLS is doing something really odd in mapping the search to a SAT instance, most of the SAT variables should directly correspond to the states of individual cells. (Some will correspond to rule string bits, and there might be some auxiliary variables used to simplify the encoding of some constraints.) So in that sense, the current variable assignments made by the SAT solver at any given time should in fact be interpretable as a partial pattern of cells (and possibly rule transitions).

I see what you mean now. Just like for WLS it doesn't make sense to make trial variable assignments with variables that represent cells which are disconnected from each other. And with each trial variable assignment further deductions can be made about variables that represent nearby cells, and so as you say the solver builds what we could interpret as a partial solution.

AforAmpere wrote:<snip fast p12 ships>

Has anyone done manual searches for a 9c/10 frontend?

Nice work with p12 there. I had done some exploration of 9c/10 but hadn't found anything promising. I was inspired to give it another go and I've been dabbling with using lls to find partials. Here's my first result - front 3 columns reappear after 10 generations:

`x = 4, y = 21, rule = B2-in3-ain4einqtz5-eij6cen7/S02an3jnqry4ijkqrty5-ekn6ai7c8`

bo$obo$b2o$o$bobo$2bo$obo$bobo$2b2o$bo$b3o$bo$2b2o$bobo$obo$2bo$bobo$o

$b2o$obo$bo!

I'm out of time, maybe someone else can complete this.