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

 Sana 21.12.2019 Hajmi 0.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
• 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
• 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.
• 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
• 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?