Logic CA Search - A SAT solver for alternating HROT rules

[lemon41625]

I've been working on this program for a few days now. I would like to thank Mateon1 for helping me with CNF and debugging and WildMyron for the original idea.

Download here: https://github.com/jedlimlx/Logic-Cellu ... ton-Search

Installation
LCAS depends on PySAT and requires Python 3.6 or higher.

If you're on Windows 10 and already have Python 3 installed, run "pip install python-sat" in your cmd.
If you don't already have Python 3 try using WSL.

If that doesn't work (it probably won't) or you are on Linux, go to Windows Subsystems for Linux (if you are on Windows 10)
Run these commands:

Code: Select all

sudo apt-get update
sudo apt-get install python3.6-dev
sudo apt install python3-pip
sudo apt-get install zlib1g-dev
pip3 install python-sat

Don't be alarmed if there are warnings produced by "pip3 install python-sat". Just let it run to completion.

To use the application, run

Code: Select all

python main.py -p <period> -dx <displace_x> -dy <displace_y> -x <bound_x> -y <bound_y>

Run

Code: Select all

python main.py --help

for more options

If there are any issues with installation, let me know, I'll try to help you install it.

The rule format is the same as CAViewer's rule.ca_rule format. You will need to specify a rule file with the relevant rule to run the program. If no rule is specified it defaults to rule.ca_rule.

Features

• Support for alternating HROT rules
• Automatic generation of pattern files for spaceship searches
• Support for C1, D2-, D2|, D4+ symmetry
• Support for Flip| transformation
• Support for Glucose4, Glucose3, Lingeling, Cadical, Minisat and MapleSAT

TODO

• Partial rules
• Isotropic Non-Totalistic Rules
• Anisotropic Non-Totalistic Rules
• Multistate Rules
• More symmetries and transformations
• Background generation (Zebra Strips, Chicken Wire)
• Pattern generation for backsearches

Rule Support
Supports alternating HROT rules (B0 can be searched by alternating relevent rules)
You can also alternate between different neighbourhoods and you can alternate as many times as you want.

Speed
Finds the following ship in R2,C2,S2,7,12,B3,8,NN in a 7x7 bounding box in 34s (Cadical), 17s (Minisat), 79s (Glucose4)

Code: Select all

x = 18, y = 16, rule = R2,C2,S2,7,10,B3,8,NN
..................$
..................$
..................$
..................$
..................$
..................$
........o.o.......$
.....oo...oo......$
..................$
.........o........$
..................$
..................$
..................$
..................$
..................$
..................$

Finds the c/5o in Minibugs in 16 mins on C1 search with Glucose4

Code: Select all

x = 13, y = 15, rule = R2,C2,M0,S6..9,B7..8,NM
.............$
.............$
.............$
.............$
.............$
.............$
.....ooo.....$
....o...o....$
....oo.oo....$
.....ooo.....$
.............$
.............$
.............$
.............$
.............$

Finds c/2o from 2c/4o C1 search in a bounding box that I don't remember after 500s with cadical

Code: Select all

x = 15, y = 17, rule = R2,C2,S2,4,12,B3,8,NN
...............$
...............$
...............$
...............$
...............$
...............$
...............$
.....o...o.....$
.....ooooo.....$
....oo...oo....$
.....oo.oo.....$
...............$
...............$
...............$
...............$
...............$
...............$
!

c/2o in Far Corners B3/S23 found by Saka found in 3 mins judging from the timing between posts

Code: Select all

x = 10, y = 8, rule = R2,C2,S2-3,B3,N@891891
6b3o$6b3o$6bo2bo$7b3o$2obo3b2o$bob2obo$o2bo$obo!

[lemon41625]

Update v1.1

Added D2-, D2|, D4+ symmetries
Added Flip| transformation
Added force change parameter so that oscillator searches don't return still lives
Added num solutions parameter to search for multiple solutions

Download here: https://github.com/jedlimlx/Logic-Cellu ... ton-Search

[lemon41625]

Update v1.2

• Added weighted rules (including weighted B0 in theory)
• Added B0 rules
• Added partial rules (broken)
• Added population bounds (broken)

Download here: https://github.com/jedlimlx/Logic-Cellu ... ton-Search