Code:
Select all

`x = 64, y = 64, rule = LifeHistory`

3D2C3D3.2A3.2D2CDC2D3.2A3.3D2C3D3.2A3.2D2CDC2D3.2A$8D8.8D8.8D8.8D$DC

6D.A6.2D2CDC2D8.DC6D.A6.2D2CDC2D$CDC5DA.A5.DCDCD3C4.2A2.CDC5DA.A5.DCD

CD3C4.2A$DC3D2CD.A3.2A.C2DC4DA2.A2.A.DC3D2CD.A3.2A.C2DC4DA2.A2.A$C3DC

2DCA3.A2.ACDC2D3C3.2A2.AC3DC2DCA3.A2.ACDC2D3C3.2A2.A$4D2C2D4.2A2.2D2C

DC2D8.4D2C2D4.2A2.2D2CDC2D$8D8.2DC2DC2D3.2A3.8D8.2DC2DC2D3.2A$8.8D3.

2A3.3D2C3D8.8D3.2A3.3D2C3D$4.2A2.4D2C2D8.8D4.2A2.4D2C2D8.8D$A3.A2.AC

3DC2DCA6.AC6DCA3.A2.AC3DC2DCA6.AC6DC$A4.2A.C4D2CD.A5.ADC5DCA4.2A.C4D

2CD.A5.ADC5DC$8.8D2A6.2C6D8.8D2A6.2C6D$8.8D2.2A.A2.2D2CDC2D8.8D2.2A.A

2.2D2CDC2D$2.A5.2DC5D2.A.2A2.2DCD2C2D2.A5.2DC5D2.A.2A2.2DCD2C2D$2.3A

3.2D3C3D8.8D2.3A3.2D3C3D8.8D$5DC2D5.A2.8D8.5DC2D5.A2.8D$2D4C2D4.A3.2D

2C4D2.2A4.2D4C2D4.A3.2D2C4D2.2A$DC6D4.4ADCDC2D2C.A.A2.2ADC6D4.4ADCDC

2D2C.A.A2.2A$D2C2D3C7.ADCDCDCDC.A.A.A.AD2C2D3C7.ADCDCDCDC.A.A.A.A$2DC

2DC2DA3.2A.ADCD2C2DC.A.2A2.A2DC2DC2DA3.2A.ADCD2C2DC.A.2A2.A$C5D2C3.A.

A.ACDC4DCA.A4.AC5D2C3.A.A.ACDC4DCA.A4.A$8D2.A5.2DC5D2.A5.8D2.A5.2DC5D

2.A$3D2C3D2.3A3.2D3C3D2.3A3.3D2C3D2.3A3.2D3C3D2.3A$3.2A3.5DC2D5.A2.5D

C2D3.2A3.5DC2D5.A2.5DC2D$8.2D4C2D4.2A2.4D2C2D8.2D4C2D4.2A2.4D2C2D$6.

2ADC6D8.8D6.2ADC6D8.8D$.A3.A.AD2C2D3C4.4A4D2C2D.A3.A.AD2C2D3C4.4A4D2C

2D$A.A.A2.A2DC2DC2DA2.A4.A3DCDCDA.A.A2.A2DC2DC2DA2.A4.A3DCDCD$A.A.2A.

2A5D2C3.5A7DCA.A.2A.2A5D2C3.5A7DC$2.A2.A2.8D8.2DE5D2.A2.A2.8D8.2DE5D$

2.A2.A2.3D2C3D2.A.2A2.2D3E3D2.A2.A2.3D2C3D2.A.2A2.2D3E3D$3D2C3D3.2A3.

2D2CDC2D3.2E3.3D2C3D3.2A3.2D2CDC2D3.2E$8D8.8D8.8D8.8D$DC6D.A6.2D2CDC

2D8.DC6D.A6.2D2CDC2D$CDC5DA.A5.DCDCD3C4.2A2.CDC5DA.A5.DCDCD3C4.2A$DC

3D2CD.A3.2A.C2DC4DA2.A2.A.DC3D2CD.A3.2A.C2DC4DA2.A2.A$C3DC2DCA3.A2.AC

DC2D3C3.2A2.AC3DC2DCA3.A2.ACDC2D3C3.2A2.A$4D2C2D4.2A2.2D2CDC2D8.4D2C

2D4.2A2.2D2CDC2D$8D8.2DC2DC2D3.2A3.8D8.2DC2DC2D3.2A$8.8D3.2A3.3D2C3D

8.8D3.2A3.3D2C3D$4.2A2.4D2C2D8.8D4.2A2.4D2C2D8.8D$A3.A2.AC3DC2DCA6.AC

6DCA3.A2.AC3DC2DCA6.AC6DC$A4.2A.C4D2CD.A5.ADC5DCA4.2A.C4D2CD.A5.ADC5D

C$8.8D2A6.2C6D8.8D2A6.2C6D$8.8D2.2A.A2.2D2CDC2D8.8D2.2A.A2.2D2CDC2D$

2.A5.2DC5D2.A.2A2.2DCD2C2D2.A5.2DC5D2.A.2A2.2DCD2C2D$2.3A3.2D3C3D8.8D

2.3A3.2D3C3D8.8D$5DC2D5.A2.8D8.5DC2D5.A2.8D$2D4C2D4.A3.2D2C4D2.2A4.2D

4C2D4.A3.2D2C4D2.2A$DC6D4.4ADCDC2D2C.A.A2.2ADC6D4.4ADCDC2D2C.A.A2.2A$

D2C2D3C7.ADCDCDCDC.A.A.A.AD2C2D3C7.ADCDCDCDC.A.A.A.A$2DC2DC2DA3.2A.AD

CD2C2DC.A.2A2.A2DC2DC2DA3.2A.ADCD2C2DC.A.2A2.A$C5D2C3.A.A.ACDC4DCA.A

4.AC5D2C3.A.A.ACDC4DCA.A4.A$8D2.A5.2DC5D2.A5.8D2.A5.2DC5D2.A$3D2C3D2.

3A3.2D3C3D2.3A3.3D2C3D2.3A3.2D3C3D2.3A$3.2A3.5DC2D5.A2.5DC2D3.2A3.5DC

2D5.A2.5DC2D$8.2D4C2D4.2A2.4D2C2D8.2D4C2D4.2A2.4D2C2D$6.2ADC6D8.8D6.

2ADC6D8.8D$.A3.A.AD2C2D3C4.4A4D2C2D.A3.A.AD2C2D3C4.4A4D2C2D$A.A.A2.A

2DC2DC2DA2.A4.A3DCDCDA.A.A2.A2DC2DC2DA2.A4.A3DCDCD$A.A.2A.2A5D2C3.5A

7DCA.A.2A.2A5D2C3.5A7DC$2.A2.A2.8D8.2DC5D2.A2.A2.8D8.2DC5D$2.A2.A2.3D

2C3D2.A.2A2.2D3C3D2.A2.A2.3D2C3D2.A.2A2.2D3C3D!

Current tiling, above. Looks weird.

Here's the tiles and how they fit together:

Code: Select all

`+---+---+---+---+`

| 2 | 2 | 3 | 2 |

|181|181|193|311|

| 0 | 0 | 2 | 2 |

+---+---+---+---+

| 0 | 0 | 2 | 2 |

|232|232|242|242|

| 1 | 1 | 0 | 0 |

+---+---+---+---+

| 1 | 1 | 0 | 0 |

|063|3a0|050|050|

| 2 | 1 | 1 | 1 |

+---+---+---+---+

| 2 | 1 | 1 | 1 |

|170|063|323|301|

| 2 | 2 | 3 | 1 |

+---+---+---+---+

Center number is the index of the tile

dvgrn wrote:I'm really happy to see someone with expertise with SAT solvers applying them successfully to Life problems.

LOL. My encodings are completely naive, and would probably make any actual expert cringe.

dvgrn wrote:Am curious to see if you can really handle the P2 case so easily -- seems like there might be a smaller tile that's all blinkers, or all P2 anyway, but I ran into ugly conflicts when I tried to lay it out manually.

It depends: if you're talking about each cell being "independent", than it's hideous. (In other words, if each tile oscillates in different ways depending on the adjacent tiles). The same problem as crops up with the corner tiles gets worse as the period increases.

dvgrn wrote:I strongly suspect that SAT solvers could break a lot of new ground in these kinds of CA puzzles, as they have already for small Gardens of Eden.

It's mainly a matter of those areas of the search space that have and have not been explored. As you say: breaking new ground.

dvgrn wrote:For example, one really simple way to solve the Conway's Life omniperiodicity problem would be to find a 2c/3 signal elbow, or alternatively a 2c/3 double-signal to single-signal converter (since we already have an elbow).

Jargon! I'll need some time to read that.

dvgrn wrote:It seems as if it should be possible to set up a SAT solver to hunt for one of these 2c/3 converter patterns, as long as the area of the reaction is small enough and the reaction settles quickly enough.

Biggest problem is defining exactly what you want.

dvgrn wrote:Maybe Dean Hickerson's 'drifter' program has already covered the ground efficiently enough, and there's no solution out there in the reachable search space -- but SAT solvers look like an interesting new angle to try, anyway.

One of the nice things about SAT solvers is that it's relatively easy to try different solvers, once you've formulated the problem.

dvgrn wrote:I'd try it myself... but I'm in need of a very basic tutorial on SAT solvers first -- e.g., where can I download one that will work well, and how do I set up constraints efficiently for a large CA grid?

So, SAT solvers. I personally have figured out how to use them pretty much entirely in a self-taught manner, although I've got enough of a math / logic / CS background to have some vague idea what they are talking about.

There are a number of different types, but most of them are effectively equivalent (in the sense that if you have a problem in one type you can fairly easily convert it to a problem in another, most of the time at least).

You've got a split between SATisfiability solvers, and OPTimizers. SAT solvers try to find an assignment of variables that satisfy all the constraints, whereas optimizers try to find an assignment of variables that satisfy all the constraints and also minimize or maximize a certain objective function. Generally you see minimization more than maximization, but they are generally fairly trivially converted back and forth.

You also have a split between straight linear programming (LP), mixed integer programming (MIP), integer linear programming (ILP), pseudo-boolean programming (PBSAT or PBOPT (or 0-1 ILP, occasionally)), binary programming (BSAT), CNFSAT, and 3CNFSAT.

Kind of two groups here: LP, MIP, ILP, and PBSAT/OPT or 0-1 ILP (and sometimes BSAT) are largely math-based; BSAT / CNFSAT / 3CNFSAT are generally logic-based.

The easier one to explain is the math-based types. You have a bunch of constraints. Each constraint is what's known as a linear sum of variables (that is: you can multiply variables by constants, and you can add variables / multiples of variables, but you cannot multiply variables), greater than some constant. (Occasionally you'll see less than, greater than or equal, less than or equal, or equal - but again you can translate between all of these fairly easily. You cannot directly express an inequality, however! ).

Depending on the type, the variables can be different types. In linear programming, the variables are general real numbers. In integer linear programming,the variables are constrained to be integers. In mixed integer programming some variables are constrained to be integers, but not necessarily all. In 0-1 ILP variables are constrained to be 0 or 1.

The logic-based ones use boolean operators instead, and are a bit more varied. CNF form is "special" - all it is is an AND of ORs of variables or their negations, the goal being to find an assignment of true/false to the variables such that the expression is true. 3CNF is a further restriction that all clauses contain only 3 variables or negations of variables.

I personally tend to use Minisat+, which is a PBSAT / PBOPT solver. In particular, it takes things in this form, which is fairly easy to output and fairly easy to understand:

Code: Select all

`* #variable= 5 #constraint= 4`

*

* comments

*

*

min: 1 x2 -1 x3 ;

1 x1 +4 x2 -2 x5 >= 2;

-1 x1 +4 x2 -2 x5 >= +3;

12345678901234567890 x4 +4 x3 >= 10;

* an equality constraint

2 x2 +3 x4 +2 x1 +3 x5 = 5 ;

So, imagine you're doing an incredibly naive encoding of the standard B3/S23 rule. You have 8 adjacent previous states of cells, A through H, the previous state of the cell P, and you want the next state of the cell, N.

If you were just describing it, it'd be "N is 1 if and only if either there are 3 living neighbors, or if there are 2 living neighbors and N is alive".

You could just work through all the cases - which is a relatively large rule, but workable for small sets of constraints. But still larger than we'd like.

First problem: how do you do a logical OR? One trick: z = (x or y) becomes

Code: Select all

` z >= x; z >= y; z <= x + y.`

A logical NOT is easy - just replace the variable with (1 - variable), and expand out and re-simplify constants as necessary. So you also have AND. z = (x and y) becomes

Code: Select all

`z <= x; z <= y; z >= x + y - 1`

Second problem: how do you do "3 living neighbors"? Well, you can't really. But you can do (>= 3 living neighbors) and (<= 3 living neighbors). There's a slight restatement of the question that makes things a little simpler, though: "N is 1 if and only if both there are <= 3 living neighbors, and either there are >=3 living neighbors, or if there are >=2 living neighbors and N is alive". Makes you only need to do 3 of these clauses instead of 4.

But how do you actually do "at least k living neighbors"? I came up with two clauses:

Code: Select all

`out *8 >= sum(neigh) + 1 - k; out * k <= sum(neigh)`

For "at most k living neighbors" I came up with a similar thing:

Code: Select all

`out * 8 >= k + 1 - sum(varr); out * (8 - k) + sum(varr) <= len(varr)`

So then all told you get the following:

Code: Select all

`* sum >= 2 follows next 2 lines`

-1 x3 -1 x4 -1 x5 -1 x6 -1 x7 -1 x8 -1 x9 -1 x10 +8 x11 >= -1;

+1 x3 +1 x4 +1 x5 +1 x6 +1 x7 +1 x8 +1 x9 +1 x10 -2 x11 >= 0;

* sum >= 3 follows next 2 lines

-1 x3 -1 x4 -1 x5 -1 x6 -1 x7 -1 x8 -1 x9 -1 x10 +8 x12 >= -2;

+1 x3 +1 x4 +1 x5 +1 x6 +1 x7 +1 x8 +1 x9 +1 x10 -3 x12 >= 0;

* sum <= 3 follows next 2 lines

+1 x3 +1 x4 +1 x5 +1 x6 +1 x7 +1 x8 +1 x9 +1 x10 +8 x13 >= 4;

-1 x3 -1 x4 -1 x5 -1 x6 -1 x7 -1 x8 -1 x9 -1 x10 -5 x13 >= -8;

* Logical and follows next 2 lines

+1 x11 +1 x2 -2 x14 >= 0;

-1 x11 -1 x2 +2 x14 >= -1;

* Logical or follows next 2 lines

-1 x14 -1 x12 +2 x15 >= 0;

+1 x14 +1 x12 -2 x15 >= -1;

* Logical and follows next 2 lines

+1 x15 +1 x13 -2 x1 >= 0;

-1 x15 -1 x13 +2 x1 >= -1;

x1 is the new cell state, x2 is the old cell state, x3..x10 are the adjacent cell states, and x11..x15 are temporary variables

(Using a slightly different encoding for and and or here than the one described)

There are substantially more efficient encodings out there, but this "works".

Notably, you can rewrite the rule as "N is 1 if and only if both there are <= 3 living neighbors, and there are >=3 living neighbors including this cell's old state".

The problem with my Wang tile finder (roughly speaking: there's a set of 11 tiles with a color per side that tile the plane aperiodicially as long as you ensure the colors match on adjacent tiles - I'm trying to find a set of Life nxn tiles that can do so, where "color match" == "pattern is stable") is twofold.

First, there's the problem of the corner cells of each tile. As long as you ignore the corner cells and are only going after still-life, the problem is simple, essentially just "For each tile, for each direction, for each other tile, all the cells on the edge of this tile and on the edge of the other tile adjacent to this one should be stable if and only if the colors match. Also: the rest of each tile should be stable". But the corner cells are more difficult, as they are dependent on three other tiles, and there doesn't seem to be a good way to avoid having to go "for all combinations of 8 tiles surrounding this one" - which involves looping over 11^9 tiles (not exactly practical).

What I'm doing now is simply enforcing that the 16 corner cells (block in each corner) of each tile remain dead - but this means that I'm missing some potential tilings.

Second, there's the problem of encoding non-still-life. In particular, imagine if the period is high. Then it is entirely possible that if you place two tiles next to each other they will not be stable - but they will appear to be stable in the immediate neighborhood. Imagine if the two tiles form a glider gun, for instance. Looking at the local neighborhood only, it appears to be stable, whereas it actually isn't.

As long as the period is less than the size of the tile, this should not be a problem (speed of light being one cell / tick and all that). But it's still potentially a problem - and regardless it expands the number of cells that are affected by the corner cell problem.