Constraint solving technology for declarative formal models has made considerable progress in recent years, and has many applications such as animation of high-level specifications, test case generation, or symbolic model checking. In this article we evaluate the idea of using very high-level declarative models themselves to express constraint satisfaction problems. In particular, we study an old mathematical puzzle from 100 years ago, called the crowded chessboard. We study various high-level and low-level encodings and solutions, covering SAT, SMT and CLP-based solutions of the puzzle. Additionally, we present a new technique combining SAT-solving with CLP which is able to solve the puzzle efficiently