Yes! SAT solvers are an amazing secret weapon for solving tricky problems. I've been collecting some fun examples of solver-aided programming here: https://github.com/kach/recreational-rosette (also, not in that repo, but still interesting: https://github.com/kach/tower-of-power).