Look also to sudoku solvers in Z3: [0] also papers such as "Evaluating SAT and SMT Solvers on Large-Scale Sudoku Puzzles" [1].

[0] https://github.com/grencez/grencez.dev/blob/trunk/2015/z3-so... [1] https://arxiv.org/pdf/2501.08569