Using Z3 to solve puzzles in a programmatic way using Python.
Example
Solving the following puzzle taken from https://www.mathsisfun.com/puzzles/lying-about-their-age.htmlÂ
Harder puzzle
Solving the following puzzle taken from https://www.brainzilla.com/logic/zebra/meeting-room/
This would output the picture on the left which is the same as the solution on the right:
