ConwayLife.com - A community for Conway's Game of Life and related cellular automata
Home  •  LifeWiki  •  Forums  •  Download Golly

Yet another search program (with hexagons!)

For scripts to aid with computation or simulation in cellular automata.

Yet another search program (with hexagons!)

Postby strake » May 1st, 2018, 4:23 am

The goods

I was tired of not having a search program for hexagonal rules, so i hacked this up over the past few days.
It's essentially a z3 driver: it declares a variable per cell and plugs in the constraints, and z3 emits patterns! Cheers!

P.S. It already disproved a few conjectures of mine about certain hexagonal rules, but i haven't slept in 36 hours so the post will have to wait.

== NEWS ==

August 21st 2018:
Now accepts symmetry constraints with g flag.

August 20th 2018:
Can now search in the Moore neighborhood — use Hensel notation.
Last edited by strake on August 23rd, 2018, 3:51 am, edited 2 times in total.
strake
 
Posts: 26
Joined: October 8th, 2014, 7:47 am
Location: Mountain View, California

Re: Yet another search program (with hexagons!)

Postby Saka » May 1st, 2018, 4:37 am

Excellent!
Although I haven't tried it yet.
I'm assuming z3 is a SAT Solver or something similar?
If you're the person that uploaded to Sakagolue illegally, please PM me.
x = 17, y = 10, rule = B3/S23
b2ob2obo5b2o$11b4obo$2bob3o2bo2b3o$bo3b2o4b2o$o2bo2bob2o3b4o$bob2obo5b
o2b2o$2b2o4bobo2b3o$bo3b5ob2obobo$2bo5bob2o$4bob2o2bobobo!

(Check gen 2)
User avatar
Saka
 
Posts: 3075
Joined: June 19th, 2015, 8:50 pm
Location: In the kingdom of Sultan Hamengkubuwono X

Re: Yet another search program (with hexagons!)

Postby Macbi » May 1st, 2018, 5:53 am

Neat! I was thinking of using z3 for LLS too, but I found that other SAT solvers were a tad faster. Using z3 probably makes it a lot easier to encode various constraints. Very cool program!
User avatar
Macbi
 
Posts: 685
Joined: March 29th, 2009, 4:58 am

Re: Yet another search program (with hexagons!)

Postby Macbi » May 1st, 2018, 5:56 am

Saka wrote:Excellent!
Although I haven't tried it yet.
I'm assuming z3 is a SAT Solver or something similar?
z3 is an "SMT" solver, which means it can handle constrains which are a bit more flexible than just ANDs and ORs. For example if you want to express a "cardinality constraint" (for example, "at least 30 out of these 60 variables are TRUE") then z3 can do this automatically. (I mentioned over in the LLS thread about how normal SAT solvers have difficulties with that sort of thing.) Although I think that the way z3 works is that it converts everything to SAT and applies a SAT solver.
User avatar
Macbi
 
Posts: 685
Joined: March 29th, 2009, 4:58 am

Re: Yet another search program (with hexagons!)

Postby Saka » May 1st, 2018, 6:07 am

I get this error while compiling z3
sakaf@Arfie-Surface /z3/z3/build
$ sudo make install
-bash: $'\302\203sudo': command not found

I'm using cygwin
EDIT: Oh, cygwin doesnt use sudo. Problem solved
If you're the person that uploaded to Sakagolue illegally, please PM me.
x = 17, y = 10, rule = B3/S23
b2ob2obo5b2o$11b4obo$2bob3o2bo2b3o$bo3b2o4b2o$o2bo2bob2o3b4o$bob2obo5b
o2b2o$2b2o4bobo2b3o$bo3b5ob2obobo$2bo5bob2o$4bob2o2bobobo!

(Check gen 2)
User avatar
Saka
 
Posts: 3075
Joined: June 19th, 2015, 8:50 pm
Location: In the kingdom of Sultan Hamengkubuwono X

Re: Yet another search program (with hexagons!)

Postby Saka » May 2nd, 2018, 5:32 am

I got this error when doing "stack build"
Network.Socket.recvBuf: does not exist (No such file or directory)
If you're the person that uploaded to Sakagolue illegally, please PM me.
x = 17, y = 10, rule = B3/S23
b2ob2obo5b2o$11b4obo$2bob3o2bo2b3o$bo3b2o4b2o$o2bo2bob2o3b4o$bob2obo5b
o2b2o$2b2o4bobo2b3o$bo3b5ob2obobo$2bo5bob2o$4bob2o2bobobo!

(Check gen 2)
User avatar
Saka
 
Posts: 3075
Joined: June 19th, 2015, 8:50 pm
Location: In the kingdom of Sultan Hamengkubuwono X

Re: Yet another search program (with hexagons!)

Postby wildmyron » May 2nd, 2018, 6:52 am

Saka wrote:I got this error when doing "stack build"
Network.Socket.recvBuf: does not exist (No such file or directory)

I think you're asking for trouble if you try to build yfind with anything to do with cygwin, except for maybe using git within cygwin to initially checkout the source.

Are you trying to run stack from within the cygwin environment? I guess that will probably work, but you won't be able to link yfind against a library built with cygwin. https://github.com/commercialhaskell/stack/issues/1714 and related issues may be relevant.

There are actually binary releases of Z3 available for Win x64, but I haven't yet figured out which release version will work best. The Haskell Z3 wrapper seems to target v4.3 (unless the version numbering is independent?), but doesn't appear to be fully compatible with it. I managed to build Z3 from current source, and that almost works, but when yfind finds a solution it crashes with an error related to conversion of Z3_BOOL to BOOL [Sorry, didn't save a copy of that message and don't currently have that environment available to test] In fact, some of the examples provided with the Z3 package crashed in the same way, in particular FourQueens and AllFourQueens, so it's not specifically a yfind problem.

Anyway, great to see another program like this being developed and look forward to seeing some results.
The latest version of the 5S Project contains over 196,000 spaceships. Tabulated pages up to period 160 are available on the LifeWiki.
wildmyron
 
Posts: 1209
Joined: August 9th, 2013, 12:45 am

Re: Yet another search program (with hexagons!)

Postby wildmyron » May 3rd, 2018, 1:43 am

wildmyron wrote:
Saka wrote:I got this error when doing "stack build"
Network.Socket.recvBuf: does not exist (No such file or directory)

I think you're asking for trouble if you try to build yfind with anything to do with cygwin, except for maybe using git within cygwin to initially checkout the source.

Are you trying to run stack from within the cygwin environment? I guess that will probably work, but you won't be able to link yfind against a library built with cygwin. https://github.com/commercialhaskell/stack/issues/1714 and related issues may be relevant.

I may have been jumping the gun here, in light of not reading the rest of the README for Z3 - it seems you can cross compile for Windows using the mingw-64 toolset. However, that turns out to be unnecessary to get yfind working on Windows, because you can just use the v4.6.0 binary Release distributed by the Z3 team. Make sure to get the x64 version. Extract the folder in the zipfile and put it somewhere sensible, I also renamed it to z3-4.6.0 . If your system does not have MSVCR110.dll, you will also need the MSVC 2012 Redistributable (Again, get the x64 version). Assuming stack is already installed (64bit version, of course), you can now build yfind with the following command in a console:
cd $YFIND_SRC_DIR
stack build --copy-bins --extra-include-dirs $PATH_TO_Z3-4.6.0\include --extra-lib-dirs $PATH_TO_Z3-4.6.0\bin

where $YFIND_SRC_DIR is the directory containing yfind source code and $PATH_TO_Z3-4.6.0 is the path to the Z3 folder installed above. Make sure to escape any spaces in the path or surround path by "". This will build yfind and install to %APP_DATA%\local\bin - which is a bit of a strange place, but is the default bin dir for stack. To run yfind, either copy the libz3.dll to the same directory as yfind.exe or copy it to the Windows\SYSTEM32 dir and register it with Windows (untested by me).

For reference, the error I get when running yfind with the Z3 dll built from current master using MSVC 2017 is:
yfind: Z3.Base.toBool: illegal `Z3_bool' value
CallStack (from HasCallStack):
  error, called at src\Z3\Base.hs:3197:23 in z3-4.3-IfCYH1bfb0wLv1j6xdboui:Z3.Base


@strake: Thank you again for releasing this search tool. I see that the way the search is set up requires a live cell on the top row, which means the x dimension of the search regulates the search run time in the same way the width does for other -find programs. My first interesting result with the program is a p3 oscillator in B2/S2op (aka 22da), which I'm posting in the thread (even though it's been inactive for years).
The latest version of the 5S Project contains over 196,000 spaceships. Tabulated pages up to period 160 are available on the LifeWiki.
wildmyron
 
Posts: 1209
Joined: August 9th, 2013, 12:45 am

Re: Yet another search program (with hexagons!)

Postby strake » May 3rd, 2018, 8:54 am

wildmyron wrote:I see that the way the search is set up requires a live cell on the top row, which means the x dimension of the search regulates the search run time in the same way the width does for other -find programs.


I'm not sure it's so smart — it blithely finds patterns of multiple non-interacting parts, which means it is effectively searching the full space at once. I have a few potential modifications in mind:
• incremental search/progressively larger spaces
• atomicity constraint (i.e. no multiple non-interacting parts)

The former should be easy. The latter is easy as a post-filter (and already implemented actually, just need to clean up and publish) but not so easy to formulate in SAT — the naïve formulation would have n! terms, where n is number of cells; i have a few ideas involving the richer theories of Z3 but am not sure yet how they will perform (if at all).
strake
 
Posts: 26
Joined: October 8th, 2014, 7:47 am
Location: Mountain View, California

Re: Yet another search program (with hexagons!)

Postby wildmyron » August 22nd, 2018, 5:22 pm

strake wrote:I'm not sure it's so smart — it blithely finds patterns of multiple non-interacting parts, which means it is effectively searching the full space at once.
Ahh, I see what you mean, however it still seems to help in some situations where a grid like 10x20 is often much faster than 20x10.
The latest version of the 5S Project contains over 196,000 spaceships. Tabulated pages up to period 160 are available on the LifeWiki.
wildmyron
 
Posts: 1209
Joined: August 9th, 2013, 12:45 am

Re: Yet another search program (with hexagons!)

Postby strake » August 22nd, 2018, 5:32 pm

I just modified it to formulate the evolutionary rule as a z3 function ­— search might be a little speedier now.

Upcoming features:

  • Ability to specify a rule range rather than a single rule, like LLS — this will allow asking questions such as this example: which D₆-symmetric hexagonal rules support small speed-1/2 orthogonal gliders?
  • Rules with more than 2 states
strake
 
Posts: 26
Joined: October 8th, 2014, 7:47 am
Location: Mountain View, California

Re: Yet another search program (with hexagons!)

Postby AlephAlpha » September 6th, 2018, 12:40 am

While building util-primitive-0.1.0.0, it said:

        Variable not in scope: unsafeInterleave :: f0 [a] -> m b
       |
    13 |     go = mma >>= unsafeInterleave . \ case
       |                  ^^^^^^^^^^^^^^^^
AlephAlpha
 
Posts: 31
Joined: October 6th, 2017, 1:50 am

Re: Yet another search program (with hexagons!)

Postby wildmyron » September 8th, 2018, 1:27 am

AlephAlpha wrote:While building util-primitive-0.1.0.0, it said:

        Variable not in scope: unsafeInterleave :: f0 [a] -> m b
       |
    13 |     go = mma >>= unsafeInterleave . \ case
       |                  ^^^^^^^^^^^^^^^^

This is because the referenced commit for the primitive repo doesn't exist. It has been merged into the main repo though. In stack.yaml, replace:
- git: https://github.com/strake/primitive.hs
commit: a43f1f488c78ffdb3acb607df703df16533fe7db

with
- git: https://github.com/haskell/primitive
commit: fb594e9897e4bf9ef7105502c04f6e438bd5fb1b


@strake: Nice to see you making some progress with this program. I hoped to try out searches on Moore neighbourhood rules which you seem to have been working on, but I gather from the lack of any results being output by the search that this is still a WIP.
The latest version of the 5S Project contains over 196,000 spaceships. Tabulated pages up to period 160 are available on the LifeWiki.
wildmyron
 
Posts: 1209
Joined: August 9th, 2013, 12:45 am

Re: Yet another search program (with hexagons!)

Postby AlephAlpha » September 9th, 2018, 9:16 am

wildmyron wrote:
AlephAlpha wrote:While building util-primitive-0.1.0.0, it said:

        Variable not in scope: unsafeInterleave :: f0 [a] -> m b
       |
    13 |     go = mma >>= unsafeInterleave . \ case
       |                  ^^^^^^^^^^^^^^^^

This is because the referenced commit for the primitive repo doesn't exist. It has been merged into the main repo though. In stack.yaml, replace:
- git: https://github.com/strake/primitive.hs
commit: a43f1f488c78ffdb3acb607df703df16533fe7db

with
- git: https://github.com/haskell/primitive
commit: fb594e9897e4bf9ef7105502c04f6e438bd5fb1b


@strake: Nice to see you making some progress with this program. I hoped to try out searches on Moore neighbourhood rules which you seem to have been working on, but I gather from the lack of any results being output by the search that this is still a WIP.


Thank you very much.

Now util-primitive-0.1.0.0 is built successfully. But when building yfind, I got a bunch of undefined reference errors:

/home/alephalpha/文档/CellularAutomata/yfind/.stack-work/install/x86_64-linux/lts-12.7/8.4.3/lib/x86_64-linux-ghc-8.4.3/ez3-0.1.0.0-FqbFYnJrQmaAsx290enwpR/libHSez3-0.1.0.0-FqbFYnJrQmaAsx290enwpR.a(Tagged.o):ezz3zm0zi1zi0zi0zmFqbFYnJrQmaAsx290enwpR_ZZ3ziTagged_zdwmkInterpolant_info: 错误: 对‘Z3_mk_interpolant’未定义的引用


And finally it said:

`gcc' failed in phase `Linker'. (Exit code: 1)


I am already using the newest version of stack and z3. The version of gcc i am using is 7.3.0-16ubuntu3.
AlephAlpha
 
Posts: 31
Joined: October 6th, 2017, 1:50 am


Return to Scripts

Who is online

Users browsing this forum: No registered users and 1 guest