One industry where SAT solvers get used frequently is in Electronic Design Automation. One comment already mentions its use in hardware/software verification. It turns out we can also use them to find efficient representations of Boolean functions (and therefore electronic circuits). This also generalizes to the synthesis of quantum logic circuits. They truly are amazingly versatile tools.