- Kyle Marple, Ajay Bansal, Richard Min, Gopal Gupta
- Applied Logic, Programming-Languages
- and Systems (ALPS) Lab
- The University of Texas at Dallas
- 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 (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
- 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
- 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
- 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
- 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
- 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
- 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
- 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)
- 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
- 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
- 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
- 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
- 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)
- 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
- 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.
- 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
- 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
- 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
Do'stlaringiz bilan baham: |