I usually spend max 20 minutes playing with something like that, then hours or even days finding a good SAT encoding for the puzzle so I can easily solve it with a program. (I can recommend this strategy to anyone who wants to improve their SAT or SMT skills.)
-
there’s a lesson in here about programmers always finding ways to create more problems for themselves :p
This is the first one I solved like that after *days* of trying it by hand. (The puzzle was passed to me through a series of people who all tried and failed.) This are five 1x1x1 pieces, five 2x2x3 pieces, six 1x2x4 pieces and a 5x5x5 box. 1/2pic.twitter.com/MxKjfMCozZ
-
-
[nerd vision turns on] just looking at this picture reminds me of an interesting work on register allocation/scheduling I was reading over recently - think of RA as puzzle solving, and formulate it as a geometric constraint problem!
-
so maybe I should rethink my position on creating problems as opposed to solving them :) (http://unison-code.github.io , if you’re interested!)
End of conversation
New conversation -
-
-
And here is the program that solves it: https://github.com/YosysHQ/yosys/blob/master/libs/ezsat/puzzle3d.cc … Not counting mirror images and rotations there are 4 unique solutions. (The program generates OpenSCAD models: https://github.com/YosysHQ/yosys/blob/master/libs/ezsat/puzzle3d.scad … You can slice and rotate in OpenSCAD to inspect the 3D model. 2/2pic.twitter.com/lpkGhOeOBZ
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
My kids played with a puzzle like that at their Montessori preschool. They were 4 years old, and were taught how to solve it!
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.