They play a big role in hardware design and verification as well. All in all, SAT solvers became very good, so the solution to many NP-hard problems is to encode them in SAT and solve them this way.