SymSAT, another SAT-solver-based search package

For scripts to aid with computation or simulation in cellular automata.
Post Reply
User avatar
pcallahan
Posts: 845
Joined: April 26th, 2013, 1:04 pm

SymSAT, another SAT-solver-based search package

Post by pcallahan » January 19th, 2021, 8:15 pm

[Note: immediately after posting I found that "GridSAT" is already in use, so I hastily changed the name though not the repo. I probably should have put more thought into a name. SymSAT reflects both the importance of symmetry and the use of symbols in place of DIMACS numerical values.]

Motivation: When I started to play around with Oscar Cunningham's Logic Life Search, I got very interested in the potential of SAT solvers for the kinds of problems I am most interested in lately, but I was also frustrated by the difficulty of making sense of DIMACS files. I got a little carried away with the idea and wrote a package that you can find at https://github.com/PaulBC/grid-sat-solver. It is not fully documented, but includes a README with "quickstart" instructions for a demo of its capabilities.

SymSAT, written in Python, is intended to solve the readability problem of SAT instances in part by making it possible to use a readable symbol-based format and apply common concepts like grid symmetry, rule symmetry, and cardinality constraints to the SAT instance. It is not intended to compete with potentially faster Life search approaches. My current interest is in finding tesselations, and I think it will be useful for this. I have included examples to show how it can be used for Life searches (as a benchmark, it can find 25P3H1V0.1 in about 3.8s of SAT solver time on my Macbook, though it also needs about 2 seconds to set up the instance; I have reduced SAT time to under 0.5s by tweaking constraints, but this is the most general approach).

Like LLS, it requires a SAT solver. I use lingeling, but any that support DIMACS format could potentially work. It is not a standalone app, but an API, so you have to write a Python main for each search. However, it would not be hard to build something more immediately usable on top of it.

Quick start:
  1. Install lingeling, e.g. by following these instructions: https://www.conwaylife.com/wiki/Tutoria ... _Lingeling
  2. Make sure the executable is on your path. E.g. copy the lingeling binary to /usr/local/bin/lingeling or add its location to PATH.
    Verify that "lingeling --help | head" produces truncated help, beginning "usage: lingeling ..."
  3. git clone https://github.com/PaulBC/grid-sat-solver
  4. cd grid-sat-solver
  5. python demo.py
One very intentional part of my approach is not to hardcode anything about Life or CAs in Python, though I have hardcoded the Moore neighborhood and certain implementations of symmetries. But the only part specific to Life is this logic template to which totalistic symmetry is applied. Note that <- is used to represent a disjunctive clause that is more intuitively seen as an implication arrow. I.e., instead of saying "a or not b or not c" you can say "a is implied by (<-) b and c" analogously to Prolog :- but we're not limited to Horn clauses.

Code: Select all

  # death by loneliness or crowding
  ~G <- ~N ~NE ~E ~SE ~S ~SW ~W
  ~G <- N NE E SE
  # birth on 3 neighbors
   G <- N NE E ~SE ~S ~SW ~W ~NW
  # survival on 2 or 3 neighbors
  ~G <- ~O N NE ~E ~SE ~S ~SW ~W ~NW
   G <- O N NE ~E ~SE ~S ~SW ~W ~NW
 
It can still perform reasonably fast searches at least for small periods. The following examples are all shown in the demo.

Here is an example of a still life patch with rotational symmetry, extended here into an agar.

Code: Select all

x = 40, y = 40, rule = B3/S23:T40,40
bobobob3obo2bobobo2bobobob3obo2bobobo$obobobo6bobo3b2obobobo6bobo3bo$
2bobo2bo4b2o2b3o3bobo2bo4b2o2b3o$obob3o3bo2bo5b2obob3o3bo2bo5bo$bo5b4o
bo3b3o2bo5b4obo3b3o$o5bo5b2o2bo2b2o5bo5b2o2bo2bo$b3obob2ob2o2bobobo2b
3obob2ob2o2bobobo$2bob2o2bobo2bobobobo2bob2o2bobo2bobobobo$o5bo5b2obo
3b2o5bo5b2obo3bo$3b2ob2o7bo3bo3b2ob2o7bo3bo$o3bo7b2ob2o3bo3bo7b2ob2o$o
3bob2o5bo5b2o3bob2o5bo5bo$obobobo2bobo2b2obo2bobobobo2bobo2b2obo$bobob
o2b2ob2obob3o2bobobo2b2ob2obob3o$o2bo2b2o5bo5b2o2bo2b2o5bo5bo$b3o3bob
4o5bo2b3o3bob4o5bo$o5bo2bo3b3obob2o5bo2bo3b3obobo$b3o2b2o4bo2bobo3b3o
2b2o4bo2bobo$o3bobo6bobobob2o3bobo6bobobobo$bobobo2bob3obobobo2bobobo
2bob3obobobo$bobobob3obo2bobobo2bobobob3obo2bobobo$obobobo6bobo3b2obob
obo6bobo3bo$2bobo2bo4b2o2b3o3bobo2bo4b2o2b3o$obob3o3bo2bo5b2obob3o3bo
2bo5bo$bo5b4obo3b3o2bo5b4obo3b3o$o5bo5b2o2bo2b2o5bo5b2o2bo2bo$b3obob2o
b2o2bobobo2b3obob2ob2o2bobobo$2bob2o2bobo2bobobobo2bob2o2bobo2bobobobo
$o5bo5b2obo3b2o5bo5b2obo3bo$3b2ob2o7bo3bo3b2ob2o7bo3bo$o3bo7b2ob2o3bo
3bo7b2ob2o$o3bob2o5bo5b2o3bob2o5bo5bo$obobobo2bobo2b2obo2bobobobo2bobo
2b2obo$bobobo2b2ob2obob3o2bobobo2b2ob2obob3o$o2bo2b2o5bo5b2o2bo2b2o5bo
5bo$b3o3bob4o5bo2b3o3bob4o5bo$o5bo2bo3b3obob2o5bo2bo3b3obobo$b3o2b2o4b
o2bobo3b3o2b2o4bo2bobo$o3bobo6bobobob2o3bobo6bobobobo$bobobo2bob3obobo
bo2bobobo2bob3obobobo!
It can search for "Phoenix" oscillators by adding an additional constraint (either "original" or "generated" must be false):

Code: Select all

# no two consecutive live generations
  ~G ~O
And here is the result, again with rotational symmetry extended into an agar:

Code: Select all

x = 48, y = 48, rule = B3/S23:T48,48
bo6b2o9bobo3bo6b2o9bobo$3b2o9bo8bo3b2o9bo8bo$o5bo3bo5bobobo3bo5bo3bo5b
obobo$2bo3bobo3bobobo5bo3bo3bobo3bobobo5bo$o9bo11bobo9bo11bo$2bo10bo
12bo10bo$9bobo8b2o11bobo8b2o$2b2o9bobo10b2o9bobo$7bobo10bo2bo7bobo10bo
2bo$bobo11bobo5bobobo11bobo5bo$5bobo11bobo7bobo11bobo$3bo13bo9bo13bo$
6bo13bo9bo13bo$2bobo11bobo7bobo11bobo$o5bobo11bobobo5bobo11bobo$o2bo
10bobo7bo2bo10bobo$8bobo9b2o10bobo9b2o$2b2o8bobo11b2o8bobo$10bo10bo12b
o10bo$bo11bo9bobo11bo9bo$bo5bobobo3bobo3bo3bo5bobobo3bobo3bo$3bobobo5b
o3bo5bo3bobobo5bo3bo5bo$o8bo9b2o3bo8bo9b2o$2bobo9b2o6bo3bobo9b2o6bo$bo
6b2o9bobo3bo6b2o9bobo$3b2o9bo8bo3b2o9bo8bo$o5bo3bo5bobobo3bo5bo3bo5bob
obo$2bo3bobo3bobobo5bo3bo3bobo3bobobo5bo$o9bo11bobo9bo11bo$2bo10bo12bo
10bo$9bobo8b2o11bobo8b2o$2b2o9bobo10b2o9bobo$7bobo10bo2bo7bobo10bo2bo$
bobo11bobo5bobobo11bobo5bo$5bobo11bobo7bobo11bobo$3bo13bo9bo13bo$6bo
13bo9bo13bo$2bobo11bobo7bobo11bobo$o5bobo11bobobo5bobo11bobo$o2bo10bob
o7bo2bo10bobo$8bobo9b2o10bobo9b2o$2b2o8bobo11b2o8bobo$10bo10bo12bo10bo
$bo11bo9bobo11bo9bo$bo5bobobo3bobo3bo3bo5bobobo3bobo3bo$3bobobo5bo3bo
5bo3bobobo5bo3bo5bo$o8bo9b2o3bo8bo9b2o$2bobo9b2o6bo3bobo9b2o6bo!
I am actually a lot more interested in hex grids, and made this with a rhombic patch that can tesselate the plane:

Code: Select all

x = 48, y = 48, rule = B2o/S2mH:T48,48
bob2o2bo2b2o2bo3b2o2b2o6bo4b2o2b2obobob2o$obo2bobo7bob2o2b2ob2o4bo3b2o
2b2obobobo$obob2o2bo3b2obobo3bo4b2o3bob2o3bo2bobobobo$3b2o2b2o2b2obobo
b2o2b2o4b2obobo5bo2bobob2o$b2o3b2o2b2o2bobo3b2o2b2o4bobobo4bo2bobo$2ob
ob2o2b2o4bobo4bo3b2o2bobobo5bo2bob2o$o2bobo2b2o4b2obo4bo5b2obobobo4bo
2bo3bo$4bobobo4b2o3bo4bo2b2o2b2obobo5bo2bo$2o2bobo2b2ob2o4bo3b2ob2ob2o
4bob2o3bo2bo$ob2obob2o2b2o6bob2o2bo4b2ob2o3b2o2b2obobo$4b2o3b2o8bobo4b
ob2o2b2o2b2o2b2o2b2obo$o6b2o2b2o7bob2o2bobob2o3b2obo3b2o$o5b2ob2o2b2o
4b2o3b2obobo2bob2o2bo5b2o$bo3b2o4b2o2b2ob2o2b2o2b2obob2obo4bo6b2o$2o2b
2o7bo3b2o2b2ob2o4b2o3b2o2bo4b2o$3b2o8bo6b2o4bob2o3b2o2b2ob2ob2obo$2b2o
2b2o6bo4b2o2b2obobob2obob2o2bo2b2o2bo$b2o2b2ob2o4bo3b2o2b2obobobo2bobo
2bobo7bo$bo3bo4b2o3bob2o3bo2bobobob2obob2o2bo3b2obo$ob2o2b2o4b2obobo5b
o2bobob2o3b2o2b2o2b2obo$o3b2o2b2o4bobobo4bo2bobo4b2o3b2o2b2o2bo$bo4bo
3b2o2bobobo5bo2bob2ob2obob2o2b2o4bo$bo4bo5b2obobobo4bo2bo3b2o2bobo2b2o
4b2o$2bo4bo2b2o2b2obobo5bo2bo7bobobo4b2o$2bo3b2ob2ob2o4bob2o3bo2bo3b2o
2bobo2b2ob2o$3bob2o2bo4b2ob2o3b2o2b2obob2ob2obob2o2b2o$3bobo4bob2o2b2o
2b2o2b2o2b2obo4b2o3b2o$4bob2o2bobob2o3b2obo3b2o4bo6b2o2b2o$3b2o3b2obob
o2bob2o2bo5b2o2bo5b2ob2o2b2o$ob2o2b2o2b2obob2obo4bo6b2obo3b2o4b2o2bo$b
2o2b2ob2o4b2o3b2o2bo4b2o2b2o2b2o7bo$4b2o4bob2o3b2o2b2ob2ob2obo4b2o8bo$
3b2o2b2obobob2obob2o2bo2b2o2bo3b2o2b2o6bo$2b2o2b2obobobo2bobo2bobo7bob
2o2b2ob2o4bo$b2o3bo2bobobob2obob2o2bo3b2obobo3bo4b2o3bo$bo5bo2bobob2o
3b2o2b2o2b2obobob2o2b2o4b2obo$obo4bo2bobo4b2o3b2o2b2o2bobo3b2o2b2o4bo$
obo5bo2bob2ob2obob2o2b2o4bobo4bo3b2o2bo$bobo4bo2bo3b2o2bobo2b2o4b2obo
4bo5b2obo$bobo5bo2bo7bobobo4b2o3bo4bo2b2o2b2o$2bob2o3bo2bo3b2o2bobo2b
2ob2o4bo3b2ob2ob2o$b2o3b2o2b2obob2ob2obob2o2b2o6bob2o2bo4b2o$2o2b2o2b
2o2b2obo4b2o3b2o8bobo4bob2o$3b2obo3b2o4bo6b2o2b2o7bob2o2bobob2o$ob2o2b
o5b2o2bo5b2ob2o2b2o4b2o3b2obobo$obo4bo6b2obo3b2o4b2o2b2ob2o2b2o2b2obob
o$3b2o2bo4b2o2b2o2b2o7bo3b2o2b2ob2o4b2o$b2o2b2ob2ob2obo4b2o8bo6b2o4bob
2o!
Here's the patch rendered using Python turtle graphics (which should work in the demo).
Screen Shot 2021-01-19 at 3.07.02 PM.png
Screen Shot 2021-01-19 at 3.07.02 PM.png (265.55 KiB) Viewed 2754 times
I can support more than two values and was able to use this to pack rhombuses, again in a patch that can be rotated and tiled. Here's a screenshot from one run of the demo (they are intentionally non-deterministic and supply a random seed to each call to lingeling).
Screen Shot 2021-01-19 at 3.13.07 PM.png
Screen Shot 2021-01-19 at 3.13.07 PM.png (507.36 KiB) Viewed 2754 times
Finally, the symbolic format, while intentionally simple, is sufficient to express hand-written problems meaningfully. A 3-coloring of a graph can be expressed as follows:

Code: Select all

# 3-coloring graph with nodes a, b, c, d and edgea a-b, b-c, c-d, d-a, a-c

# a-b not the same color
~a(0) ~b(0)
~a(1) ~b(1)
~a(2) ~b(2)

# b-c not the same color
~b(0) ~c(0)
~b(1) ~c(1)
~b(2) ~c(2)

# c-d not the same color
~c(0) ~d(0)
~c(1) ~d(1)
~c(2) ~d(2)

# d-a not the same color
~d(0) ~a(0)
~d(1) ~a(1)
~d(2) ~a(2)

# a-c not the same color
~a(0) ~c(0)
~a(1) ~c(1)
~a(2) ~c(2)
Any comments in the symbolic file are echoed to the resulting DIMACS file, providing a guide to the compiled form of the SAT instance.

Code: Select all

p cnf 8 19
c variable a#0: 1
c variable a#1: 2
c variable b#0: 3
c variable b#1: 4
c variable c#0: 5
c variable c#1: 6
c variable d#0: 7
c variable d#1: 8
c 3-coloring graph with nodes a, b, c, d and edgea a-b, b-c, c-d, d-a, a-c
c 
c a-b not the same color
1 2 3 4 0
-1 2 -3 4 0
1 -2 3 -4 0
c 
c b-c not the same color
3 4 5 6 0
-3 4 -5 6 0
3 -4 5 -6 0
c 
c c-d not the same color
5 6 7 8 0
-5 6 -7 8 0
5 -6 7 -8 0
c 
c d-a not the same color
1 2 7 8 0
-1 2 -7 8 0
1 -2 7 -8 0
c 
c a-c not the same color
1 2 5 6 0
-1 2 -5 6 0
1 -2 5 -6 0
c Setting upper bound on tags.
-1 -2 0
-3 -4 0
-5 -6 0
-7 -8 0
Added 30 Jan 2020 Here's an example taken from Knuth's fascicle.

Code: Select all

# From Knuth: Find a sequence x1 x2 ... x8 with no three evenly spaced 0s or 1s

# spaced 1 apart
x1 x2 x3
x2 x3 x4
x3 x4 x5
x4 x5 x6
x5 x6 x7
x6 x7 x8
~x1 ~x2 ~x3
~x2 ~x3 ~x4
~x3 ~x4 ~x5
~x4 ~x5 ~x6
~x5 ~x6 ~x7
~x6 ~x7 ~x8

# spaced 2 apart
x1 x3 x5
x2 x4 x6
x3 x5 x7
x4 x6 x8
~x1 ~x3 ~x5
~x2 ~x4 ~x6
~x3 ~x5 ~x7
~x4 ~x6 ~x8

# spaced 3 apart
x1 x4 x7
x2 x5 x8
~x1 ~x4 ~x7
~x2 ~x5 ~x8
This preserves the comments in the generated DIMACS file as shown:

Code: Select all

p cnf 8 24
c variable x1: 1
c variable x2: 2
c variable x3: 3
c variable x4: 4
c variable x5: 5
c variable x6: 6
c variable x7: 7
c variable x8: 8
c From Knuth: Find a sequence x1 x2 ... x8 with no three evenly spaced 0s or 1s
c 
c spaced 1 apart
1 2 3 0
2 3 4 0
3 4 5 0
4 5 6 0
5 6 7 0
6 7 8 0
-1 -2 -3 0
-2 -3 -4 0
-3 -4 -5 0
-4 -5 -6 0
-5 -6 -7 0
-6 -7 -8 0
c 
c spaced 2 apart
1 3 5 0
2 4 6 0
3 5 7 0
4 6 8 0
-1 -3 -5 0
-2 -4 -6 0
-3 -5 -7 0
-4 -6 -8 0
c 
c spaced 3 apart
1 4 7 0
2 5 8 0
-1 -4 -7 0
-2 -5 -8 0
Last edited by pcallahan on January 30th, 2021, 3:49 pm, edited 2 times in total.

User avatar
pcallahan
Posts: 845
Joined: April 26th, 2013, 1:04 pm

Re: SymSAT, another SAT-solver-based search package

Post by pcallahan » January 20th, 2021, 9:28 pm

As an addendum, I extended the definition of templates a little so you can associate extra variables with cell constraints. E.g. these clauses

Code: Select all

  # stator is true iff two consecutive live generations
  stator$ <- G O
  ~stator$ <- ~G
  ~stator$ <- ~O
 
assign a new "stator" truth value to each cell in each generation to indicate that it stays live. So instead of merely constraining a period-2 oscillator to be a phoenix (i.e. no stators), you can put cardinality bounds on the number of stators. I added an example to the demo. (I did a lot of refactoring this morning including moving methods and changing a directory name.)

Here are some p2 oscillators, not that interesting, but which illustrate that this constraint can be used to require a certain number of stators. They were not constrained to be symmetrical, so I'm not sure why they turned out that way.

Code: Select all

x = 36, y = 10, rule = B3/S23
8b2o18bo$3o4bobo6bo3b2o6bobo2b2o$b3obo9b2o2bo6bo2bo4bo$7bo7b2o5bo8bobo
$5b2o7bob5obo3b2o$3bob2o7bo5b2o7bo3bo$3b2o2b2o8bo2b2o5b2obo2bobo$6bo8b
2o3bo8bo4bo$9bo18bo3bobo$7b2o21bobo!
I can do this with agars as well, but with stators, they're typically pretty uninteresting, consisting of isolated oscillators. Again, the point here isn't really to compete with existing Life searches but to develop a logic language expressive enough to represent many problems in this domain and compile them into input to SAT solvers.

That doesn't mean it cannot be competitive, but it might require some tweaking of clauses to help the SAT solver out. E.g., would it help to do some forward inferencing and generate clauses that skip a generation? The SAT solver has to start with a completely blank slate about how to assign values, and I'm impressed at what it can do. I wonder if there is a way to take some of the shortcuts we may know now and encode them as clauses (this idea is left intentionally vague). I especially wonder if SAT solvers can be adapted to do a Bellman-like search.

Update 21 Jan 2021: I verified that SAT solvers cadical and kissat work as drop-in replacements since they accept DIMACS files (but kissat does not have a --seed option). The code is updated so the solver is configurable, but lingeling remains the default. The others do seem to be faster. I have not benchmarked.

Update (a couple hours later)
I set up a p3 spaceship search with grid size 19x8 and a cardinality constraint that the initial population must be >=29. Performance was as follows:
  • kissat:
    c maximum-resident-set-size: 302782611456 bytes 288756 MB
    c process-time: 4m 5s 245.19 seconds
  • cadical:
    c total process time since initialization: 154.45 seconds
    c total real time since initialization: 154.62 seconds
    c maximum resident set size of process: 445384.00 MB
  • lingeling:
    c 2741.7 seconds, 162.0 MB
So timewise, lingeling is a distant third for a long-running search like this. They all found the same spaceship as expected:

Code: Select all

x = 19, y = 8, rule = B3/S23
11bo$10b4o$9bo3b2ob2o$7bo5bo2b2o$5b3o7bo2bo$b2ob2o3bo$b2o2bo2bo$o2bo!
Last edited by pcallahan on January 24th, 2021, 11:52 pm, edited 1 time in total.

User avatar
pcallahan
Posts: 845
Joined: April 26th, 2013, 1:04 pm

Re: SymSAT, another SAT-solver-based search package

Post by pcallahan » January 24th, 2021, 5:47 pm

Working with this a little further, I coded up the kind of search I really intended this for (and was working on before I decided I needed a better API), which is hexagon grid colorings using "triomino" constraints. These are constraints on mutually adjacent triples of hexagons that may be realized using a tesselation of triangles with colored vertices that need to match up as placed. I posted about this a few years ago.

Though it may be of limited interest (like just to me, not sure), it illustrates some of the features of this SAT abstraction, since it can use labels beyond binary and represents symmetries. It is included in the demo, and it can be run directly as:

python3 -m example.triominoes data/tri lingeling

which is in the repo as example/triominoes.py (Note that cadical or kissat can be used as the argument instead of lingeling if installed and in the command PATH).

Setup is a bit too programmatic for my tastes, but I'm resisting the urge to write a whole new specification language. Maybe someone has done that. SAT-solvers make me think of Prolog without unification but with much more powerful resolution, and I would like a syntax that reflects this. I am not sure how old DIMACS format is. One gets the impression they wanted something compatible with punch cards (but they were founded in 1989!).

Anyway, here's how I set up a particular set of triomino constraints (using O for center, compass directions N, E, SE, S, W, NW for Moore-embedded hex neighborhood and using SW and NE to extend the reach a little to rule out a trivial coloring that came up a lot).

Code: Select all

...
# tags for triomino matching
TRI_TAGS = [
  (1, 2, 3),
  (2, 1, 4),
  (3, 4, 1),
  (4, 3, 2),
  (0, 4, 1),
  (3, 0, 1),
  (0, 3, 2),
  (4, 0, 2),
  (1, 2, 0),
  (2, 1, 0),
]

LOWER_MATCHES = expand_symmetry(ROTATED_TRI_BELOW, all_tag_tuples((O, W, S), TRI_TAGS))
UPPER_MATCHES = expand_symmetry(ROTATED_TRI_ABOVE, all_tag_tuples((O, E, N), TRI_TAGS))
LOWER_CLAUSES = ['Clauses for lower triomino match'] + make_matching_clauses(LOWER_MATCHES)
UPPER_CLAUSES = ['Clauses for upper triomino match'] + make_matching_clauses(UPPER_MATCHES)
MISC_CLAUSES = expand_symmetry(ROTATED_HEX, parse_lines('''
  # Do not use 0 label when 3-4 cells in straight line.
  ~W(3) ~O(0) ~E(3)
  ~W(4) ~O(0) ~E(4)
  # Rule out trivial 0-1-2 coloring
  ~O(0) ~SW(0) ~NE(0) ~NW(2) ~N(1) ~E(2) ~SE(1) ~S(2) ~W(1)
  '''))

ALL_CLAUSES = LOWER_CLAUSES + UPPER_CLAUSES + MISC_CLAUSES
...
The full list of constraints on cells is quite long, and even longer when expanded out to booleans, but just grepping for comments, i.e. grep '^#' data/tri.sym, provides a somewhat more readable description. Each clause corresponds to a forbidden triple, up to symmetry. E.g. ~O(0) ~S(0) ~W(0) means at least one of the center cell, its south neighbor, or its west neighbor must not be zero. Otherwise the tags would be O(0), S(0), W(0) which is not permitted. But the clause # Template: ~O(0) ~S(1) ~W(2) is not present, because O(0), S(1), W(2) is permitted:

Code: Select all

# Clauses for lower triomino match
# Template: ~O(0) ~S(0) ~W(0)
# Template: ~O(0) ~S(0) ~W(1)
# Template: ~O(0) ~S(0) ~W(2)
# Template: ~O(0) ~S(0) ~W(3)
# Template: ~O(0) ~S(0) ~W(4)
# Template: ~O(0) ~S(1) ~W(0)
# Template: ~O(0) ~S(1) ~W(1)
# Template: ~O(0) ~S(1) ~W(3)
# Template: ~O(0) ~S(2) ~W(0)
# Template: ~O(0) ~S(2) ~W(2)
# Template: ~O(0) ~S(2) ~W(4)
# Template: ~O(0) ~S(3) ~W(0)
# Template: ~O(0) ~S(3) ~W(2)
# Template: ~O(0) ~S(3) ~W(3)
# Template: ~O(0) ~S(3) ~W(4)
# Template: ~O(0) ~S(4) ~W(0)
# Template: ~O(0) ~S(4) ~W(1)
# Template: ~O(0) ~S(4) ~W(3)
# Template: ~O(0) ~S(4) ~W(4)
# Template: ~O(1) ~S(0) ~W(0)
# Template: ~O(1) ~S(0) ~W(1)
# Template: ~O(1) ~S(0) ~W(4)
# Template: ~O(1) ~S(1) ~W(0)
# Template: ~O(1) ~S(1) ~W(1)
# Template: ~O(1) ~S(1) ~W(2)
# Template: ~O(1) ~S(1) ~W(3)
# Template: ~O(1) ~S(1) ~W(4)
# Template: ~O(1) ~S(2) ~W(1)
# Template: ~O(1) ~S(2) ~W(2)
# Template: ~O(1) ~S(2) ~W(3)
# Template: ~O(1) ~S(3) ~W(0)
# Template: ~O(1) ~S(3) ~W(1)
# Template: ~O(1) ~S(3) ~W(3)
# Template: ~O(1) ~S(3) ~W(4)
# Template: ~O(1) ~S(4) ~W(1)
# Template: ~O(1) ~S(4) ~W(2)
# Template: ~O(1) ~S(4) ~W(4)
# Template: ~O(2) ~S(0) ~W(0)
# Template: ~O(2) ~S(0) ~W(2)
# Template: ~O(2) ~S(0) ~W(3)
# Template: ~O(2) ~S(1) ~W(1)
# Template: ~O(2) ~S(1) ~W(2)
# Template: ~O(2) ~S(1) ~W(4)
# Template: ~O(2) ~S(2) ~W(0)
# Template: ~O(2) ~S(2) ~W(1)
# Template: ~O(2) ~S(2) ~W(2)
# Template: ~O(2) ~S(2) ~W(3)
# Template: ~O(2) ~S(2) ~W(4)
# Template: ~O(2) ~S(3) ~W(1)
# Template: ~O(2) ~S(3) ~W(2)
# Template: ~O(2) ~S(3) ~W(3)
# Template: ~O(2) ~S(4) ~W(0)
# Template: ~O(2) ~S(4) ~W(2)
# Template: ~O(2) ~S(4) ~W(3)
# Template: ~O(2) ~S(4) ~W(4)
# Template: ~O(3) ~S(0) ~W(0)
# Template: ~O(3) ~S(0) ~W(1)
# Template: ~O(3) ~S(0) ~W(3)
# Template: ~O(3) ~S(0) ~W(4)
# Template: ~O(3) ~S(1) ~W(1)
# Template: ~O(3) ~S(1) ~W(2)
# Template: ~O(3) ~S(1) ~W(3)
# Template: ~O(3) ~S(2) ~W(0)
# Template: ~O(3) ~S(2) ~W(2)
# Template: ~O(3) ~S(2) ~W(3)
# Template: ~O(3) ~S(2) ~W(4)
# Template: ~O(3) ~S(3) ~W(0)
# Template: ~O(3) ~S(3) ~W(1)
# Template: ~O(3) ~S(3) ~W(2)
# Template: ~O(3) ~S(3) ~W(3)
# Template: ~O(3) ~S(3) ~W(4)
# Template: ~O(3) ~S(4) ~W(0)
# Template: ~O(3) ~S(4) ~W(1)
# Template: ~O(3) ~S(4) ~W(3)
# Template: ~O(3) ~S(4) ~W(4)
# Template: ~O(4) ~S(0) ~W(0)
# Template: ~O(4) ~S(0) ~W(2)
# Template: ~O(4) ~S(0) ~W(3)
# Template: ~O(4) ~S(0) ~W(4)
# Template: ~O(4) ~S(1) ~W(0)
# Template: ~O(4) ~S(1) ~W(1)
# Template: ~O(4) ~S(1) ~W(3)
# Template: ~O(4) ~S(1) ~W(4)
# Template: ~O(4) ~S(2) ~W(1)
# Template: ~O(4) ~S(2) ~W(2)
# Template: ~O(4) ~S(2) ~W(4)
# Template: ~O(4) ~S(3) ~W(0)
# Template: ~O(4) ~S(3) ~W(2)
# Template: ~O(4) ~S(3) ~W(3)
# Template: ~O(4) ~S(3) ~W(4)
# Template: ~O(4) ~S(4) ~W(0)
# Template: ~O(4) ~S(4) ~W(1)
# Template: ~O(4) ~S(4) ~W(2)
# Template: ~O(4) ~S(4) ~W(3)
# Template: ~O(4) ~S(4) ~W(4)
# Clauses for upper triomino match
# Template: ~E(0) ~N(0) ~O(0)
# Template: ~E(0) ~N(0) ~O(1)
# Template: ~E(0) ~N(0) ~O(2)
# Template: ~E(0) ~N(0) ~O(3)
# Template: ~E(0) ~N(0) ~O(4)
# Template: ~E(0) ~N(1) ~O(0)
# Template: ~E(0) ~N(1) ~O(1)
# Template: ~E(0) ~N(1) ~O(4)
# Template: ~E(0) ~N(2) ~O(0)
# Template: ~E(0) ~N(2) ~O(2)
# Template: ~E(0) ~N(2) ~O(3)
# Template: ~E(0) ~N(3) ~O(0)
# Template: ~E(0) ~N(3) ~O(1)
# Template: ~E(0) ~N(3) ~O(3)
# Template: ~E(0) ~N(3) ~O(4)
# Template: ~E(0) ~N(4) ~O(0)
# Template: ~E(0) ~N(4) ~O(2)
# Template: ~E(0) ~N(4) ~O(3)
# Template: ~E(0) ~N(4) ~O(4)
# Template: ~E(1) ~N(0) ~O(0)
# Template: ~E(1) ~N(0) ~O(1)
# Template: ~E(1) ~N(0) ~O(3)
# Template: ~E(1) ~N(1) ~O(0)
# Template: ~E(1) ~N(1) ~O(1)
# Template: ~E(1) ~N(1) ~O(2)
# Template: ~E(1) ~N(1) ~O(3)
# Template: ~E(1) ~N(1) ~O(4)
# Template: ~E(1) ~N(2) ~O(1)
# Template: ~E(1) ~N(2) ~O(2)
# Template: ~E(1) ~N(2) ~O(4)
# Template: ~E(1) ~N(3) ~O(1)
# Template: ~E(1) ~N(3) ~O(2)
# Template: ~E(1) ~N(3) ~O(3)
# Template: ~E(1) ~N(4) ~O(0)
# Template: ~E(1) ~N(4) ~O(1)
# Template: ~E(1) ~N(4) ~O(3)
# Template: ~E(1) ~N(4) ~O(4)
# Template: ~E(2) ~N(0) ~O(0)
# Template: ~E(2) ~N(0) ~O(2)
# Template: ~E(2) ~N(0) ~O(4)
# Template: ~E(2) ~N(1) ~O(1)
# Template: ~E(2) ~N(1) ~O(2)
# Template: ~E(2) ~N(1) ~O(3)
# Template: ~E(2) ~N(2) ~O(0)
# Template: ~E(2) ~N(2) ~O(1)
# Template: ~E(2) ~N(2) ~O(2)
# Template: ~E(2) ~N(2) ~O(3)
# Template: ~E(2) ~N(2) ~O(4)
# Template: ~E(2) ~N(3) ~O(0)
# Template: ~E(2) ~N(3) ~O(2)
# Template: ~E(2) ~N(3) ~O(3)
# Template: ~E(2) ~N(3) ~O(4)
# Template: ~E(2) ~N(4) ~O(1)
# Template: ~E(2) ~N(4) ~O(2)
# Template: ~E(2) ~N(4) ~O(4)
# Template: ~E(3) ~N(0) ~O(0)
# Template: ~E(3) ~N(0) ~O(2)
# Template: ~E(3) ~N(0) ~O(3)
# Template: ~E(3) ~N(0) ~O(4)
# Template: ~E(3) ~N(1) ~O(0)
# Template: ~E(3) ~N(1) ~O(1)
# Template: ~E(3) ~N(1) ~O(3)
# Template: ~E(3) ~N(1) ~O(4)
# Template: ~E(3) ~N(2) ~O(1)
# Template: ~E(3) ~N(2) ~O(2)
# Template: ~E(3) ~N(2) ~O(3)
# Template: ~E(3) ~N(3) ~O(0)
# Template: ~E(3) ~N(3) ~O(1)
# Template: ~E(3) ~N(3) ~O(2)
# Template: ~E(3) ~N(3) ~O(3)
# Template: ~E(3) ~N(3) ~O(4)
# Template: ~E(3) ~N(4) ~O(0)
# Template: ~E(3) ~N(4) ~O(2)
# Template: ~E(3) ~N(4) ~O(3)
# Template: ~E(3) ~N(4) ~O(4)
# Template: ~E(4) ~N(0) ~O(0)
# Template: ~E(4) ~N(0) ~O(1)
# Template: ~E(4) ~N(0) ~O(3)
# Template: ~E(4) ~N(0) ~O(4)
# Template: ~E(4) ~N(1) ~O(1)
# Template: ~E(4) ~N(1) ~O(2)
# Template: ~E(4) ~N(1) ~O(4)
# Template: ~E(4) ~N(2) ~O(0)
# Template: ~E(4) ~N(2) ~O(2)
# Template: ~E(4) ~N(2) ~O(3)
# Template: ~E(4) ~N(2) ~O(4)
# Template: ~E(4) ~N(3) ~O(0)
# Template: ~E(4) ~N(3) ~O(1)
# Template: ~E(4) ~N(3) ~O(3)
# Template: ~E(4) ~N(3) ~O(4)
# Template: ~E(4) ~N(4) ~O(0)
# Template: ~E(4) ~N(4) ~O(1)
# Template: ~E(4) ~N(4) ~O(2)
# Template: ~E(4) ~N(4) ~O(3)
# Template: ~E(4) ~N(4) ~O(4)
# Do not use 0 label when 3-4 cells in straight line.
# Template: ~S(3) ~O(0) ~N(3)
# Template: ~SE(3) ~O(0) ~NW(3)
# Template: ~W(3) ~O(0) ~E(3)
# Template: ~S(4) ~O(0) ~N(4)
# Template: ~SE(4) ~O(0) ~NW(4)
# Template: ~W(4) ~O(0) ~E(4)
# Rule out trivial 0-1-2 coloring
# Template: ~O(0) ~SW(0) ~NE(0) ~NW(2) ~N(1) ~E(2) ~SE(1) ~S(2) ~W(1)
# Template: ~O(0) ~SW(0) ~NE(0) ~W(2) ~NW(1) ~N(2) ~E(1) ~SE(2) ~S(1)
# Setting upper bound on tags.
These triominoes (described here) seem too rigid to be universal, but I think they make appealing decorative patterns, depending on the periodicity you choose. What seems to work best is Toroidal wrapping with a negative shift equal to half the height of the torus. For example:
Screen Shot 2021-01-24 at 1.41.41 PM.png
Screen Shot 2021-01-24 at 1.41.41 PM.png (554.3 KiB) Viewed 2617 times
One thing I observed at the time, though I may not have posted about it, is that this coloring partitions the plane into parallelograms like this:
Screen Shot 2021-01-24 at 2.04.18 PM.png
Screen Shot 2021-01-24 at 2.04.18 PM.png (755.94 KiB) Viewed 2613 times
This makes it sort of uninteresting (I think) from the standpoint of universal computation. It also makes it pretty hard to build periodic patterns by hand, though there may be a special purpose algorithm. The general applicability of SAT solvers make them appealing.

When I was working on this a few years back, I had a couple of hacky search methods. One was a little like simulated annealing, and another was either recursive backtracking or possibly more like dynamic programming, storing a whole row at a time and extending from it (I don't really remember). They were both pretty limited. A SAT solver (kissat) finds this one in under 22 seconds, though it takes a lot longer including the time to construct the symbolic and DIMACS input formats. It is based on a 42x43 torus with a shift of 21 columns.
Screen Shot 2021-01-24 at 7.18.37 PM.png
Screen Shot 2021-01-24 at 7.18.37 PM.png (1.28 MiB) Viewed 2583 times

User avatar
dexter1
Posts: 71
Joined: February 26th, 2020, 8:46 am

Re: SymSAT, another SAT-solver-based search package

Post by dexter1 » January 26th, 2021, 9:45 am

I would like to comment on the fact that you have written a nice software tool to help in creating specific DIMACS input to be solved by SAT solvers. Thank you!

My use of logic-life-search has been hampered a bit by specifying the input file as many rows and columns of 0's and symbols. It is easy to make a mistake in that file if you do this by hand. So, having this tool to create DIMACS files more easily, I could perhaps use this in finding diagonal glide-reflect ships for certain speeds.
Frank Everdij

User avatar
pcallahan
Posts: 845
Joined: April 26th, 2013, 1:04 pm

Re: SymSAT, another SAT-solver-based search package

Post by pcallahan » January 26th, 2021, 1:09 pm

dexter1 wrote:
January 26th, 2021, 9:45 am
So, having this tool to create DIMACS files more easily, I could perhaps use this in finding diagonal glide-reflect ships for certain speeds.
I appreciate your interest. Let me know if you want to implement any general-purpose features to contribute to the code base.

I have not added any way to assign symmetry within the grid, though you might be able to handle glide reflection by defining a tessellation. For spaceships, the "PeriodicTimeAdjust" object could be augmented to include transformations other than just translation. I just haven't had a chance to do it.

A more direct approach is to add clauses that require two variables to be equal. I.e.: "~a b" and "a ~b" (equivalently ~a <- ~b, a <- b). I would guess that SAT solvers are pretty good at picking these up and eliminating variables. Alternatively, equivalence classes of variables could be dealt with as a post-processing step on the input. I'm not sure which is better. (My experience with SAT solvers is limited to a few months and I still have not read Knuth's chapter on them.)

Hooloovoo
Posts: 38
Joined: July 11th, 2015, 8:59 pm

Re: SymSAT, another SAT-solver-based search package

Post by Hooloovoo » February 24th, 2021, 5:48 pm

I defininitely agree that a standard way to specify SAT problems would be useful for CA problems, however I think it's hard to represent it without writing code. From experience: I've tried to use ikpx, lls, and lsss for various problems (mostly unsuccessfully). For most, I had to write code to produce a useful problem definition (and the problem definition sometimes depends on the approach). I haven't looked specifically at symsat's code/interface or tried to use it yet though - I will look through the examples directory later tonight.

I noticed one thing about the SAT solver performance results:
pcallahan wrote:
January 20th, 2021, 9:28 pm
  • kissat:
    c maximum-resident-set-size: 302782611456 bytes 288756 MB
    c process-time: 4m 5s 245.19 seconds
  • cadical:
    c total process time since initialization: 154.45 seconds
    c total real time since initialization: 154.62 seconds
    c maximum resident set size of process: 445384.00 MB
  • lingeling:
    c 2741.7 seconds, 162.0 MB
So timewise, lingeling is a distant third for a long-running search like this. They all found the same spaceship as expected:a
Lingeling is the only one which didn't take a large amount of RAM: it could run on an average person's computer, while the others appear to need hundreds of gigabytes of RAM (unless I'm misreading something). Even though it takes a lot longer, it might be possible to run many more threads of it on a large computer, with better average performance.

User avatar
pcallahan
Posts: 845
Joined: April 26th, 2013, 1:04 pm

Re: SymSAT, another SAT-solver-based search package

Post by pcallahan » February 24th, 2021, 10:40 pm

Hooloovoo wrote:
February 24th, 2021, 5:48 pm
Lingeling is the only one which didn't take a large amount of RAM: it could run on an average person's computer, while the others appear to need hundreds of gigabytes of RAM (unless I'm misreading something). Even though it takes a lot longer, it might be possible to run many more threads of it on a large computer, with better average performance.
They all ran on a MacBook Pro. I am not sure how to read the memory stats. Is it swap size, a mistake, or does it just mean something entirely different from what it looks like?

I am not doing this on a supercomputer. In practice, cadical seems like the best choice in most of the tests I've run.
I defininitely agree that a standard way to specify SAT problems would be useful for CA problems, however I think it's hard to represent it without writing code.
It would be good to have a programming language in which SAT clauses could be written directly or generated, including from templates, i.e. something like Prolog but not limited to Horn clauses. This is well beyond the scope of anything I can work on. I think I have this project in a state where I can proceed on triomino tilings effectively. I have put it aside (and out of my mind) for a few weeks as I try to be more productive with my actual job.

Post Reply