zzyzek

At the time I posted this submission, the proof was `sorry` and `axiom` free but had 154 `native_decide`s. The proof is enumeration heavy and so for efficiencies sake, the `native_decide`s were used to speed up proof compilation.

Since the submission here, I've had Claude remove the `native_decide`s and optimize the proof so that it now compiles with the three standard axioms only (`propext`, `Classical.choice` and `Quot.sound`).

I've also submitted it to the Palomar registry, which can be seen at:

  https://palomar-registry.org/entry?id=PALOMAR-2026-11-04-000002&version=1

GitHub repo can be found at:

  https://github.com/zzyzek/R2K2ZZN

along with a web demo:

  https://zzyzek.github.io/R2K2ZZN/demo/

In case it's not clear, two-colour Zig Zag Numberlink on rectangles is a special case of the more general NP-complete problem of arbitrary colour count Zig Zag Numberlink on rectangles. With arbitrary colour count, Zig Zag Numberlink is known NP-complete [0]. It was an open problem whether there were polynomial time algorithms when the colour count was finite.

This result doesn't answer the general question of whether there's a polynomial time algorithm for fixed number of colours for the Zig Zag Numberlink problem but provides a partial answer ("yes") of whether for some fixed colour count there exists a polynomial time algorithm. Namely, when the colour count is two, there exists a polynomial algorithm to determine whether the Zig Zag Numberlink problem is solvable and, if solvable, to provide a solution in polynomial time.

[0] https://arxiv.org/abs/1410.5845

Boris the brave coined the term "Constraint Based Tile Generators" (CBTG) [0], which is a specialization of the more general CSPs to this particular domain.

Personally, I find CSPs overly general and mired in esoteric, byzantine terminology. It's a large cognitive load to put on people to run through the glossary of terms just to talk about the problem set up. I don't think the quantum mechanic analogy is great but I can see it being much more intuitive than the obscure language of CSPs.

[0] https://www.boristhebrave.com/2021/10/31/constraint-based-ti...

For many, the name is intuitive as its encapsulating the idea that a cell can hold a variety of states until it gets "collapsed".

This is based off of Paul Merrell's Model Synthesis work [0]. Boris The Brave had a good writeup of the core of the algorithm [1].

Max Gumin focused on just the constraint solver and added a "minimum entropy heuristic", popularized the work and coined the term "wave function collapse", as the way the solver worked was evocative of (a naive view) of how quantum mechanics solves systems [2]. Gumin's repo also has many other resources of implementations and descriptions [3].

I've published a paper on an extension that adds in a type of backtracking to both the "WFC" portion of the solver and the modify in blocks portion of the solver, which can be found in [4], for those interested.

[0] https://paulmerrell.org/model-synthesis/

[1] https://www.boristhebrave.com/2021/10/26/model-synthesis-and...

[2] https://github.com/mxgmn/WaveFunctionCollapse

[3] https://github.com/mxgmn/WaveFunctionCollapse?tab=readme-ov-...

[4] https://zzyzek.github.io/PunchOutModelSynthesisPaper/

Publishing on arXiv is now very difficult. You need someone to endorse you who has an account on arXiv and has three recent publications in the area of research you're trying to submit.

I just went through this and had prominent researchers willing to endorse me but unable to do so because of the now stringent requirements on arXiv.

FYI, I am an independent researcher.

Very nice! Putting in an arXiv ID looks to produce many results that are much more relevant.

EDIT: You should provide this in an "information"/"about"/"how to use" dialogue or page to help people use the tool better.

This seems like a cool idea, thanks for creating it!

Some feedback:

I tried searching for "wave function collapse algorithm", "gumin wave function collapse", "wfc" and "model synthesis" without any relevant hits to the area of research I was interested in. I got a lot of quantum computing and other physics related papers.

The "WFC algorithm" overloaded the term (and has nothing to do with quantum mechanics) so it's kind of a bad case for this type of search. Model synthesis is way too generic, so again, might be a bad case for this.

The first page of results using "wave function collapse algorithm" from arXiv itself gives relevant results.

I'm working on an extension to the Modify in blocks Model Synthesis algorithm [0] and the Wave Function Collapse algorithm [1] called "Punch Out Model Synthesis":

https://github.com/zzyzek/PunchOutModelSynthesis

Here's a gallery of sample outputs from the algorithm:

https://github.com/zzyzek/PunchOutModelSynthesis/blob/main/r...

I have an online demo of the algorithm in action for different tilesets (it's a little rough, so be warned):

https://zzyzek.github.io/PunchOutModelSynthesis/

The idea is you take an example image, chop it into little segments and infer tile rules depending on the overlap. It's very much old fashioned "machine learning/artificial intelligence" (that is, without any neural networks involved). There's also a demo of tile rule inference idea here:

https://zzyzek.github.io/TileRuleHighlighter/

[0] https://github.com/mxgmn/WaveFunctionCollapse

[1] https://github.com/merrell42/model-synthesis