Comment by mzl

SAT (satisfiability), SMT (satisfiability modulo theories), CP (constraint programming) and so on are not magic solutions. They are more or less really smart backtracking solvers that use lots of heuristics, deductions based on the constraints, learning, restarts, portfolios, and so on. A real benefit is that one can re-use the algorithms that someone else has developed and debugged.

For toy-sized problems such as the LinkedIn Queens, 8-queens, and 9x9 Sudoku more or less any competently implemented solver will work fine. As soon as the size of the problem starts to grow, the difference between a plain backtracking algorithm and a SAT/SMT/CP system.