(25 April 2016)
These notes should document the relation between the concepts, as I see them. This is not a rant against Answer Set Programming. It is not against any-thing, much less against any person.
Comments welcome. Especially (see below) I’m looking for ASP examples that need ASP semantics. (And I guess I should include some examples throughout.)
is one way of assigning meaning to extended logic programs.
What is the motivation for this? A logic program is just a formula in predicate logic, consisting of facts and rules (implications). There is no question about defining when a structure (an interpretation) is a model of a formula. Yet, that “being a model” is not the usual semantics of classical logic programming.
Instead, the semantics of a PROLOG program is "the model that you (possibly) find when you execute the given strategy for resolution, e.g., rules in top-down order, premises inside rules from left to right. So, this semantics is operational.
An extended logic program may contain elements like negation, for which an operational semantics is not obvious. That was the reason for defining denotational semantics for extended logic programs. One way to do this, is “Answer set semantics”. This defines a concept “stability”, and then the ASP semantics of a program is the set of models (in the predicate-logic sense) that are also stable.
means satisfiability for propositional logic.
Why is this interesting? 1. Any problem in NP can be reduced in polynomial time to SAT. 2. There are powerful SAT solvers. So, SAT can be used as an “assembly language” for constraint programming - at least for some domains (finite) and constraints (first-order).
SAT corresponds to assembly language also because a “SAT program” is actually a conjunctive normal form (CNF), and as such is pretty much unreadable and unwritable for humans. So, we need translators (compilers), to make it usable in modelling.
The prominent example here is Bit-Vector (QFBV) logics. This is a language that is used in the hardware and software industry to specify and verify the behaviour of digital circuits, CPUs, and machine programs. Typically, a BV solver compiles to SAT, and then calls a SAT solver, and has optimizations that would in some cases reduce or avoid compilation of sub-formulas (because satisifiability status can be determined without it). Example: QFBV solver Boolector, SAT solver Lingeling.
We note that in the original definition of SAT, and in all applications that were mentioned here, the semantics is plain satisfiability (existence of a model in the classical sense), and it is denotational - not operational. Indeed SAT solvers will do some kind of resolution, but they can choose freely the order in which clauses are used and variables are assigned, and they are free to transform the formula as well - the outcome (status of satisfiability) must not depend on these choices (while performance could, and does).
For the reasons mentioned above, ASP solvers want to use SAT solvers. But ASP semantics is different from satisfiability, as “stability” needs to be expressed. This is possible, but costly. (One has to add “loop formulas”, and there may be exponentially many.) This is not a surprise since existence of a stable model is in the compexity class NP^NP (NP machine with an NP oracle), and not believed to be in NP (unless P = NP, of course).
well, that is just a catch phrase that I use to describe what I sometimes see:
People argue that
ASP languages allow to express constraints at a higher level than SAT - Indeed, they typically have some abstraction mechanisms that allow to express
ASP solvers use SAT solvers.
and conclude that
Why is this confusing? Because
There are other higher level languages for expressing finite-domain constraint problems that are, or can be, compiled to SAT. I mentioned QFBV, as part of the SMTLIB standard, and there is also (mini)Zinc, which currently has no SAT compiler that I know of, but it certainly can be done, at least for the “FD constraint subset” of Zinc.
I have attended several ASP demonstrations (talks), and my combined impression is that none of the examples shown there made actual use of ASP semantics. Examples given were colouring or assignment problems - well, that’s obviously in NP, and has an obvious SAT translation - we don’t need ASP here.
Of course it is reasonable to use the notational convenience that is missing in SAT (which is just CNF), and happens to be present in today’s ASP languages. But that is just syntax, not semantics.
When we write a straightforward formula (that is, logic program) for an FD satisfiability problem, it is not clear (to me) that ASP semantics is indeed what we want. If I only need some model - I still have to invest extra work to think about its stability, and perhaps make the ASP encoding “work around” that feature.
(on Answer Sets - other references are embeedded in the text)
Thomas Eiter: Answer Set Programming in a Nutshell - this contains a nice overview, has exact definitions, and avoids “ASP examples in NP”.
Torsten Schaub et al.: Teaching Answer Set Programming - this has all the details for the theory, but in the exampes (modeling) section(s) we get: N Queens, Travelling Salesperson, Reviewer Assignment, STRIPS planning. Looks NP to me. I do not find any mention of stability of models on the slides - but it could be elsewhere, e.g., in the book, which I don’t have.