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.