> What would be a concrete problem you could solve with SAT solvers, besides the obvious "satisfy this boolean expression" (which doesn't exactly come up every day)?

Say, you want to implement a package manager, with dependencies.