I'm not sure I'd set up an opposition between SAT solvers like Z3 on one hand, and ASP on the other. I recommend to think of ASP (and other approaches like CSP

I'm not sure I'd set up an opposition between SAT solvers like Z3 on one hand, and ASP on the other. I recommend to think of ASP (and other approaches like CSP (constraint satisfaction problems)) as high-level languages for solving combinatorial problems. In this understanding, high-level (ASP, CSP) contrasts with low-level (SAT and SMT) for the same problem domain: just as with high- and low-level programming languages like Java are compiled down to low-level programming languages like x86 machine code, high-level formalism like ASP, CSP, ... can be compiled down to low-level SAT/SMT. SAT/SMT is the assembly language of combinatorial problems because you have to state explicitly all forbidden solutions using CNF (conjuncive normal form). For examle if you have variables x, y and z, then the CNF ( x \/ y \/ not z ) /\ ( not x /\ not y ) has as models all maps from {x, y, z} to {0, 1} except {x=0, y=0, z=1}, {x=1, y=1, z=1} and {x=1, y=1, z=0}. The problem with using CNFs to enumerate forbidden solutions is that the formulae can be long (just like assembler programs can be long). With high-level formalisms like ASP you often get a much more succinct specification. With a bit of squinting, you can even see first-order logic as a high-level formalism that compiles down to propositional logic (via skolemisation, resolution, unification, herbrand etc).