Three is a crowd: SAT, SMT and CLP on a chessboard
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.