N Queens Puzzle [5 points]

The \(n\)-queens puzzle is the problem of placing \(n\) queens on an \(n\times n\) chessboard such that no two queens attack each other. Model the puzzle as a SAT or SMT problem. Use a SAT or SMT solver to solve the \(n\)-queens puzzle and measure how the running time increases with the increasing values of \(n\).

Try at least three different SAT or SMT solvers and compare their performance for different values of \(n\). For example, what is the maximum value of \(n\) for which each SAT or SMT solver solves the problem within a minute?

Write a report with the results.