Introduction
Answer Set Programming (ASP) [1] has emerged as a successful paradigm for developing intelligent reasoning applications. ASP is based on adding negation as failure to logic programming under the stable model semantics regime [2]. ASP allows for sophisticated reasoning mechanisms that are employed by humans (common sense reasoning, default reasoning, counterfactual reasoning, abductive reasoning, etc.) to be modeled elegantly. Numerous systems have been built to execute answer set programs that are extremely sophisticated and efficient. CLASP is the best representative of these systems [8]. These systems restrict programs to predicates that only have variables and constants as arguments (general structures are not allowed). Answer sets (or stable models) of such programs are computed by grounding the program rules with the (finite) Herbrand universe, suitably transforming it, and then using a SAT solver to compute models of the transformed program. These models of the transformed program are the stable models of the original Answer Set Program. There are many problems with these model-finding approaches that rely on a SAT solver:
Query-driven Execution of Answer Set Programs
We have been working on designing query-driven answer set programming systems [3] for last several years. A query-driven system computes the partial answer set that contains the query. Thus, it does not compute the entire answer set; it computes only those parts of the answer set that are relevant to answering the query. Having a query-driven system addresses problems 5, 6, 7, and 8 mentioned above [4], however, issues mentioned in points 1, 2, 3 and 4 above still remain as problems. To alleviate problems 1, 2, 3 and 4 above, we have extended our system to allow general-purpose predicates. Thus, our extended system, called s(ASP), admits answer set programs containing predicates that are allowed to have variables, constants and structures as arguments [5,6].
Our s(ASP) system does not ground the program. It can be thought of as full Prolog extended with negation-as-failure under the stable model semantics regime [6]. Problem 1, 2, 3 and 4 above are eliminated by s(ASP), since programs do not have to be grounded prior to execution. Note also that incorporating the stable model semantics within Prolog means that not everything has to be modeled using ASP, as is the case if one uses traditional ASP systems. For example, generator predicates can be written using standard Prolog predicates such as member and select; they don't have to be always written using choice rules alone.
As we extend ASP to allow direct execution of predicates, a number of subtleties arise. As an example, consider the following simple program:
d(1).
p(X) :- not d(X).
If we ground this program, we obtain:
d(1).
p(1) :- not d(1).
Given the query ?- p(X)., its execution will always fail (the answer set of the grounded program is {d(1)}). However, execution of the same query with the original program with predicates under s(ASP) should succeed and return the solution {p(X), not d(X) (X =\= 1)} (note that since s(ASP) computes the partial answer set containing the query, both positive and negative atoms have to be specified). Note that the answer set computed by s(ASP) is still compatible with the grounded program, if we restrict X to range over the domain {1}.
As an example of an actual program, consider the answer set program for finding Hamiltonian cycles in a graph:
reachable(V) :- chosen(U, V), reachable(U).
reachable(0) :- chosen(V, 0).
% Every vertex must be reachable.
:- vertex(U), not reachable(U).
% Choose exactly one edge from each vertex.
other(U, V) :-
(U), vertex(V), vertex(W),
\= W, chosen(U, W).
chosen(U, V) :-
(U), vertex(V),
(U, V), not other(U, V).
% Two edges cannot be incident on the same vertex.
:- chosen(U, W), chosen(V, W), U \= V.
% Sample graph: vertices and connecting edges.
vertex(0). vertex(3).
vertex(1). vertex(4).
vertex(2).
edge(0, 1). edge(1, 2).
edge(2, 3). edge(3, 4).
edge(4, 0). edge(4, 1).
edge(4, 2). edge(4, 3).
Notice that the above program has an odd loop over negation. The partial answer set produced for the query ?- reachable(0). is shown below.
{ chosen(0,1), chosen(1,2), chosen(2,3), chosen(3,4), chosen(4,0),
edge(0,1), edge(1,2), edge(2,3), edge(3,4), edge(4,0), edge(4,1),
edge(4,2), edge(4,3), other(0,0), other(0,2), other(0,3),
other(0,4), other(1,0), other(1,1), other(1,3), other(1,4),
other(2,0), other(2,1), other(2,2), other(2,4), other(3,0),
other(3,1), other(3,2), other(3,3), other(4,1), other(4,2),
other(4,3), other(4,4), reachable(0), reachable(1), reachable(2),
reachable(3), reachable(4), vertex(0), vertex(1), vertex(2),
vertex(3), vertex(4), not chosen(0,0), not chosen(0,2), not
chosen(0,3), not chosen(0,4), not chosen(0,Var644) ( Var644 \= 0,
Var644 \= 1, Var644 \= 2, Var644 \= 3, Var644 \= 4 ), not
chosen(1,0), not chosen(1,1), not chosen(1,3), not chosen(1,4), not
chosen(1,Var710) ( Var710 \= 0, Var710 \= 1, Var710 \= 2, Var710 \= 3,
Var710 \= 4 ), not chosen(2,0), not chosen(2,1), not chosen(2,2),
not chosen(2,4), not chosen(2,Var776) ( Var776 \= 0, Var776 \= 1,
Var776\= 2, Var776 \= 3, Var776 \= 4 ), not chosen(3,0), not
chosen(3,1), not chosen(3,2), not chosen(3,3), not chosen(3,Var842)
( Var842 \= 0, Var842 \= 1, Var842 \= 2, Var842 \= 3, Var842 \= 4 ),
not chosen(4,1), not chosen(4,2), not chosen(4,3), not chosen(4,4),
not chosen(4,Var908) ( Var908 \= 0, Var908 \= 1, Var908 \= 2, Var908 \= 3,
Var908 \= 4 ), not chosen(Var627,_) ( Var627 \= 0, Var627 \= 1,
Var627 \= 2, Var627 \= 3, Var627 \= 4 ), not chosen(Var663,1) (
Var663 \= 0, Var663 \= 1, Var663 \= 2, Var663 \= 3, Var663 \= 4 ),
not chosen(Var734,2) ( Var734 \= 0, Var734 \= 1, Var734 \= 2, Var734 \= 3,
Var734 \= 4 ), not chosen(Var805,3) ( Var805 \= 0, Var805 \= 1,
Var805 \= 2, Var805 \= 3, Var805 \= 4 ), not chosen(Var876,4) (
Var876 \= 0, Var876 \= 1, Var876 \= 2, Var876 \= 3, Var876 \= 4 ),
not chosen(Var922,0) ( Var922 \= 0, Var922 \= 1, Var922 \= 2, Var922 \= 3,
Var922 \= 4 ), not edge(0,0), not edge(0,2), not edge(0,3),
not edge(0,4), not edge(1,0), not edge(1,1), not edge(1,3), not
edge(1,4), not edge(2,0), not edge(2,1), not edge(2,2), not
edge(2,4), not edge(3,0), not edge(3,1), not edge(3,2), not
edge(3,3), not edge(4,4), not other(0,1), not other(1,2), not
other(2,3), not other(3,4), not other(4,0), not vertex(Var31) (
Var31 \= 0, Var31 \= 1, Var31 \= 2, Var31 \= 3, Var31 \= 4 ) } .
The s(ASP) system makes several novel contributions:
A prototype implementation of the s(ASP) system has been developed. The system supports abductive reasoning. It also provides justification (proof trace) for a given query. The implementation relies on several novel techniques [6] that include:
Unfortunately, more details cannot be given due to lack of space. They will appear in a forthcoming paper [6]. The correctness of the s(ASP) method has been established. We show that the s(ASP) method is sound for all legal programs and argue that while completeness is in fact impossible to achieve, the method is still useful for a vast majority of practical programs [6]. For finite, ground, legal programs, the method is indeed complete. Note that legal programs are those that obey the following restrictions: (i) operands of arithmetic operations are ground at the time they are executed; (ii) left recursion cannot lead to success; and, (iii) a negatively constrained variable cannot be disunified with or constrained against another negatively constrained variable.
The s(ASP) system is publicly available [5] and has been used to develop a number of non-trivial applications based on ASP; it has also been used to organize an AI hackathon [9]. Some of these applications cannot be executed on traditional ASP systems such as CLASP, as these applications make use of lists and structures to represent information. They have been developed by people who are not experts in ASP. These applications include:
We believe that the ASP paradigm is a very powerful paradigm that allows for complex human thought processes to be elegantly emulated. Complex reasoning patterns that humans use can be elegantly modeled using ASP [7]. However, as argued above, the current model-finding, SAT solver-based approaches are not able to realize the full power of ASP. We argue that query-driven implementations of predicate ASP are crucial to the paradigm's success. An additional advantage of a query-driven approach over model-finding approaches is that in the latter case, everything has to be modeled in the ASP paradigm, while in the former case both the standard logic programming paradigm and the ASP paradigm can be made to work together. Abductive reasoning under the stable model semantics is also better realized in a query-driven approach such as s(ASP).
Significant progress has been made with the realization of the s(ASP) system, however, a considerable amount of research remains to be done. The s(ASP) system suffers from some of the same disadvantages that Prolog systems suffer (e.g., certain left-recursive programs may not terminate or the search may have to be guided by the programmer). For this reason it is important to extend the s(ASP) system with (i) constraint logic programming over finite domains, (ii) constraint logic programming over reals, and (iii) tabled logic programming. Note that due to top-down, query-driven nature of execution, both constraints and tabling can be naturally integrated into s(ASP). Finally, the problem of determining the query-relevant part of a given knowledgebase has been solved for top-down propositional ASP in the Galliwasp system, it remains a subject of research in the predicate case.
Acknowledgment: Support from NSF Grant IIS 1423419 is gratefully acknowledged.
References
[1] C. Baral. Knowledge Representation - Reasoning and Declarative Problem Solving. Cambridge Univ. Press. 2003.
[2] M. Gelfond, V. Lifschitz. The stable model semantics for logic programming. Proc. Joint International Conference and Symposium on Logic Programming, 1070--1080. 1988.
[3] K. Marple, A. Bansal, R. Min, G. Gupta. Goal-directed execution of answer set programs. Proc. PPDP 2012: 35-44
[4] K. Marple, G. Gupta. Dynamic Consistency Checking in Goal-Directed Answer Set Programming. TPLP 14(4-5): 415-427 (2014)
[5] K. Marple, E. Salazar, G. Gupta. The s(ASP) system. https://sourceforge.net/projects/sasp-system/}
[6] K. Marple, E. Salazar, G. Gupta. Computing Stable Models of Normal Logic Programs without Grounding. Forthcoming paper. March 2017.
[7] Z. Chen, K. Marple, E. Salazar, G. Gupta, L. Tamil. A Physician Advisory System for Chronic Heart Failure management based on knowledge patterns. TPLP 16(5-6):604-618, 2016.
[8] M. Gebser, B. Kaufmann, A. Neumann, T. Schaub. clasp: A Conflict-Driven Answer Set Solver, Proc. LPNMR07, 2007. https://potassco.org/
[9] The UT Dallas AI Society. s(ASP) Hackathon. https://hackai16.devpost.com/submissions
[10] A. Sobhi, S. Srirangapalli, K. Marple, E. Salazar, G. Gupta. The UT Dallas Degree Audit System. 2016. http://gradaudit.xyz/