The doctoral dissertations of the former Helsinki University of Technology (TKK) and Aalto University Schools of Technology (CHEM, ELEC, ENG, SCI) published in electronic format are available in the electronic publications archive of Aalto University - Aaltodoc.
|
|
|
Logic Programs and Cardinality Constraints: Theory and Practice
Tommi Syrjänen
Dissertation for the degree of Doctor of Science in Technology to be presented with due permission of the Faculty of Information and Natural Sciences for public examination and debate in Auditorium T2 at Helsinki University of Technology (Espoo, Finland) on the 20th of March, 2009, at 12 noon.
Dissertation in PDF format (ISBN 978-951-22-9763-4) [1206 KB]
Dissertation is also available in print (ISBN 978-951-22-9762-7)
Abstract
Answer set programming (ASP) is a method for solving hard problems using computational logic. We describe a problem as a set of formulas of a declarative logical language in such way that the solutions correspond to the models (answer sets) of the set and then use a general-purpose inference engine to find the answer sets.
In this work we define an ASP language, cardinality constraint programs (CCP). The language extends normal logic programs by adding cardinality and conditional literals as well as choice rules. These extensions allow us to represent many if not most NP-complete problems in a concise and intuitive way. The language is defined in two phases where we first introduce a simple basic language and then define the constructs of the full language in terms of translations to the basic language.
The language has a declarative formal semantics that is based on the stable model semantics of normal logic programs. The semantics of a program with variables is defined via its ground instantiation. In addition of using the Herbrand instantiation a program can be instantiated with respect to some other universe, which makes it possible to have a direct support for interpreted functions in the semantics.
The semantics is undecidable in the general case. We identify a syntactic subclass of CCPs, namely omega-restricted programs, that are decidable even when function symbols are allowed. The stable models of such programs are created by a finite relevant instantiation that we can always compute. We analyze the computational complexity of omega-restricted programs and show that deciding whether a program has a stable model is 2-NEXP-complete. We identify further subclasses of programs that are NP- and NEXP-complete in the same sense. We also present an algorithm for instantiating omega-restricted programs.
We discuss programming methodology and show how we can create uniform CCP encodings for different problems using the generate-and-test methodology. We examine how we can combine ASP with traditional programming languages by treating an ASP solver as an oracle.
As an extended case study we examine how we can solve AI planning problems using ASP. We present a systematic translation from an action language planning formalism into CCPs and give encodings for three sample planning domains. We also examine how we can add domain-specific knowledge to the encodings to make them more efficient in practice.
Keywords: computational logic, logic programming, answer set programming, stable model semantics, cardinality constraints, planning
This publication is copyrighted. You may download, display and print it for Your own personal use. Commercial use is prohibited.
© 2009 Helsinki University of Technology
Last update 2011-05-26