Yet another search program (with hexagons!)

For scripts to aid with computation or simulation in cellular automata.
Post Reply
strake
Posts: 26
Joined: October 8th, 2014, 7:47 am
Location: Mountain View, California
Contact:

Yet another search program (with hexagons!)

Post by 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.

User avatar
Saka
Posts: 3627
Joined: June 19th, 2015, 8:50 pm
Location: Indonesia
Contact:

Re: Yet another search program (with hexagons!)

Post by 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?

User avatar
Macbi
Posts: 903
Joined: March 29th, 2009, 4:58 am

Re: Yet another search program (with hexagons!)

Post by 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: 903
Joined: March 29th, 2009, 4:58 am

Re: Yet another search program (with hexagons!)

Post by 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
Saka
Posts: 3627
Joined: June 19th, 2015, 8:50 pm
Location: Indonesia
Contact:

Re: Yet another search program (with hexagons!)

Post by Saka » May 1st, 2018, 6:07 am

I get this error while compiling z3

Code: Select all

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

User avatar
Saka
Posts: 3627
Joined: June 19th, 2015, 8:50 pm
Location: Indonesia
Contact:

Re: Yet another search program (with hexagons!)

Post by Saka » May 2nd, 2018, 5:32 am

I got this error when doing "stack build"

Code: Select all

Network.Socket.recvBuf: does not exist (No such file or directory)

wildmyron
Posts: 1542
Joined: August 9th, 2013, 12:45 am
Location: Western Australia

Re: Yet another search program (with hexagons!)

Post by wildmyron » May 2nd, 2018, 6:52 am

Saka wrote:I got this error when doing "stack build"

Code: Select all

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 5S project (Smallest Spaceships Supporting Specific Speeds) is now maintained by AforAmpere. The latest collection is hosted on GitHub and contains well over 1,000,000 spaceships.

Semi-active here - recovering from a severe case of LWTDS.

wildmyron
Posts: 1542
Joined: August 9th, 2013, 12:45 am
Location: Western Australia

Re: Yet another search program (with hexagons!)

Post by wildmyron » May 3rd, 2018, 1:43 am

wildmyron wrote:
Saka wrote:I got this error when doing "stack build"

Code: Select all

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:

Code: Select all

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:

Code: Select all

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 5S project (Smallest Spaceships Supporting Specific Speeds) is now maintained by AforAmpere. The latest collection is hosted on GitHub and contains well over 1,000,000 spaceships.

Semi-active here - recovering from a severe case of LWTDS.

strake
Posts: 26
Joined: October 8th, 2014, 7:47 am
Location: Mountain View, California
Contact:

Re: Yet another search program (with hexagons!)

Post by 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).

wildmyron
Posts: 1542
Joined: August 9th, 2013, 12:45 am
Location: Western Australia

Re: Yet another search program (with hexagons!)

Post by 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 5S project (Smallest Spaceships Supporting Specific Speeds) is now maintained by AforAmpere. The latest collection is hosted on GitHub and contains well over 1,000,000 spaceships.

Semi-active here - recovering from a severe case of LWTDS.

strake
Posts: 26
Joined: October 8th, 2014, 7:47 am
Location: Mountain View, California
Contact:

Re: Yet another search program (with hexagons!)

Post by 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

AlephAlpha
Posts: 66
Joined: October 6th, 2017, 1:50 am

Re: Yet another search program (with hexagons!)

Post by AlephAlpha » September 6th, 2018, 12:40 am

While building util-primitive-0.1.0.0, it said:

Code: Select all

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

wildmyron
Posts: 1542
Joined: August 9th, 2013, 12:45 am
Location: Western Australia

Re: Yet another search program (with hexagons!)

Post by wildmyron » September 8th, 2018, 1:27 am

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

Code: Select all

        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:

Code: Select all

- git: https://github.com/strake/primitive.hs
commit: a43f1f488c78ffdb3acb607df703df16533fe7db
with

Code: Select all

- 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 5S project (Smallest Spaceships Supporting Specific Speeds) is now maintained by AforAmpere. The latest collection is hosted on GitHub and contains well over 1,000,000 spaceships.

Semi-active here - recovering from a severe case of LWTDS.

AlephAlpha
Posts: 66
Joined: October 6th, 2017, 1:50 am

Re: Yet another search program (with hexagons!)

Post by AlephAlpha » September 9th, 2018, 9:16 am

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

Code: Select all

        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:

Code: Select all

- git: https://github.com/strake/primitive.hs
commit: a43f1f488c78ffdb3acb607df703df16533fe7db
with

Code: Select all

- 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:

Code: Select all

/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:

Code: Select all

`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.

Post Reply