[mjn]

> 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.

[Dn_Ab]

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.