I love it how with the Z3Py solver you just write down a few constraints (rows, columns, 3x3 boxes and the given values) and you immediately get an answer.

[0] https://ericpony.github.io/z3py-tutorial/guide-examples.htm

[1] https://yurichev.com/writings/SAT_SMT_by_example.pdf