Logic programming and cardinality constraints : theory and practice

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