In a waiting room this week I opened a newspaper to find the following puzzle, named “Suko” (a trademark of Puzzler).
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.
The puzzle The idea behind Suko is simple (manually solving is not!). In the puzzle above the following requirements must be met: