Definitely agree that they are criminally underused. I used to work for a large virtualization company, and used a SAT solver to walk an extremely complex dependency graph. We had originally been using a simple hill climbing algorithm and the SAT solver absolutely trounced it in terms of performance.
The biggest problem though, was when I would describe how we were using SAT to solve the graph, I generally would get extremely puzzled looks. Most other engineers have no exposure to them whatsoever.
Sometimes discrete graph theory problems can be relaxed into a continuous space where gradient descent can be used. If you want a concrete example of how this happens, take a look at the "Continuous Optimization" section in the "Thirty Years of Graph Matching in Pattern Recognition" paper (graph/subgraph isomorphism).
The biggest problem though, was when I would describe how we were using SAT to solve the graph, I generally would get extremely puzzled looks. Most other engineers have no exposure to them whatsoever.