For those of us who'd rather have Haskell do the thinking for us: https://gist.github.com/LeventErkok/654a86a3ec7d3799b624 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. Enjoy.. -Levent. PS. Thanks to Amit Goel for suggesting the formalization strategy used in the encoding.