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