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

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.

Type
Publication
In Proceedings 20th International Symposium on Practical Aspects of Declarative Languages (PADL 2018), Springer LNCS
Sebastian Krings
Sebastian Krings
Software Engineer

My interests include software analysis, formal methods and offensive security.