Informaticus is an educational point and click adventure game. You explore the remainders of an ancient civilization that, at its time, possessed remarkable informational technology. Confronted with mysterious events surrounding the exploring team, you must solve riddles and puzzles based on computer science topics.
It has a puzzle in the temple:
It would be a great chance to test Wolfram Mathematica SAT solving capabilities:
List all digits:
And encode the equations:
One can now get rid of images and transfer the problem into a set of variables:
Boolean variables can be modelled with "one-hot" encoding, where x[v[i],j], means v[i]=j.
Here one can use the "no-good" SAT modelling approach: for each equation list the set of assignments that make it false and negate it:
Throwing all this into the solver with "All" option yields answer with certificate of uniqueness of the solution:
