[HN Gopher] Solving the Whole Year Puzzle with Z3
       ___________________________________________________________________
        
       Solving the Whole Year Puzzle with Z3
        
       Author : jaycrowell
       Score  : 14 points
       Date   : 2025-11-17 01:42 UTC (4 days ago)
        
 (HTM) web link (jcrowell.net)
 (TXT) w3m dump (jcrowell.net)
        
       | thechao wrote:
       | 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.
        
       | matthewfcarlson wrote:
       | This is incredible, time to make a 3d printable version of this
        
       | bena wrote:
       | 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.
        
       | vjerancrnjak wrote:
       | 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.
        
       ___________________________________________________________________
       (page generated 2025-11-21 23:01 UTC)