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:
- Install lingeling, e.g. by following these instructions: https://www.conwaylife.com/wiki/Tutoria ... _Lingeling
- 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 ..." - git clone https://github.com/PaulBC/grid-sat-solver
- cd grid-sat-solver
- python demo.py
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
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!
Code: Select all
# no two consecutive live generations
~G ~O
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!
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!
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)
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
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
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