The s(ASP) Predicate Answer Set Programming System

By

Kyle Marple, Elmer Salazar
Zhuo Chen, and Gopal Gupta
Department of Computer Science
The University of Texas at Dallas

 

Abstract:

We present the s(ASP) system that computes stable models of normal logic programs, i.e., logic programs extended with negation, in the presence of predicates with arbitrary terms.
Such programs need not have a finite grounding, so traditional methods SAT solver-based
methods do not apply.
Our method relies on the use of an extended Herbrand universe, as well as coinduction, constructive negation and a number of other novel techniques. Using our method, a normal logic program with predicates can be executed directly under the stable model semantics without requiring it to be grounded either before or during execution and without requiring that its variables range over a finite domain.

Our method is quite general and supports the use of terms as arguments, including lists and complex data structures. A prototype implementation has been realized and non-trivial applications
have been developed to demonstrate the feasibility of our method.

 

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 [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:

1. Since SAT solvers can only handle propositional programs, these approaches only work for finitely-groundable programs. That is, programs with structures and lists occurring in arguments of predicates cannot be executed, as grounding of such programs will result in an infinite-sized program (due to the Herbrand universe being infinite). In many instances, lists and structures are essential for representing information.
2. Grounding of the program can lead to an exponential blowup in program size. For programs to be executable in such a system, a programmer has to be aware of how the grounding process works and how the ASP solver works and then they have to write their code in such a way that this blowup is minimized. This places undue burden on the programmer, as the programmer has to have knowledge of the grounding procedure as well as the model-finding process.
3. If the number of constants in the program is large, then a SAT-based approach may be infeasible due to the size of the grounded program that will be created. It is next to impossible to build a large general-purpose knowledge-based system—for example, a medical diagnosis system—using such an approach, as such a knowledge-based system will potentially have tens of thousands of constants. The challenge is exacerbated by the fact that such systems are generally developed incrementally over time.
4. SAT-based ASP solvers do not allow reasoning with real numbers.
5. SAT-based model-finding approaches compute the entire model. That is obviously an overkill. Most of the time users are interested in a specific piece of information. Thus, if we were to develop a general purpose knowledge-based system, then the current ASP systems will compute the entire model, i.e., everything that can be inferred from the knowledge-base will be computed.
6. Often, it is hard to isolate the solution that is embedded in the model that is produced by the SAT solver. For example, if one solves the Tower of Hanoi problem using a SAT-based ASP solver, then the answer set will contain a large set of moves that are in the model. One cannot easily isolate the sequence of moves that represent the solution to the problem.
7. Since ASP systems compute the entire model, even a minor inconsistency in a narrow part of the knowledge base will result in the system concluding that no answer set exists. A practical, large, real-world knowledgebase is very likely going to contain inconsistencies.
8. Justification for why an atom is present in an answer set is difficult to produce.

While SAT solver-based ASP systems such as CLASP are very powerful, their use is limited to solving specific well-defined problems, e.g., resource optimization problems. Their use is suboptimal for implementing large-scale, general-purpose knowledge-based system due to the problems mentioned above.

 

The PDF Version of the complete paper is available.

 

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/

[11] Ajay Bansal, Neda Saeedloei, Gopal Gupta. Timed Planning. Proc. 23rd FLAIRS Conference. AAAI Press. 2010.