Answer Set Programming1 Abdallah Saffidine
COMP4418
1Slides designed by Christoph Schwering
Non-Monotonic Reasoning
2 / 30
Non-Monotonic Reasoning
∀x (Car(x) → ¬Entry(x))
2 / 30
Non-Monotonic Reasoning
∀x (Car(x) → ¬Entry(x))
∀x (Car(x) ∧ Auth(x) → Entry(x))
2 / 30
Non-Monotonic Reasoning
∀x (Car(x) → ¬Entry(x)) ∀x (Car(x) ∧ Auth(x) → Entry(x))
|= Car(C)∧Auth(C) → ¬Entry(C)
2 / 30
ASP at a Glance
ASP=AnswerSetProgramming
ASP ̸= Microsoft’s Active Server Pages
ASPbelongstologicprogramming
Like Prolog: Head ← Body or Head :- Body.
Like Prolog: negation as failure
Unlike Prolog: Head may be empty ⇒ constraints
Declarativeprogramming
Unlike Prolog: no procedural control Order has no impact on semantics
ASPprogramscomputemodels
Unlike Prolog: not query-oriented, no resolution
Unlike Prolog: not Turing-complete Tool for problems in NP and NPNP
3 / 30
Motivation for ASP and this Lecture
Veryusefulinpractice!
Declarative problem solving
Very fast to write Very fast to run Few experts
Interestingcasestudy
Small, simple core language
Great expressivity by reduction to core language
Knowingthetheoryisessential
4 / 30
Example: Graph Colouring
Definition: graph colouring problem
Input: graph with vertices V and edges E ⊆ V × V, set of colors C. Isthereamappingm:V →Cwithm(x)̸=m(y)forall(x,y)∈E?
35
6
12
4
Adopted from Potassco Slide Packages
5 / 30
Example: Graph Colouring
Definition: graph colouring problem
Input: graph with vertices V and edges E ⊆ V × V, set of colors C. Isthereamappingm:V →Cwithm(x)̸=m(y)forall(x,y)∈E?
35
6
12
4
Adopted from Potassco Slide Packages
5 / 30
Example: Graph Colouring
Definition: graph colouring problem
Input: graph with vertices V and edges E ⊆ V × V, set of colors C. Isthereamappingm:V →Cwithm(x)̸=m(y)forall(x,y)∈E?
GraphCoulouringisNP-complete
NP: guess solution, verify in polynomial time NP-complete: among hardest in NP
Manyapplications:
Mapping (neighbouring countries to different colors)
Compilers (register allocation)
Scheduling (e.g., conflicting jobs to different time slots) Allocationproblems,Sudoku,…
Adopted from Potassco Slide Packages
5 / 30
Example: Graph Colouring
Definition: graph colouring problem
Input: graph with vertices V and edges E ⊆ V × V, set of colors C. Isthereamappingm:V →Cwithm(x)̸=m(y)forall(x,y)∈E?
c(r). c(g). c(b).
v(1). … v(6). 35 e(1, 2). e(1, 3). e(1, 4). e(2, 4). e(2, 5). e(2, 6). 6 e(3, 1). e(3, 4). e(3, 5).
12
4
e(4, 1). e(4, 2).
e(5, 3). e(5, 4). e(5, 6). e(6, 2). e(6, 3). e(6, 5).
Adopted from Potassco Slide Packages
5 / 30
Example: Graph Colouring
Definition: graph colouring problem
Input: graph with vertices V and edges E ⊆ V × V, set of colors C. Isthereamappingm:V →Cwithm(x)̸=m(y)forall(x,y)∈E?
c(r). c(g). c(b).
v(1). … v(6). 35 e(1, 2). e(1, 3). e(1, 4). e(2, 4). e(2, 5). e(2, 6). 6 e(3, 1). e(3, 4). e(3, 5).
12
e(4, 1). e(4, 2).
e(5, 3). e(5, 4). e(5, 6). e(6, 2). e(6, 3). e(6, 5).
4
1 {m(X, C) : c(C)} 1 :- v(X). guess mapping m :- e(X, Y), m(X, C), m(Y, C). verify m(X) ̸= m(Y)
Adopted from Potassco Slide Packages 5 / 30
Example: Graph Colouring
Definition: graph colouring problem
Input: graph with vertices V and edges E ⊆ V × V, set of colors C. Isthereamappingm:V →Cwithm(x)̸=m(y)forall(x,y)∈E?
c(r). c(g). c(b).
v(1). … v(6). 35 e(1, 2). e(1, 3). e(1, 4). e(2, 4). e(2, 5). e(2, 6). 6 e(3, 1). e(3, 4). e(3, 5).
12
e(4, 1). e(4, 2).
e(5, 3). e(5, 4). e(5, 6). e(6, 2). e(6, 3). e(6, 5).
4
1 {m(X, C) : c(C)} 1 :- v(X). guess mapping m :- e(X, Y), m(X, C), m(Y, C). verify m(X) ̸= m(Y)
Adopted from Potassco Slide Packages 5 / 30
Applications of ASP
Automatedproductconfiguration
Linuxpackagemanager
Decision-supportsystemforspaceshuttle
Bioinformatics(diagnosis,inconsistencydetection) Generalgameplaying
Severalimplementationsareavailable
Forthislecture:Clingowww.potassco.org
6 / 30
Overview of the Lecture
SemanticsofASPprograms ExtensionsofASPprograms HandlingofvariablesinASP ASPasmodellinglanguage
7 / 30
Prolog vs ASP
Consider the following logic program:
a.
c ← a, b.
d ← a,notb.
a.
c :- a, b.
d :- a,notb.
8 / 30
Prolog vs ASP
Consider the following logic program:
a.
c ← a, b.
d ← a,notb.
PrologprovesbySLDresolution:
8 / 30
Prolog vs ASP
Consider the following logic program:
a.
c ← a, b.
d ← a,notb.
PrologprovesbySLDresolution:
Provesa(foraisafact)
8 / 30
Prolog vs ASP
Consider the following logic program:
a.
c ← a, b.
d ← a,notb.
PrologprovesbySLDresolution:
Provesa(foraisafact)
Cannot prove b (for b is in no head)
8 / 30
Prolog vs ASP
Consider the following logic program:
a.
c ← a, b.
d ← a,notb.
PrologprovesbySLDresolution:
Provesa(foraisafact)
Cannot prove b (for b is in no head) Cannot prove c (for cannot prove b)
8 / 30
Prolog vs ASP
Consider the following logic program:
a.
c ← a, b.
d ← a,notb.
PrologprovesbySLDresolution:
Provesa(foraisafact)
Cannot prove b (for b is in no head) Cannot prove c (for cannot prove b) Proves d (for prove a but not b)
Algorithm defines what Prolog does
8 / 30
Prolog vs ASP
Consider the following logic program:
a.
c ← a, b.
d ← a,notb.
PrologprovesbySLDresolution:
Provesa(foraisafact)
Cannot prove b (for b is in no head) Cannot prove c (for cannot prove b) Proves d (for prove a but not b)
Algorithm defines what Prolog does
Whatisthesemanticsofthislogicprogram?
8 / 30
Prolog vs ASP
Consider the following logic program:
a.
c ← a, b.
a
a ∧ b → c a ∧ ¬b → d
d ← a, not b.
PrologprovesbySLDresolution:
Provesa(foraisafact)
Cannot prove b (for b is in no head) Cannot prove c (for cannot prove b) Proves d (for prove a but not b)
Algorithm defines what Prolog does
Whatisthesemanticsofthislogicprogram?
Models: M1 = M2 = …
a
b
c
d
1
0
0
1
a
b
c
d
1
1
1
0
8 / 30
Prolog vs ASP
Consider the following logic program:
a.
c ← a, b.
a
a ∧ b → c a ∧ ¬b → d
d ← a, not b.
PrologprovesbySLDresolution:
Provesa(foraisafact)
Cannot prove b (for b is in no head) Cannot prove c (for cannot prove b) Proves d (for prove a but not b)
Algorithm defines what Prolog does
Whatisthesemanticsofthislogicprogram?
Models: M1 = M2 = … M1 corresponds to Prolog, what is special about M1?
a
b
c
d
1
0
0
1
a
b
c
d
1
1
1
0
8 / 30
Prolog vs ASP
Consider the following logic program:
a.
c ← a, b.
a
a ∧ b → c a ∧ ¬b → d
d ← a, not b.
PrologprovesbySLDresolution:
Provesa(foraisafact)
Cannot prove b (for b is in no head) Cannot prove c (for cannot prove b) Proves d (for prove a but not b)
Algorithm defines what Prolog does
Whatisthesemanticsofthislogicprogram?
Models: M1 = M2 = …
M1 corresponds to Prolog, what is special about M1? M1 is a stable model a.k.a. answer set:
M1 only satisfies justified propositions ASP gives semantics to logic programming
a
b
c
d
1
0
0
1
a
b
c
d
1
1
1
0
8 / 30
Intuition
The motivating guidelines behind stable model semantics are:
Astablemodelsatisfiesalltherulesofalogicprogram
Thereasonershallnotbelieveanythingtheyarenotforcedto believe — the rationality principle
9 / 30
Intuition
The motivating guidelines behind stable model semantics are:
Astablemodelsatisfiesalltherulesofalogicprogram
Thereasonershallnotbelieveanythingtheyarenotforcedto believe — the rationality principle
Next: formalisation of this intuition
For now: only ground programs, i.e., no variables
9 / 30
Syntax
Definition: normal logic program (NLP)
A normal logic program P is a set of (normal) rules of the form A ← B1, …,Bm,notC1, …,notCn.
where A, Bi, Cj are atomic propositions.
When m = n = 0, we omit the “←” and just write A.
10 / 30
Syntax
Definition: normal logic program (NLP)
A normal logic program P is a set of (normal) rules of the form A ← B1, …,Bm,notC1, …,notCn.
where A, Bi, Cj are atomic propositions.
When m = n = 0, we omit the “←” and just write A.
For such a rule r, we define:
Head(r) = {A}
Body(r) = {B1,…,Bm,notC1,…,notCn}
In code, r is written as A :- B1, . . . , Bm, not C1, . . . , not Cn.
10 / 30
Semantics: Interpretation
Definition: interpretation, satisfaction
An interpretation S is a set of atomic propositions.
SsatisfiesA←B1,…,Bm,notC1,…,notCn iff A∈S or someBi ∈/S or someCj ∈S.
In English:
S satisfies rule iff S satisfies the head or falsifies the body S falsifies body iff S falsifies some Bi or satisfies some Cj
11 / 30
Semantics: Interpretation
Definition: interpretation, satisfaction
An interpretation S is a set of atomic propositions.
SsatisfiesA←B1,…,Bm,notC1,…,notCn iff A∈S or someBi ∈/S or someCj ∈S.
In English:
S satisfies rule iff S satisfies the head or falsifies the body S falsifies body iff S falsifies some Bi or satisfies some Cj
Ex.: Let P = {a. c ← a, b. d ← a, not b.}
11 / 30
Semantics: Interpretation
Definition: interpretation, satisfaction
An interpretation S is a set of atomic propositions.
SsatisfiesA←B1,…,Bm,notC1,…,notCn iff A∈S or someBi ∈/S or someCj ∈S.
In English:
S satisfies rule iff S satisfies the head or falsifies the body S falsifies body iff S falsifies some Bi or satisfies some Cj
Ex.: Let P = {a. c ← a, b. d ← a, not b.}
S = {a, b, c} satisfies a, but it does not satisfy (not b).
11 / 30
Semantics: Interpretation
Definition: interpretation, satisfaction
An interpretation S is a set of atomic propositions.
SsatisfiesA←B1,…,Bm,notC1,…,notCn iff A∈S or someBi ∈/S or someCj ∈S.
In English:
S satisfies rule iff S satisfies the head or falsifies the body S falsifies body iff S falsifies some Bi or satisfies some Cj
Ex.: Let P = {a. c ← a, b. d ← a, not b.}
S = {a, b, c} satisfies a, but it does not satisfy (not b).
It satisfies c ← a, b because it satisfies the head because c ∈ S
11 / 30
Semantics: Interpretation
Definition: interpretation, satisfaction
An interpretation S is a set of atomic propositions.
SsatisfiesA←B1,…,Bm,notC1,…,notCn iff A∈S or someBi ∈/S or someCj ∈S.
In English:
S satisfies rule iff S satisfies the head or falsifies the body S falsifies body iff S falsifies some Bi or satisfies some Cj
Ex.: Let P = {a. c ← a, b. d ← a, not b.}
S = {a, b, c} satisfies a, but it does not satisfy (not b).
It satisfies c ← a, b because it satisfies the head because c ∈ S
It satisfies d ← a, not b because it falsifies the body because b ∈ S
11 / 30
Semantics without Negation
Definition: stable model for programs without negation
For P without negated literals: S is a stable model of P iff
S is a minimal set (w.r.t. ⊆) that satisfies all r ∈ P.
12 / 30
Semantics without Negation
Definition: stable model for programs without negation
For P without negated literals: S is a stable model of P iff
S is a minimal set (w.r.t. ⊆) that satisfies all r ∈ P.
Ex.: P = {a. c ← a, b.}
12 / 30
Semantics without Negation
Definition: stable model for programs without negation
For P without negated literals: S is a stable model of P iff
S is a minimal set (w.r.t. ⊆) that satisfies all r ∈ P.
Ex.: P = {a. c ← a, b.}
S1 ={a}isastablemodelofP
12 / 30
Semantics without Negation
Definition: stable model for programs without negation
For P without negated literals: S is a stable model of P iff
S is a minimal set (w.r.t. ⊆) that satisfies all r ∈ P.
Ex.: P = {a. c ← a, b.}
S1 ={a}isastablemodelofP
S2 = {a,b} is not a stable model of P
12 / 30
Semantics without Negation
Definition: stable model for programs without negation
For P without negated literals: S is a stable model of P iff
S is a minimal set (w.r.t. ⊆) that satisfies all r ∈ P.
Ex.: P = {a. c ← a, b.}
S1 ={a}isastablemodelofP
S2 = {a,b} is not a stable model of P S3 = {a,b,c} is not a stable model of P
12 / 30
Semantics without Negation
Definition: stable model for programs without negation
For P without negated literals: S is a stable model of P iff
S is a minimal set (w.r.t. ⊆) that satisfies all r ∈ P.
Ex.: P = {a. c ← a, b.}
S1 ={a}isastablemodelofP
S2 = {a,b} is not a stable model of P S3 = {a,b,c} is not a stable model of P
Theorem: unique-model property
If P is negation-free (i.e., contains no (not C)), then there is exactly one stable model, which can be computed in linear time.
12 / 30
Semantics without Negation – Examples
Compute stable model of a negation-free P by unit propagation: S0 = {}
Si+1 = Si ∪ r∈P:S satisfies Body(r) Head(r) until Si+1 = Si
13 / 30
Semantics without Negation – Examples
Compute stable model of a negation-free P by unit propagation: S0 = {}
Si+1 = Si ∪ r∈P:S satisfies Body(r) Head(r) until Si+1 = Si
Ex.: P1 = {a. b ← a.}
S0 = {} S1 = {a} S2 = {a,b} Fixpoint
13 / 30
Semantics without Negation – Examples
Compute stable model of a negation-free P by unit propagation: S0 = {}
Si+1 = Si ∪ r∈P:S satisfies Body(r) Head(r) until Si+1 = Si
Ex.: P1 = {a. b ← a.}
S0 = {} S1 = {a} S2 = {a,b} Fixpoint
Ex.: P2 = {a ← b. b ← a.} S0 = {} Fixpoint
13 / 30
Semantics without Negation – Examples
Compute stable model of a negation-free P by unit propagation: S0 = {}
Si+1 = Si ∪ r∈P:S satisfies Body(r) Head(r) until Si+1 = Si
Ex.: P1 = {a. b ← a.}
S0 = {} S1 = {a} S2 = {a,b}
Ex.: P2 = {a ← b. b ← a.} S0 = {} Fixpoint
Ex.: P3 = {a ← b. b ← a. a.}
S0 = {} S1 = {a} S2 = {a,b}
Fixpoint
Fixpoint
13 / 30
Semantics with Negation
Definition: reduct
The reduct PS of P relative to S is the least set such that
if A ← B1, …,Bm,notC1, …,notCn ∈ P and C1,…,Cn ∈/ S then A ← B1, …,Bm ∈ PS.
In English: for each rule r from P,
if(notC)∈Body(r)forsomeC∈S:droptherule else:removeallnegatedliteralsandaddtoPS
14 / 30
Semantics with Negation
Definition: reduct
The reduct PS of P relative to S is the least set such that
if A ← B1, …,Bm,notC1, …,notCn ∈ P and C1,…,Cn ∈/ S then A ← B1, …,Bm ∈ PS.
In English: for each rule r from P,
if(notC)∈Body(r)forsomeC∈S:droptherule else:removeallnegatedliteralsandaddtoPS
Ex.: P = {a. c ← a, b. d ← a, not b.}
14 / 30
Semantics with Negation
Definition: reduct
The reduct PS of P relative to S is the least set such that
if A ← B1, …,Bm,notC1, …,notCn ∈ P and C1,…,Cn ∈/ S then A ← B1, …,Bm ∈ PS.
In English: for each rule r from P,
if(notC)∈Body(r)forsomeC∈S:droptherule else:removeallnegatedliteralsandaddtoPS
Ex.: P = {a. c ← a, b. d ← a, not b.}
S1 ={a} ⇒ PS1 ={a. c←a,b. d←a,notb.}
14 / 30
Semantics with Negation
Definition: reduct
The reduct PS of P relative to S is the least set such that
if A ← B1, …,Bm,notC1, …,notCn ∈ P and C1,…,Cn ∈/ S then A ← B1, …,Bm ∈ PS.
In English: for each rule r from P,
if(notC)∈Body(r)forsomeC∈S:droptherule else:removeallnegatedliteralsandaddtoPS
Ex.: P = {a. c ← a, b. d ← a, not b.}
S1 ={a} ⇒ PS1 ={a. c←a,b. d←a,notb.} S2 ={a,b} ⇒ PS2 ={a. c←a,b. d←a,notb.}
14 / 30
Semantics with Negation
Definition: reduct
The reduct PS of P relative to S is the least set such that
if A ← B1, …,Bm,notC1, …,notCn ∈ P and C1,…,Cn ∈/ S then A ← B1, …,Bm ∈ PS.
In English: for each rule r from P,
if(notC)∈Body(r)forsomeC∈S:droptherule else:removeallnegatedliteralsandaddtoPS
Ex.: P = {a. c ← a, b. d ← a, not b.}
S1 ={a} ⇒ PS1 ={a. c←a,b. d←a,notb.} S2 ={a,b} ⇒ PS2 ={a. c←a,b. d←a,notb.} S3 ={a,d} ⇒ PS3 ={a. c←a,b. d←a,notb.}
14 / 30
Semantics with Negation
Definition: reduct
The reduct PS of P relative to S is the least set such that
if A ← B1, …,Bm,notC1, …,notCn ∈ P and C1,…,Cn ∈/ S then A ← B1, …,Bm ∈ PS.
In English: for each rule r from P,
if(notC)∈Body(r)forsomeC∈S:droptherule else:removeallnegatedliteralsandaddtoPS
Ex.: P = {a. c ← a, b. d ← a, not b.}
S1 ={a} ⇒ PS1 ={a. c←a,b. d←a.} S2 ={a,b} ⇒ PS2 ={a. c←a,b.}
S3 ={a,d} ⇒ PS3 ={a. c←a,b. d←a.}
14 / 30
Semantics with Negation
Definition: reduct
The reduct PS of P relative to S is the least set such that
if A ← B1, …,Bm,notC1, …,notCn ∈ P and C1,…,Cn ∈/ S then A ← B1, …,Bm ∈ PS.
In English: for each rule r from P,
if(notC)∈Body(r)forsomeC∈S:droptherule else:removeallnegatedliteralsandaddtoPS
Ex.: P = {a. c ← a, b. d ← a, not b.}
S1 ={a} ⇒ PS1 ={a. c←a,b. d←a.} S2 ={a,b} ⇒ PS2 ={a. c←a,b.}
S3 ={a,d} ⇒ PS3 ={a. c←a,b. d←a.}
Definition: stable model for programs with negation
For P with negated literals:
SisastablemodelofP iff SisastablemodelofPS.
14 / 30
Semantics with Negation
Definition: reduct
The reduct PS of P relative to S is the least set such that
if A ← B1, …,Bm,notC1, …,notCn ∈ P and C1,…,Cn ∈/ S then A ← B1, …,Bm ∈ PS.
In English: for each rule r from P,
if(notC)∈Body(r)forsomeC∈S:droptherule else:removeallnegatedliteralsandaddtoPS
Ex.: P = {a. c ← a, b. d ← a, not b.}
S1 ={a} ⇒ PS1 ={a. c←a,b. d←a.} # S2 ={a,b} ⇒ PS2 ={a. c←a,b.}
S3 ={a,d} ⇒ PS3 ={a. c←a,b. d←a.}
Definition: stable model for programs with negation
For P with negated literals:
SisastablemodelofP iff SisastablemodelofPS.
14 / 30
Semantics with Negation
Definition: reduct
The reduct PS of P relative to S is the least set such that
if A ← B1, …,Bm,notC1, …,notCn ∈ P and C1,…,Cn ∈/ S then A ← B1, …,Bm ∈ PS.
In English: for each rule r from P,
if(notC)∈Body(r)forsomeC∈S:droptherule else:removeallnegatedliteralsandaddtoPS
Ex.: P = {a. c ← a, b. d ← a, not b.}
S1 ={a} ⇒ PS1 ={a. c←a,b. d←a.} # S2 ={a,b} ⇒ PS2 ={a. c←a,b.} # S3 ={a,d} ⇒ PS3 ={a. c←a,b. d←a.}
Definition: stable model for programs with negation
For P with negated literals:
SisastablemodelofP iff SisastablemodelofPS.
14 / 30
Semantics with Negation
Definition: reduct
The reduct PS of P relative to S is the least set such that
if A ← B1, …,Bm,notC1, …,notCn ∈ P and C1,…,Cn ∈/ S then A ← B1, …,Bm ∈ PS.
In English: for each rule r from P,
if(notC)∈Body(r)forsomeC∈S:droptherule else:removeallnegatedliteralsandaddtoPS
Ex.: P = {a. c ← a, b. d ← a, not b.}
S1 ={a} ⇒ PS1 ={a. c←a,b. d←a.} # S2 ={a,b} ⇒ PS2 ={a. c←a,b.} # S3 ={a,d} ⇒ PS3 ={a. c←a,b. d←a.}
Definition: stable model for programs with negation
For P with negated literals:
SisastablemodelofP iff SisastablemodelofPS.
14 / 30
Semantics with Negation – Examples
Ex.: P = {a ← not b. b ← not a.}
15 / 30
Semantics with Negation – Examples
Ex.: P = {a ← not b. b ← not a.} S1 = {} ⇒ PS1 =
15 / 30
Semantics with Negation – Examples
Ex.: P = {a ← not b. b ← not a.}
S1 ={} ⇒ PS1 ={a←notb. b←nota.}
15 / 30
Semantics with Negation – Examples
Ex.: P = {a ← not b. b ← not a.}
S1 ={} ⇒ PS1 ={a←notb. b←nota.} S2 = {a} ⇒ PS2 =
15 / 30
Semantics with Negation – Examples
Ex.: P = {a ← not b. b ← not a.}
S1 ={} ⇒ PS1 ={a←notb. b←nota.} S2 ={a} ⇒ PS2 ={a←notb. b←nota.}
15 / 30
Semantics with Negation – Examples
Ex.: P = {a ← not b. b ← not a.}
S1 ={} S2 ={a} S3 = {b}
⇒ PS1 ={a←notb. b←nota.}
⇒ PS2 ={a←notb. b←nota.} ⇒ PS3 =
15 / 30
Semantics with Negation – Examples
Ex.: P = {a ← not b. b ← not a.}
S1 ={} S2 ={a} S3 ={b}
⇒ PS1 ={a←notb. b←nota.} ⇒ PS2 ={a←notb. b←nota.} ⇒ PS3 ={a←notb. b←nota.}
15 / 30
Semantics with Negation – Examples
Ex.: P = {a ← not b.
b ← not a.} ={a←notb. b←nota.}
={a←notb. b←nota.} ={a←notb. b←nota.} =
S1 ={}
S2 ={a}
S3 ={b}
S4 ={a,b} ⇒ PS4
⇒ PS1 ⇒ PS2 ⇒ PS3
15 / 30
Semantics with Negation – Examples
Ex.: P = {a ← not b.
b ← not a.} ={a←notb. b←nota.}
={a←notb. b←nota.} ={a←notb. b←nota.} ={a←notb. b←nota.}
S1 ={}
S2 ={a}
S3 ={b}
S4 ={a,b} ⇒ PS4
⇒ PS1 ⇒ PS2 ⇒ PS3
15 / 30
Semantics with Negation – Examples
Ex.: P = {a ← not b.
b ← not a.} = {a. b}
={a.} ={b.} ={}
S1 = {}
S2={a}
S3={b}
S4 ={a,b} ⇒ PS4
⇒ PS1 ⇒ PS2 ⇒ PS3
15 / 30
Semantics with Negation – Examples
Ex.: P = {a ← not b.
b ← not a.}
= {a. b} #
={a.} ={b.} ={}
S1 = {}
S2={a}
S3={b}
S4 ={a,b} ⇒ PS4
⇒ PS1 ⇒ PS2 ⇒ PS3
15 / 30
Semantics with Negation – Examples
Ex.: P = {a ← not b.
b ← not a.}
= {a. b} #
={a.} ={b.}
={}
S1 = {}
S2={a}
S3={b}
S4 ={a,b} ⇒ PS4
⇒ PS1 ⇒ PS2 ⇒ PS3
15 / 30
Semantics with Negation – Examples
Ex.: P = {a ← not b.
b ← not a.}
= {a. b} #
={a.} ={b.} ={}
S1 = {}
S2={a}
S3={b}
S4 ={a,b} ⇒ PS4
⇒ PS1 ⇒ PS2 ⇒ PS3
15 / 30
Semantics with Negation – Examples
Ex.: P = {a ← not b.
b ← not a.}
= {a. b} #
={a.} ={b.} ={} #
S1 = {}
S2={a}
S3={b}
S4 ={a,b} ⇒ PS4 Two stable models!
⇒ PS1 ⇒ PS2 ⇒ PS3
15 / 30
Semantics with Negation – Examples
Ex.: P = {a ← not b.
b ← not a.}
= {a. b} #
={a.} ={b.} ={} #
S1 = {}
S2={a}
S3={b}
S4 ={a,b} ⇒ PS4 Two stable models!
Ex.: P = {a ← not a.}
⇒ PS1 ⇒ PS2 ⇒ PS3
15 / 30
Semantics with Negation – Examples
Ex.: P = {a ← not b.
b ← not a.}
= {a. b} #
={a.} ={b.} ={} #
S1 = {}
S2={a}
S3={b}
S4 ={a,b} ⇒ PS4 Two stable models!
Ex.: P = {a ← not a.} S1={} ⇒PS1=
⇒ PS1 ⇒ PS2 ⇒ PS3
15 / 30
Semantics with Negation – Examples
Ex.: P = {a ← not b.
b ← not a.}
= {a. b} #
={a.} ={b.} ={} #
S1 = {}
S2={a}
S3={b}
S4 ={a,b} ⇒ PS4 Two stable models!
⇒ PS1 ⇒ PS2 ⇒ PS3
Ex.: P = {a ← not a.}
S1 ={} ⇒ PS1 ={a←nota.}
15 / 30
Semantics with Negation – Examples
Ex.: P = {a ← not b.
b ← not a.}
= {a. b} #
={a.} ={b.} ={} #
S1 = {}
S2={a}
S3={b}
S4 ={a,b} ⇒ PS4 Two stable models!
⇒ PS1 ⇒ PS2 ⇒ PS3
Ex.: P = {a ← not a.}
S1 ={} ⇒ PS1 ={a←nota.} S2 = {a} ⇒ PS2 =
15 / 30
Semantics with Negation – Examples
Ex.: P = {a ← not b.
b ← not a.}
= {a. b} #
={a.} ={b.} ={} #
S1 = {}
S2={a}
S3={b}
S4 ={a,b} ⇒ PS4 Two stable models!
⇒ PS1 ⇒ PS2 ⇒ PS3
Ex.: P = {a ← not a.}
S1 ={} ⇒ PS1 ={a←nota.} S2 ={a} ⇒ PS2 ={a←nota.}
15 / 30
Semantics with Negation – Examples
Ex.: P = {a ← not b.
b ← not a.}
= {a. b} #
={a.} ={b.} ={} #
S1 = {}
S2={a}
S3={b}
S4 ={a,b} ⇒ PS4 Two stable models!
Ex.: P = {a ← not a.}
S1={} ⇒ PS1 ={a.} S2 ={a} ⇒ PS2 ={}
⇒ PS1 ⇒ PS2 ⇒ PS3
15 / 30
Semantics with Negation – Examples
Ex.: P = {a ← not b.
b ← not a.}
= {a. b} #
={a.} ={b.} ={} #
S1 = {}
S2={a}
S3={b}
S4 ={a,b} ⇒ PS4 Two stable models!
⇒ PS1 ⇒ PS2 ⇒ PS3
Ex.: P = {a ← not a.}
S1={} ⇒PS1={a.} # S2 ={a} ⇒ PS2 ={}
15 / 30
Semantics with Negation – Examples
Ex.: P = {a ← not b.
b ← not a.}
= {a. b} #
={a.} ={b.} ={} #
S1 = {}
S2={a}
S3={b}
S4 ={a,b} ⇒ PS4 Two stable models!
⇒ PS1 ⇒ PS2 ⇒ PS3
Ex.: P = {a ← not a.}
S1={} ⇒PS1={a.} # S2={a} ⇒ PS2 ={} # No stable model!
15 / 30
Semantics: Overview
Definition: reduct
The reduct PS of P relative to S is the least set such that
if A ← B1, …,Bm,notC1, …,notCn ∈ P and C1,…,Cn ∈/ S then A ← B1, …,Bm ∈ PS.
Definition: stable model
If P contains no (not C):
S is a stable model of P iff
S is a minimal set (w.r.t. ⊆) that satisfies all r ∈ P.
If P contains (not C):
SisastablemodelofP iffSisastablemodelofPS.
Theorem: necessary satisfaction condition
If S is a stable model and A ∈ S,
then S satisfies some r ∈ P with A ∈ Head(r).
16 / 30
Semantics – Examples
Ex.: P = {a ← a. b ← not a.} S PS
Stable model?
Ex.: P = {a ← not b. b ← not c.} S PS
Stable model?
Example on paper
17 / 30
Overview of the Lecture
SemanticsofASPprograms
ExtensionsofASPprograms HandlingofvariablesinASP ASPasmodellinglanguage
18 / 30
Integrity Constraints
Definition: integrity constraint
An integrity constraint is a rule r of the form
← B1, …,Bm,notC1, …,notCn
Ssatisfiesr iff someBi ∈/S or someCj ∈S. PScontains←B1,…,Bm iffPcontainsrandC1,…,Cn∈/S.
19 / 30
Integrity Constraints
Definition: integrity constraint
An integrity constraint is a rule r of the form
← B1, …,Bm,notC1, …,notCn
Ssatisfiesr iff someBi ∈/S or someCj ∈S. PScontains←B1,…,Bm iffPcontainsrandC1,…,Cn∈/S.
Theorem: reduction to normal rules
Let P′ be like P except that every integrity constraint ← B1, …,Bm,notC1, …,notCn
is replaced with
dummy ← B1, …,Bm,notC1, …,notCn,notdummy for some new atom dummy.
Then P and P′ have the same stable models.
19 / 30
Choice Rules
Definition: choice rule
A choice rule is a rule the form
{A1,…,Ak} ← B1, …,Bm,notC1, …,notCn
which allows any subset of {A1, . . . , Ak} in a stable model.
20 / 30
Choice Rules
Definition: choice rule
A choice rule is a rule the form
{A1,…,Ak} ← B1, …,Bm,notC1, …,notCn
which allows any subset of {A1, . . . , Ak} in a stable model.
Theorem: reduction to normal rules
A choice rule can be encoded by 2k + 1 normal rules using 2k + 1 new atoms.
20 / 30
Choice Rules
Definition: choice rule
A choice rule is a rule the form
{A1,…,Ak} ← B1, …,Bm,notC1, …,notCn
which allows any subset of {A1, . . . , Ak} in a stable model.
Theorem: reduction to normal rules
A choice rule can be encoded by 2k + 1 normal rules using 2k + 1 new atoms.
Further extensions:
Conditional literals: {A : B}
Ex.: {m(v, C) : c(C)} expands to {m(v, r), m(v, g), m(v, b)}
Cardinality constraints: min {A1, . . . , Ak} max Ex.: 1 {m(v, r), m(v, g), m(v, b)} 1
20 / 30
Negation in the Rule Head
Definition: rules with negated head
A rule with negated head is of the form
notA ← B1, …,Bm,notC1, …,notCn
21 / 30
Negation in the Rule Head
Definition: rules with negated head
A rule with negated head is of the form
notA ← B1, …,Bm,notC1, …,notCn
Theorem: reduction to normal rules
Let P′ be like P except that every rule with negated head notA ← B1, …,Bm,notC1, …,notCn
is replaced with
← B1, …,Bm,notC1, …,notCn,notdummy
and
dummy ← not A for some new atom dummy.
Then P and P′ have the same stable models (modulo dummy propositions).
21 / 30
Complexity
Theorem: complexity of NLPs without negations
Is S a stable model of a negation-free P? – Linear time
Does a negation-free P have a stable model? – Constant (yes, one)
Theorem: complexity of NLPs with negations
Is S a stable model of P? – Linear time
Does P have a stable model? – NP-complete
Note: integrity constraints, choice rules, negation in heads preserve complexity (program grows only polynomially)
22 / 30
Overview of the Lecture
SemanticsofASPprograms
ExtensionsofASPprograms HandlingofvariablesinASP ASPasmodellinglanguage
23 / 30
Programs with Variables
Atomicpropositionsmaynowcontainvariables,e.g., p(X, Z) ← e(X, Y), p(Y, Z).
24 / 30
Programs with Variables
Atomicpropositionsmaynowcontainvariables,e.g., p(X, Z) ← e(X, Y), p(Y, Z).
Herbranduniverse
U contains all constants from P
U contains all f(t1,…,tk) from P if f is a k-ary function in P
and U contains t1,…,tk
24 / 30
Programs with Variables
Atomicpropositionsmaynowcontainvariables,e.g., p(X, Z) ← e(X, Y), p(Y, Z).
Herbranduniverse
U contains all constants from P
U contains all f(t1,…,tk) from P if f is a k-ary function in P
and U contains t1,…,tk
ASPgroundsvariableswithHerbranduniverse
Unlike Prolog: instantiation instead of unification
Caution: the ground program may grow exponentially
Caution: function symbols make grounding Turing-complete If P is finite and mentions only constants, grounding is finite
24 / 30
Programs with Variables
f(X) ← b(X),nota(X). a(X) ← p(X).
b(sam).
b(tweety).
p(tweety).
f(sam)←b(sam),nota(sam).
f (tweety) ← b(tweety), not a(tweety). a(sam) ← p(sam).
a(tweety) ← p(tweety).
b(sam).
b(tweety).
p(tweety).
25 / 30
Overview of the Lecture
SemanticsofASPprograms ExtensionsofASPprograms HandlingofvariablesinASP ASPasmodellinglanguage
26 / 30
ASP Modelling
Typical ASP structure:
Probleminstance:asetoffacts Problemclass:asetofrules
Generator rules: often choice rules Test rules: often integrity constraints
Ideal modeling is uniform: problem class encoding fits all instances
Semantically equivalent encodings may differ immensely in performance!
27 / 30
c(r). c(g). c(b).
v(1). … v(6).
e(1, 2). e(1, 3). e(1, 4). e(2, 4). e(2, 5). e(2, 6). e(3, 1). e(3, 4). e(3, 5). e(4, 1). e(4, 2).
e(5, 3). e(5, 4). e(5, 6). e(6, 2). e(6, 3). e(6, 5).
1 {m(X, C) : c(C)} 1 :- v(X). :- e(X, Y), m(X, C), m(Y, C).
Example: Non-monotonic Reasoning
Tweety the penguin:
(Normal)Birdsfly.
Penguinsareabnormal.
Tweetyisabird.SoTweetyflies.
Tweetyisapenguin.SoTweetydoesn’tfly.
28 / 30
Example: Non-monotonic Reasoning
Tweety the penguin:
(Normal)Birdsfly.
Penguinsareabnormal.
Tweetyisabird.SoTweetyflies.
Tweetyisapenguin.SoTweetydoesn’tfly.
U = {f(X) ← b(X),nota(X). a(X) ← p(X). b(t).} P = {f (t) ← b(t), not a(t). a(t) ← p(t). b(t).}
28 / 30
Example: Non-monotonic Reasoning
Tweety the penguin:
(Normal)Birdsfly.
Penguinsareabnormal.
Tweetyisabird.SoTweetyflies.
Tweetyisapenguin.SoTweetydoesn’tfly.
U = {f(X) ← b(X),nota(X). a(X) ← p(X). b(t).} P = {f (t) ← b(t), not a(t). a(t) ← p(t). b(t).}
S1 = {b(t), f (t)} ⇒ PS1 = {f (t) ← b(t), not a(t). S2 = {a(t), b(t), p(t)} ⇒ PS2 = {f (t) ← b(t), not a(t). Tweety flies!
a(t) ← p(t). a(t) ← p(t).
b(t).} b(t).} #
28 / 30
Example: Non-monotonic Reasoning
Tweety the penguin:
(Normal)Birdsfly.
Penguinsareabnormal.
Tweetyisabird.SoTweetyflies.
Tweetyisapenguin.SoTweetydoesn’tfly.
U = {f(X) ← b(X),nota(X). a(X) ← p(X). b(t).} P = {f (t) ← b(t), not a(t). a(t) ← p(t). b(t).}
S1 = {b(t), f (t)}
S2 = {a(t), b(t), p(t)} Tweety flies!
S1 = {b(t), f (t)}
⇒ PS1 = {f (t) ← b(t), not a(t). ⇒ PS2 = {f (t) ← b(t), not a(t).
a(t) ← p(t). a(t) ← p(t).
b(t).} b(t).} #
⇒ (P ∪ {p(t).})S1 = PS1 ∪ {p(t).} # 2
S2 = {a(t), b(t), p(t)} ⇒ (P ∪ {p(t).})S2 = PS1 ∪ {p(t).} 2
Tweety doesn’t fly.
28 / 30
Example: Hamilton Cycle
Definition: Hamilton cycle problem
Input: graph with vertex set V and edges E ⊆ V × V. Is there a cycle that visits every vertex exactly once?
35 6 12
4
{p(X, Y)} ← e(X, Y). r(X) ← p(1, X).
r(Y) ← r(X), p(X, Y). ← 2 {p(X, Y)} , v(X). ← 2 {p(X, Y)} , v(Y). ← not r(X), v(X).
29 / 30
Example: Hamilton Cycle
Definition: Hamilton cycle problem
Input: graph with vertex set V and edges E ⊆ V × V. Is there a cycle that visits every vertex exactly once?
35 6 12
4
{p(X, Y)} ← e(X, Y). r(X) ← p(1, X).
r(Y) ← r(X), p(X, Y). ← 2 {p(X, Y)} , v(X). ← 2 {p(X, Y)} , v(Y). ← not r(X), v(X).
29 / 30
Example: N-Queens
Definition: N-queens problem
Place N queens on a N × N chessboard so that they do not attack each other, i.e., share no row, column, or diagonal.
Program on paper
4 3 2 1
0Z0Z
Z0Z0
0Z0Z
Z0Z0
1234
30 / 30
Example: N-Queens
Definition: N-queens problem
Place N queens on a N × N chessboard so that they do not attack each other, i.e., share no row, column, or diagonal.
Program on paper
4 3 2 1
0ZQZ
L0Z0
0Z0L
ZQZ0
1234
30 / 30