ABSTRACT
In this chapter we introduce the reader to a formalism closely related to propositional satisfiability, namely answer set programming (ASP for short). ASP is an extension of Horn logic, i.e., logic based on an extension of the logic admitting only Horn clauses. The extension uses a nonstandard negation not. This negation is sometimes called negation-by-failure. As in other cases (viz. our discussion of relationship of SAT and integer programming) we will touch only “the tip of the iceberg.” This area is well developed, and it has a number of monographs, for instance, [MT93, Ba03].
Let us recall that Horn clauses were clauses of the form p ∨ ¬q1 ∨ . . . ∨ ¬qk and of the form ¬q1 ∨ . . .∨¬qk. The clauses of the first kind were called program clauses, the second kind – constraints. We could treat the program clauses as implications: q1 ∧ . . .∧ qk ⇒ p. Traditionally, such clauses, when written by ASP researchers, are written like this:
