Solving Knights and Knaves with Z3
jamiecollinson.com