General SAT solver discussion thread?

For general discussion about Conway's Game of Life.
Post Reply
User avatar
pcallahan
Posts: 845
Joined: April 26th, 2013, 1:04 pm

General SAT solver discussion thread?

Post by pcallahan » January 23rd, 2021, 3:33 pm

When I look at old Forum postings, I can see there is a lot of interest in SAT solvers for Life and other CA searching, though I don't see a general thread for discussing ideas of how to get the most effective use of SAT solvers. I'd like to start one, though I'm happy to move my question to an existing one if I missed it.

First a comment: SAT is one of the classic NP complete problems, and writing a SAT instance is essentially programming a non-deterministic machine (more in the sense of "linear programming" than "Java programming" since a SAT instance is not a general TM program). As a result, you get a remarkable amount of expressive power, and if you had an actual non-deterministic machine, you'd have a sort of magic oracle for all your search needs. That part is fantasy, but the reality is that modern SAT solvers can seem pretty magical, at least to me. It is often possible to write instances of problems without thinking too hard beyond expressive power and a SAT solver can give you an answer in reasonable time. This is exciting, since the alternative is to make up a whole new search algorithm every time (and I'm embarrassed to say I'm at least 10 years behind the curve on this, but trying to catch up).

Second, I have a lot of questions, but here's a very specific one to start out. Has anyone used a SAT-solver to do collision-based searching in addition to the more typical oscillator searches? Here's the kind of of encoding I have in mind.

A collision search requires a correlated pattern of cells to be placed at one of a number of positions initially, say mn positions on a subgrid of m rows and n columns. For the sake of simplicity, suppose m=2, n=2, and there is just one live cell to place. Then we can label positions with binary-encoded integers, and introduce 4 position booleans i_0, i_1, j_0, j_1 to encode the bits.

E.g. place a live cell in one of 16 positions relative to an original--say (3, 7)--on a larger grid. Giving grid cells names, c_3_7, c_3_8, ..., c_6_9, c_6_10 must be live. Then we can introduce clauses that require the live cell to match bit positions. E.g.:

c_4_9 or i_1 or ~i_0 or ~j_1 or j_0

Rewriting as an implication, we have:

~i_1 and i_0 and j_1 and ~j_0 → c_4_9.

Or in other words, if i=1 (01 binary) and j=2 (10 binary), then the cell at (3+1, 7+2) must be live.

This can be extended to force cells off, and the same position variable set can force the placement of multiple cells relative to each other. E.g. to place a glider in a particular phase and position with a one-cell empty boundary, introduce 25 clauses for each cell in the 5x5 box. Introduce ⌈log_2 m⌉ + ⌈log_2 n⌉ positional variables along with some additional logic to bound m and n if they are not powers of 2.

All right, so that's the encoding. The question is whether a SAT solver can handle it. I suspect it will be able to, at least based on my other experience encoding integers as labels and cardinality constraints with binary adder clauses.

You might ask what's this good for. If you just want to set up collisions of gliders, it's a roundabout way, and likely to get infeasible for interactions of more than a few generations. On the other hand, the fact that it's in SAT instance allows you to express other constraints that are less rigid. For instance, I can imagine this being used to combine a collision with an unspecified catalyst that is only required to be a still life and be restored after the collision. It would only work for fairly fast-acting catalysts, but this might extend the types of search. Of course, if you just want a single eater, you can begin with a glider in a fixed position.

It's possible that this whole approach is silly and it would be better to construct multiple SAT instances, each based on an initial setup for a collision. This is part of the reason I'm asking. I am curious if anyone has try anything like this.

Post Reply