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/g

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-solves-sudoku-20150129/sudoku.smt2 https://github.com/grencez/grencez.dev/blob/trunk/2015/z3-so... [1] https://arxiv.org/pdf/2501.08569 https://arxiv.org/pdf/2501.08569