I’m not an expert in it either, but this problem is similar to both the N-queens problem and Sudoku, both of which can be solved via SAT, so tutorials for those

I’m not an expert in it either, but this problem is similar to both the N-queens problem and Sudoku, both of which can be solved via SAT, so tutorials for those should be a good start. Good luck!