SAT solvers as searchers and Wang tiles

[NotLiving]

(Note: this was pulled away from the "basic questions" thread here.)

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

11_4color_Wang_tiles.png (28.06 KiB) Viewed 6535 times

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.

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.

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.

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.

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.

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.

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.

There are more efficient encodings, but this works. (Just work through all the possible combinations of x/y/z being 0 and 1. Or alternatively: the first two constraints force the output to be 1 if either input is 1, and the third forces the output to be 0 if neither output is 1)

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)

. It works out - the first constraint forces the output variable to be true if there are at least k living neighbors, the second forces the output variable to be false if there are less than k living neighbors.

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)

. Same comment as above, albeit switched.

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.

[dvgrn]

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.

Here's a post from last year, where I guessed that it might be wishful thinking to expect to get anywhere by throwing SAT solvers at the omniperiodicity problem -- specifically at the 2c/3 elbow/converter problem.

That was just a guess, though, based on the theory that SAT solvers are going to be much happier figuring out stable stuff, and maybe p2 or p3 stuff on the outside, as opposed to elbow mechanisms that might take a dozen or more ticks to settle.

Anyway, there was a link in there to the Garden of Eden #6 paper, which was a nice application of SAT solvers. The practical limit that the paper described seemed to be 30-40 unknown cells... but a 2c/3 wire will have a sheath of stable cells (stator) and the trick might be to do progressively more ambitious searches with increasing rotor size, until a working elbow is found.

[NotLiving]

Things like garden-of-eden problems are rather difficult to express cleanly as a SAT problem - given they are more alone the lines of "find a pattern such that there does not exist a precursor", and it's hard to map that easily. The paper you linked did warm-start based QSAT; I'd be shocked if it wasn't at a minimum hundreds of thousands of restarts (if not more). Warm restarts, but still. It's substantially easier to do straight existence-finding.

(Case in point: the aperiodic tiling I found was ~181 live cells, and that just took a few hours on a laptop.)

So...

What exactly is this conduit you are talking about, and what state do you want to come from, and what state do you want to go to, in how many ticks? I'm assuming it needs to be stable even without a signal? Does it need to be stilllife without a signal, or just stable? Any other properties it has to have?

It's worth a try, at least. Worse comes to worse, it doesn't work.

[dvgrn]

What exactly is this conduit you are talking about, and what state do you want to come from, and what state do you want to go to, in how many ticks?

The 2c/3 wire in its simplest form looks like the following. The signal is the two colored cells in the northwest:

Code: Select all

x = 40, y = 38, rule = LifeHistory
8.2A$3.2A.A2.A$3.2A.3A2$3.6A$2.A6.A$2.A.CD4A$A.A.A7.A$2A2.A2.6A$4.A.A
$3.2A.A2.6A$6.A.A6.A$6.A.A2.5A$7.2A.A7.A$10.A2.6A$10.A.A$9.2A.A2.6A$
12.A.A6.A$12.A.A2.5A$13.2A.A7.A$16.A2.6A$16.A.A$15.2A.A2.6A$18.A.A6.A
$18.A.A2.5A$19.2A.A7.A$22.A2.6A$22.A.A$21.2A.A2.6A$24.A.A6.A.2A$24.A.
A2.5A.2A$25.2A.A$28.A2.6A$28.A.A5.A$27.2A.A2.3A$30.A.A5.2A$30.A2.A4.
2A$31.2A!

Golly's files include a Python script, heisenburp.py, that showcases a complete conversion from a glider signal to one of these 2c/3 signals, and back to a glider again. But to solve the omniperiodicity problem we need to keep the signal as a 2c/3 signal most of the time. Any mechanisms need to be stable when there isn't a signal passing through them, and they need to recover in less than 19 ticks.

That's because periods 19, 23, 38 and 41 are the only remaining missing periods needed to prove that Life is omniperiodic. The simplest way to build those is to put a bunch of equally-spaced signals into an adjustable-length signal loop, and adjust the length so the configuration repeats at p19 or p23 or p38 or p41. All that's needed is an extensible stable wire like this one, and a way to bend a signal around a 90-degree corner.

I'm assuming it needs to be stable even without a signal? Does it need to be stilllife without a signal, or just stable? Any other properties it has to have?

Stable is best. A p2 structure could solve the p38 case but not the other ones, and any other period besides 19, 23, or 41 wouldn't help at all.

There's a stable elbow already known, but it doubles the signal:

Code: Select all

x = 38, y = 57, rule = LifeHistory
9.2A$4.2A.A2.A$4.2A.3A2$4.6A$3.A6.A$3.A.CD4A$.A.A.A7.A$.2A2.A2.6A$5.A
.A$4.2A.A2.6A$7.A.A6.A$7.A.A2.5A$8.2A.A7.A$11.A2.6A$11.A.A$10.2A.A2.
6A$13.A.A6.A3.2A$13.A.A2.5A2.A2.A$14.2A.A7.3A.A$17.A2.5A3.A.A.2A$17.A
.A6.A3.A.A$16.2A.A2.6A2.A.A$19.A.A6.A.A.A.A$19.A.A2.4A.A2.2A.A$20.2A.
A3.A.A.A3.A$23.A.A3.A.A.2A.2A$20.3A.A.4A.A2.A.A$20.A3.A7.A.A2.A$24.8A
2.3A$31.A.A$22.7A2.A.2A$21.A7.A.2A2.A$21.6A2.A4.2A$27.A.A$19.6A2.A.2A
$18.A6.A.A$18.5A2.A.A$15.A7.A.2A$15.6A2.A$21.A.A$13.6A2.A.2A$12.A6.A.
A$12.5A2.A.A$9.A7.A.2A$9.6A2.A$15.A.A$7.6A2.A.2A$3.2A.A6.A.A$3.2A.5A
2.A.A$11.A.2A$3.6A2.A$3.A5.A.A$4.3A2.A.2A$2A5.A.A$2A4.A2.A$7.2A!

By sheer coincidence, the doubled signal can still interact with the end of the wire in the same way, as shown. But a doubled signal can't be run through another elbow, so there's no known way to close a loop (except for what heisenburp.py does, which is much much too slow to handle p41, let alone p19).

So what's needed is either

1) a stable wire pattern that converts a double signal back to a single signal traveling in the same direction, or
2) a stable elbow that converts a single signal into a 90-degree single signal.

Or

3) a stable elbow that converts a double signal to a 90-degree double signal would be fine too, of course.

And proceeding at exponential speed down the unlikely-to-be-findable scale, it would be great to find a stable wire termination that produces an output glider or Herschel and recovers its original configuration, and/or a stable object that eats a glider and guides the active reaction into a 2c/3 wire. Those have been on the Most Wanted list for a couple of decades also.

2c/3 wires aren't the only possibility, just the most likely one. For example, getting a lightspeed wire signal to turn a corner would also solve the omniperiodicity problem very nicely.