Solving Suko with pysmt

In a waiting room this week I opened a newspaper to find the following puzzle, named “Suko” (a trademark of Puzzler).

Suko puzzle from The Times

Various approaches exist to solving them manually and it’s possible to play online. However they are an excellent candidate for an SMT solver so I decided to implement one using pysmt.