Answer Set Programming
Origin. Emerged from logic programming semantics: stable model semantics (Gelfond & Lifschitz, 1988) and well-founded semantics. Answer Set Programming (ASP) as a paradigm crystallized in the 1990s-2000s. Non-monotonic, supports negation as failure, defaults, and constraints. Implemented in efficient solvers: Clingo, DLV, WASP.
Models. Declarative problem solving through stable models. Write rules describing when conclusions hold; the solver finds models (answer sets) satisfying all rules. "Guess and check" problems: generate candidates, filter by constraints. Natural for combinatorial search, planning, diagnosis.
Formalism.
Logic program: Set of rules of the form:
head :- body.
- head: atom or disjunction of atoms
- body: literals (atoms or their negations)
Rule types:
- Fact: a. (always true)
- Rule: a :- b, c, not d. (a holds if b, c hold and d doesn't)
- Constraint: :- b, c. (b and c can't both hold)
- Choice: {a; b; c} :- body. (choose subset)
- Disjunction: a | b :- body. (at least one holds)
Negation as failure (NAF): not a means "a is not derivable" — closed-world assumption. Different from classical negation (-a).
Stable model / Answer set: A model M is stable for program P if:
- M satisfies all rules
- M is minimal: no proper subset satisfies the "reduct" P^M
Reduct P^M: for each rule, if NAF literals are false in M, keep the rule without NAF; otherwise delete the rule.
Example — Graph coloring:
% Generate: each node gets a color
1 { color(X,C) : col(C) } 1 :- node(X).
% Test: adjacent nodes differ
:- edge(X,Y), color(X,C), color(Y,C).
Aggregates:
:- #count{X : selected(X)} > K.
Optimization:
#minimize { W,X : cost(X,W), selected(X) }.
Symbols.
| Symbol | Unicode | Name | Meaning |
|---|---|---|---|
| | | U+007C | Vertical line / Disjunction | Disjunctive head, at least one disjunct holds |
| , | U+002C | Comma | Conjunction in a body |
| ; | U+003B | Semicolon | Separator inside a choice or disjunction |
| : | U+003A | Colon / Condition | Restricts a variable inside a set or aggregate |
| - | U+002D | Hyphen-minus / Strong negation | Explicit falsity, distinct from not |
| { | U+007B | Left brace | Opens a choice or aggregate set |
| } | U+007D | Right brace | Closes a choice or aggregate set |
| > | U+003E | Greater-than sign | Comparison in an aggregate constraint |
| % | U+0025 | Percent sign | Comment |
| :- | — | Rule arrow | Head holds if body holds; empty head gives a constraint |
| not | — | Negation as failure | Succeeds when the atom is not derivable |
| #count | — | Aggregate | Cardinality of a set |
| #sum | — | Aggregate | Sum of weights |
| #minimize | — | Optimization directive | Prefers answer sets of least cost |
| P^M | — | Reduct | Program with negative literals evaluated in M |
| M | — | Candidate model | Set of atoms tested for stability |
Metatheory. Gelfond and Lifschitz (1988) defined M to be a stable model of P when M is the least model of the reduct P^M, a definition that is a fixpoint condition rather than a derivation, since M appears on both sides. Every stable model is a minimal model and every atom in it is supported by a rule whose body holds, but neither converse holds, so stability is strictly stronger than minimality plus supportedness. Marek and Truszczyński (1989) showed that the stable models of a normal program are exactly the extensions of the corresponding default theory, which fixes ASP's place among the non-monotonic formalisms. For propositional programs, deciding whether an answer set exists is NP-complete for normal programs and Σ₂ᵖ-complete once disjunction is admitted (Eiter and Gottlob 1995); cautious consequence is correspondingly coNP-complete and Π₂ᵖ-complete. Lifschitz, Pearce and Valverde (2001) characterized strong equivalence — interchangeability in every context — as equivalence in the logic of here-and-there, giving the notion of program substitution a decidable monotonic criterion.
Applies to. Combinatorial optimization. Planning and scheduling. Configuration. Diagnosis and abduction. Bioinformatics (phylogeny, haplotyping). Knowledge representation. Product configuration. Solving NP-hard problems declaratively.
Limitations. Ordinary equivalence is not a congruence: two programs with the same answer sets can behave differently once embedded in a larger program, so nothing may be substituted for anything else without checking the stricter relation of strong equivalence, and the everyday notion supports no compositional reasoning. A program may have no answer set at all — a :- not a. is the minimal case — and cautious consequence then collapses into vacuous totality. Minimality is built into the semantics, so non-minimal models are not representable and disjunctive heads are minimal rather than inclusive: a | b never yields both disjuncts unless something else forces it. The language is propositional at bottom; variables are schematic and every program is grounded before solving, which costs exponentially in the number of variables per rule. Admitting function symbols removes the guarantee of a finite grounding and makes the existence of an answer set undecidable.
© 2026 Lingenic LLC