Yet another search program (with hexagons!)
Yet another search program (with hexagons!)
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.
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.
Re: Yet another search program (with hexagons!)
Excellent!
Although I haven't tried it yet.
I'm assuming z3 is a SAT Solver or something similar?
Although I haven't tried it yet.
I'm assuming z3 is a SAT Solver or something similar?
Re: Yet another search program (with hexagons!)
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!
Re: Yet another search program (with hexagons!)
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.Saka wrote:Excellent!
Although I haven't tried it yet.
I'm assuming z3 is a SAT Solver or something similar?
Re: Yet another search program (with hexagons!)
I get this error while compiling z3
I'm using cygwin
EDIT: Oh, cygwin doesnt use sudo. Problem solved
Code: Select all
sakaf@Arfie-Surface /z3/z3/build
$ sudo make install
-bash: $'\302\203sudo': command not found
EDIT: Oh, cygwin doesnt use sudo. Problem solved
Re: Yet another search program (with hexagons!)
I got this error when doing "stack build"
Code: Select all
Network.Socket.recvBuf: does not exist (No such file or directory)
Re: Yet another search program (with hexagons!)
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.Saka wrote:I got this error when doing "stack build"Code: Select all
Network.Socket.recvBuf: does not exist (No such file or directory)
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.
Semi-active here - recovering from a severe case of LWTDS.
Re: Yet another search program (with hexagons!)
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:wildmyron wrote: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.Saka wrote:I got this error when doing "stack build"Code: Select all
Network.Socket.recvBuf: does not exist (No such file or directory)
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.
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
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
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.
Semi-active here - recovering from a severe case of LWTDS.
Re: Yet another search program (with hexagons!)
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: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.
• 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).
Re: Yet another search program (with hexagons!)
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.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.
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.
Semi-active here - recovering from a severe case of LWTDS.
Re: Yet another search program (with hexagons!)
I just modified it to formulate the evolutionary rule as a z3 function — search might be a little speedier now.
Upcoming features:
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
-
- Posts: 66
- Joined: October 6th, 2017, 1:50 am
Re: Yet another search program (with hexagons!)
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
| ^^^^^^^^^^^^^^^^
Re: Yet another search program (with hexagons!)
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: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 | ^^^^^^^^^^^^^^^^
Code: Select all
- git: https://github.com/strake/primitive.hs
commit: a43f1f488c78ffdb3acb607df703df16533fe7db
Code: Select all
- git: https://github.com/haskell/primitive
commit: fb594e9897e4bf9ef7105502c04f6e438bd5fb1b
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.
Semi-active here - recovering from a severe case of LWTDS.
-
- Posts: 66
- Joined: October 6th, 2017, 1:50 am
Re: Yet another search program (with hexagons!)
Thank you very much.wildmyron wrote: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: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 | ^^^^^^^^^^^^^^^^
withCode: Select all
- git: https://github.com/strake/primitive.hs commit: a43f1f488c78ffdb3acb607df703df16533fe7db
@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.Code: Select all
- git: https://github.com/haskell/primitive commit: fb594e9897e4bf9ef7105502c04f6e438bd5fb1b
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’未定义的引用
Code: Select all
`gcc' failed in phase `Linker'. (Exit code: 1)