Solving the Whole Year Puzzle with Z3

I think the major issue I have with Z3 is that if your input constraints are large and non-decomposable, then the resulting output is functionally undebuggable. There's a bit of handwaving from Z3folk about using assert_and_track() along with pseudoboolean proxies. But, there's a lot of pitfalls using these techniques. Combining bitvectors and pseudobooleans (y'know — the common case) under implication can either weaken or strengthen the constraints which literally changes the behavior of the given constraint problem. That means that any attempt to add tracing to the problem to debug your constraints can lead Z3 to change its behavior (because the underlying problem is different).

I really like Z3, and I like the convenience of Z3, but ... dang ... it'd be nice if you could trace internal statements.

Oh! Another pet-peeve is that there's no (sane) way to print large expressions. Once an expression gets large, Z3 begins dumping opaque internal variables (K!##). There is no way to get Z3 to unmunge these variables — that information is forever lost to you.

Interestingly, Knuth swapped dancing links for dancing arrays and implemented a bunch of SAT solvers (and counting solutions to polyomino tiling problems) using zero suppressed binary decision diagrams. So algorithms X has newer and more efficient successors.

This is incredible, time to make a 3d printable version of this

I have this, I've so far solved every day this year. And I think the last week of December, because I also received this for Christmas.

Some days are incredibly easy due to the day before. Some days, you can flip the orientation of one block and be done.

The most difficult days are when entire sections have to be rearranged. Like going from one week to the next or starting a new month.