For those of us who'd rather have Haskell do the thinking for us:

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.