If you have a combinatorial problem that your first inclination is to use a brute-force backtracking-based search then maybe you could you a SAT solver instead.

If you have a combinatorial problem that your first inclination is to use a brute-force backtracking-based search then maybe you could you a SAT solver instead. It is a declarative way to solve the problem and good SAT solvers employ some very clever heuristics such as non-chronological backtracking and clause learning, which you might not get if you try to write the backtracking search yourself. One example that I like is that some Linux package managers have switched to using a SAT solver to satisfy package version constraints.