I have only made light contact with SMTs in my explorations but SMT solvers have massive applicability. They're used in theorem proving - verification, dependent typing, contracts - scheduling, planning, and for understanding/modelling cell regulatory networks in biology.
Satisfiability stuff is interesting because it shows that just because something is NP-complete doesn't mean that it is unapproachable or 'hard' (just as linear programming shows just cause something is in P doesn't mean it is 'easy' - for large values of easy). To ground the concept you can roughly categorize it with logic programming, answer set programming, constraint satisfaction and integer programming. I've made use of answer set programming for certain planning problems as a kind of better prolog but SMT is a 'bit' more flexible.
> I've made use of answer set programming for certain planning problems as a kind of better prolog but SMT is a 'bit' more flexible.
I suppose it depends on what you mean by flexible. I would say that ASP is more flexible as a modeling language—you can specify all sorts of logic and constraints in it in a fairly expressive logical formalism, with both generative (Prolog-like) and constraint-oriented (CSP-like) language constructs. Particularly with the extensions the Potassco people have been making in their version: http://potassco.sourceforge.net/
However, current ASP solvers ground to variable-free (propositional) programs before solving, which means they blow up on large-ish integer domains, since you end up propositionalizing the whole integer range. I've had some examples where just grounding out the problem takes ages, but then it's nearly instant to solve once the grounding is done. SMT avoids that by providing a way to ground "modulo" a domain theory, rather than fully grounding, with a theory of integers being a common example.
Awesome response thanks. The increased ease of use for modeling is part of why I decided on it rather than an SMT solver. One should prefer ASP wherever the assumptions hold. I use(d) DLV-Complex but will check your link.
But right, by more flexible I meant the availability of quantifiers in SMT solvers.
Satisfiability stuff is interesting because it shows that just because something is NP-complete doesn't mean that it is unapproachable or 'hard' (just as linear programming shows just cause something is in P doesn't mean it is 'easy' - for large values of easy). To ground the concept you can roughly categorize it with logic programming, answer set programming, constraint satisfaction and integer programming. I've made use of answer set programming for certain planning problems as a kind of better prolog but SMT is a 'bit' more flexible.