He's stretching the definition of "interesting" I think. The main application of modern SAT solvers (and SMT solvers) is formal verification, which I do think is interesting, but you're very unlikely to be using it.
There are some other uses, e.g. for programming languages with advanced type systems, but I doubt most people interact with SAT solvers basically ever.
Have you used, interacted with, or benefited from AWS? ;)
You are right that most people do not have to interact with SAT solvers. Everyone has, almost surely, interacted with software with uses SAT solvers or have used SAT solvers for development tools.
If not software, your chips were definitely designed using tools which are nowadays based on SAT.
> If not software, your chips were definitely designed using tools which are nowadays based on SAT.
To some degree sure (assuming a generous definition of "designed"). I mentioned formal verification, and I expect synthesis uses it a bit. Still a pretty minor use IMO. You definitely could still design chips without SAT/SMT.
There are some other uses, e.g. for programming languages with advanced type systems, but I doubt most people interact with SAT solvers basically ever.