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 cells 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.
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.
It’s unclear from your description is this Z3 problem or this is the nature of such problems (and it’s a wish).
Are there other tools that do it better or proposal how Z3 would do it?
Are there any alternatives to Z3 that fixes these issues?
Interestingly, Knuth swapped dancing links for dancing cells 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.
just a headsup, your ssl certificate has expired, might wanna look into it
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.