<div dir="ltr"><div>For those of us who'd rather have Haskell do the thinking for us:</div><div><br></div><a href="https://gist.github.com/LeventErkok/654a86a3ec7d3799b624">https://gist.github.com/LeventErkok/654a86a3ec7d3799b624</a><div><br></div><div>Honestly, this is more an exercise in how to formalize such puzzles as opposed to demonstrating the capabilities of SBV or SMT-solvers in general; but fun nonetheless. The backend SMT solver (I used Z3) solves the puzzle instantly.</div><div><br></div><div>Enjoy..</div><div><br></div><div>-Levent.</div><div><br></div><div>PS. Thanks to Amit Goel for suggesting the formalization strategy used in the encoding.<br><div><br></div><div><br></div></div></div>