Three is a crowd: SAT, SMT and CLP on a chessboard

@INPROCEEDINGS{crowdedchessboard,
  ABSTRACT = {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.},
  AUTHOR = {Sebastian Krings and Michael Leuschel and Philipp K\"{o}rner and Stefan Hallerstede and Miran Hasanagi\'{c}},
  BOOKTITLE = {Proceedings PADL 2018},
  PUBLISHER = {Springer},
  SERIES = {LNCS},
  TITLE = {Three is a crowd: SAT, SMT and CLP on a chessboard},
  VOLUME = {10702},
  YEAR = {2018},
}