Comment by gotski

Slightly off topic, but this made me think of an example from the PuLP (Python Linear Programming library) that solves a sudoku using LP constraints.

https://coin-or.github.io/pulp/CaseStudies/a_sudoku_problem....

One nice thing about this approach is that by adding each solution in as a constraint and re-running, you can exhaustively enumerate all possible solutions for a given puzzle.