SAT is a key technology in electronic design automation (EDA), the industry making the tools allowing designing chips. From [1]:

"Within EDA, SAT solvers are used for such disparate tasks as test pattern generation, circuit delay computation, logic optimization, combinational equivalence checking, bounded model checking and functional test vector generation."

Improvement in SAT solving allows designing more and more complex chips.

In software it's used for formal checking, through SMT (Satisfiability Modulo Theory [2]). SMT is an extension of SAT. For an example application, Microsoft is using their z3 SMT solver [3], now open source, for the automated Windows driver verification process.

[1] https://semiengineering.com/knowledge_centers/eda-design/ver... [2] https://en.wikipedia.org/wiki/Satisfiability_modulo_theories [3] https://en.wikipedia.org/wiki/Z3_Theorem_Prover

FDIV cost Intel hundreds of millions, formal verification is big money.