Goal-directed Execution of Answer Set Programs Kyle Marple, Ajay Bansal, Richard Min, Gopal Gupta


Download 0.56 Mb.
Sana21.12.2019
Hajmi0.56 Mb.
  • Kyle Marple, Ajay Bansal, Richard Min, Gopal Gupta
  • Applied Logic, Programming-Languages
  • and Systems (ALPS) Lab
  • The University of Texas at Dallas
  • Outline
  • Answer Set Programming
    • General overview
    • Odd Loops Over Negation (OLONs)
    • Other Implementations
  • Goal-directed execution of ASP Programs
    • Why we want it
    • How we achieve it
  • Our Implementation, Galliwasp
    • Improving performance
    • Benchmark results
  • Related and Future Work
    • Updated benchmark results
  • Answer Set Programming
  • Answer set programming (ASP)
    • Based on Stable Model Semantics
    • Attempts to give a better semantics to negation as failure (not p holds if we fail to establish p)
    • Captures default reasoning, non-monotonic reasoning, etc., in a natural way
  • Applications of ASP
    • Default/Non-monotonic reasoning
    • Planning problems
    • Action Languages
    • Abductive reasoning
  • Serious applications of ASP developed
  • Gelfond-Lifschitz Method
  • Given an answer set program and a candidate answer set S, compute the residual program:
    • for each p ∈ S, delete all rules whose body contains “not p”
    • delete all goals of the form “not q” in remaining rules
  • Compute the least fix point, L, of the residual program
  • If S = L, then S is an answer set
  • ASP
  • Consider the following program, P: p :- not q. t. r :- t, s. q :- not p. s.
  • P has 2 answer sets: {p, r, t, s} & {q, r, t, s}.
  • Now suppose we add the following rule to P: h :- p, not h. (falsify p)
  • Only one answer set remains: {q, r, t, s}
  • Consider another program: p :- not q. q :- not p. r :- not r.
  • No answer set exists
  • Odd Loops Over Negation
  • The rules that cause problems are of the form: h :- p, not h.
  • ASP also allows rules of the form: :- p.
  • Such rules are said to contain Odd Loops Over Negation (OLONs) and force p to be false
  • The two are equivalent, except that in the first case, not h may be called indirectly: h :- p, q, s. s :- r, not h.
  • More generally, the recursive call to h may be under any odd number of negations
  • Implementations of ASP
  • ASP currently implemented using
    • Guess and check + heuristics (Smodels)
    • SAT Solvers (Cmodels, ASSAT) + Learning (CLASP)
  • There are many more implementations available
  • A goal-directed method deemed impossible
  • Several attempts made which either modify the semantics or restrict the program and/or query
  • We present an SLD resolution-style, goal-directed method that works for any ASP program and query
    • One poses a query Q to the system and partial answer sets satisfying Q are systematically computed via backtracking
    • Partial answer sets are subsets of some answer set
  • Why Goal-directed ASP?
  • Most of the time, given a theory, we are interested in knowing if a particular goal is true or not
  • Top down goal-directed execution provides an operational semantics (important for usability)
  • Why check the consistency of the whole knowledgebase?
    • Inconsistency in some unrelated part will scuttle the whole system
  • Why Goal-directed ASP?
  • Many practical examples imitate the use of a query anyway, using a constraint to force the answer set to contain a certain goal
    • E.g. Zebra puzzle: :- not satisfied.
  • With a goal-directed strategy, it is possible to extend ASP to predicates; current execution methodology can only handle finitely groundable programs
  • Goal-directed ASP can be extended (more) naturally
    • with constraints (e.g., CLP(R))
    • with probabilistic reasoning (in style of ProbLog)
  • Abduction can be incorporated with greater ease
  • Or-parallel implementations can be obtained
  • Coinductive LP
  • Our goal-directed procedure relies on coinduction
  • Coinduction is the dual of induction: a proof technique to reason about rational infinite quantities
  • Incorporating coinduction in LP (coinductive LP or Co-LP) allows computation of elements of the GFP
    • Given the rule: p :- p. the query ?-p. will succeed
    • To adhere to stable model semantics, our ASP algorithm disallows; recursive calls with no intervening negation fail
  • Co-LP proofs are infinite in size; they terminate because we are only interested in rational infinite proofs
  • Co-LP is implemented by remembering ancestor calls. If a recursive call unifies with its ancestor call, it succeeds (coinductive hypothesis rule)
  • Negation in Co-LP
  • For ASP, Co-LP must be extended with negation
  • To incorporate negation, a negative coinductive hypothesis rule is needed:
    • In the process of establishing not p, if not p is seen again, then not p succeeds [co-SLDNF Resolution]
  • Given a clause such as p :- q, not p. p fails coinductively when not p is encountered
  • not not p reduces to p
  • Goal-directed Execution
  • Consider an answer set program; we first identify OLON rules and ordinary rules
  • Ordinary rules:
    • contain an even number of negations between the head of a clause and its recursive invocation in the call graph, or are
    • Non-recursive
  • OLON rules:
    • contain an odd number of negations between the head of a clause and its recursive invocation in the call graph p :- q, not r. …Rule 1 Rule 1 is both an ordinary r :- not p. …Rule 2 and an OLON rule q :- t, not p. …Rule 3
  • Ordinary Rules
  • If the head of an OLON rule matches a call, expanding it will always lead to failure
  • So, only ordinary rules produce a successful execution
  • Given a goal G and a program P with only ordinary rules, G can be executed top-down using coinduction:
    • Record each call in a coinductive hypothesis set (CHS)
    • At the time of call c, if c is in CHS, then c succeeds, if not c is in the CHS, the call fails and we backtrack
    • If call c is not in CHS, expand it using a matching rule
    • Simplify not not p to p wherever applicable
    • If no goals left, and success is achieved, the CHS contains a partial answer set
  • Ordinary Rules
  • Consider the following ordinary rules: p :- not q. q :- not p.
  • Two answer sets: {p, not q} and {q, not p}
    • :- p % CHS = {} :- not q % CHS = {p} :- not not p % CHS = {p, not q} :- p % CHS = {p, not q} :- true % success: answer set is {p, not q}
    • :- q % CHS = {} :- not p % CHS = {q} :- not not q % CHS = {q, not p} :- q % CHS = {q, not p} :- true % success: answer set is {q, not p}
  • Every candidate answer set produced by ordinary rules in response to a query must obey the constraints laid down by the OLON rules
  • Consider an OLON rule: p :- B, not p. where B is a conjunction of positive and negative literals
  • A candidate answer set must satisfy (p ∨ not B) to stay consistent with the OLON rule above
  • If p is present in the candidate answer set, then the constraint rule will be removed by the GL method
  • If not, then the candidate answer set must falsify B in order to be a valid partial answer set
  • Handling OLON Rules
  • In general, for the constraint rules with p as their head: p :- B1. p :- B2. ... p :- Bn. generate rule(s) of the form: chk_p1 :- not p, B1. chk_p2 :- not p, B2. ... chk_pn :- not p, Bn.
  • Generate: nmr_chk :- not chk_p1, ... , not chk_pn.
  • Append the NMR check to each query: if user wants to ask a query Q, then ask: ?- Q, nmr_chk.
  • Execution keeps track of positive and negative literals in the answer set (CHS)
  • Goal-directed ASP
  • Consider the following program, A: p :- not q. t. r :- t, s. q :- not p, r. s. h :- p, not h.
  • Separate into OLON and ordinary rules: only 1 OLON rule in this case
  • Execute the query under co-LP to generate candidate answer sets
  • Keep the candidate sets not rejected OLON rules
  • Suppose the query is ?- q.
  • Execution: q  not p, r  not not q, r  q, r  r  t, s  s  success. Ans = {q, r, t, s}
  • Next, we need to check that constraint rules will not reject the generated answer set.
    • it doesn’t in this case as {q, r, t, s} falsifies p
  • Goal-directed ASP
  • Consider the following program, P1: (i) p :- not q. (ii) q:- not r. (iii) r :- not p. (iv) q :- not p.
  • Separate into:
    • 3 OLON rules (i, ii, iii)
    • 2 ordinary rules (i, iv).
  • Generate nmr_chk:
    • p :- not q. q :- not r. r :- not p. q :- not p.
    • chk_p :- not p, not q. chk_q :- not q, not r. chk_r :- not r, not p.
    • nmr_chk :- not chk_p, not chk_q, not chk_r.
  • Suppose the query is ?- r. Expand as in co-LP:
    • r  not p  not not q  q ( not r  fail, backtrack)  not p  success.
  • Ans = {r, q} which satisfies the nmr_chk.
  • Implementation
  • Galliwasp implements our goal-directed procedure
  • Supports A-Prolog with no restrictions on rules or queries
  • Uses grounded programs from lparse; grounded program analyzed further (compiler is ~7400 lines of Prolog)
  • The compiled program is executed by the runtime system (~5,600 lines of C) implementing the top-down procedure
  • Given a query Q, it is extended to Q, nmr_chk
  • Q generates candidate sets and nmr_chk tests them
  • Dynamic Reordering of the NMR Check
  • The order of goals and rules becomes very important as goals are tried left to right and rules top to bottom textually
  • Significant amount of backtracking can take place
  • Efficiency can be significantly improved through incremental generate and test
  • Given Q, nmr_chk, as soon as Q generates an element of the candidate answer set, the corresponding checks in nmr_chk will be simplified
  • When a check becomes deterministic, the corresponding call in nmr_chk is reordered to allow immediate execution
  • Galliwasp System Architecture
  • Old Performance Figures
  • Problem
  • Galliwasp
  • Clasp
  • Cmodels
  • Smodels
  • Queens-12
  • 0.033
  • 0.019
  • 0.055
  • 0.112
  • Queens-13
  • 0.034
  • 0.022
  • 0.071
  • 0.132
  • Queens-14
  • 0.076
  • 0.029
  • 0.098
  • 0.362
  • Queens-15
  • 0.071
  • 0.034
  • 0.119
  • 0.592
  • Queens-16
  • 0.293
  • 0.043
  • 0.138
  • 1.356
  • Queens-17
  • 0.198
  • 0.049
  • 0.176
  • 4.293
  • Queens-18
  • 1.239
  • 0.059
  • 0.224
  • 8.653
  • Queens-19
  • 0.148
  • 0.070
  • 0.272
  • 3.288
  • Queens-20
  • 6.744
  • 0.084
  • 0.316
  • 47.782
  • Queens-21
  • 0.420
  • 0.104
  • 0.398
  • 95.710
  • Queens-22
  • 69.224
  • 0.112
  • 0.472
  • N/A
  • Queens-23
  • 1.282
  • 0.132
  • 0.582
  • N/A
  • Queens-24
  • 19.916
  • 0.152
  • 0.602
  • N/A
  • Old Performance Figures
  • Problem
  • Galliwasp
  • Clasp
  • Cmodels
  • Smodels
  • Mapcolor-4x20
  • 0.018
  • 0.006
  • 0.011
  • 0.013
  • Mapcolor-4x25
  • 0.021
  • 0.007
  • 0.014
  • 0.016
  • Mapcolor-4x29
  • 0.023
  • 0.008
  • 0.016
  • 0.018
  • Mapcolor-4x30
  • 0.026
  • 0.008
  • 0.016
  • 0.019
  • Mapcolor-3x20
  • 0.022
  • 0.005
  • 0.009
  • 0.008
  • Mapcolor-3x25
  • 0.065
  • 0.006
  • 0.011
  • 0.010
  • Mapcolor-3x29
  • 0.394
  • 0.006
  • 0.012
  • 0.011
  • Mapcolor-3x30
  • 0.342
  • 0.007
  • 0.012
  • 0.011
  • Schur-3x13
  • 0.209
  • 0.006
  • 0.010
  • 0.009
  • Schur-2x13
  • 0.019
  • 0.005
  • 0.007
  • 0.006
  • Schur-4x44
  • N/A
  • 0.230
  • 1.394
  • 0.349
  • Schur-3x44
  • 7.010
  • 0.026
  • 0.100
  • 0.076
  • Pigeon-10x10
  • 0.020
  • 0.009
  • 0.020
  • 0.025
  • Pigeon-20x20
  • 0.050
  • 0.048
  • 0.163
  • 0.517
  • Pigeon-30x30
  • 0.132
  • 0.178
  • 0.691
  • 4.985
  • Pigeon-8x7
  • 0.123
  • 0.072
  • 0.089
  • 0.535
  • Pigeon-9x8
  • 0.888
  • 0.528
  • 0.569
  • 4.713
  • Pigeon-10x9
  • 8.339
  • 4.590
  • 2.417
  • 46.208
  • Pigeon-11x10
  • 90.082
  • 40.182
  • 102.694
  • N/A
  • Future Work
  • Further improvements to the implementation of Galliwasp
  • Generalize to predicates (datalog ASP); work for call-consistent datalog ASP programs already done
  • Add constraints so that applications like real-time planning can be realized
  • Add support for probabilistic reasoning
  • Realize an or-parallel implementation through stack-splitting
  • Related Work
  • Kakas and Toni: Query driven procedure with argumentation semantics (works for only call-consistent programs)
  • Pareira and Pinto have explored variants of ASP. Given p :- not p. p is in the answer set
  • Bonatti et al: restrict the type of programs that can be executed; inefficient since computations may be executed multiple times
  • Alferes et al: Implementation of abduction; does not handle arbitrary ASP
  • QUESTIONS?


Download 0.56 Mb.

Do'stlaringiz bilan baham:




Ma'lumotlar bazasi mualliflik huquqi bilan himoyalangan ©fayllar.org 2020
ma'muriyatiga murojaat qiling