Janhunen, Tomi (Aalto University) | Nimelä, Ilkka (Aalto University)

Janhunen, Tomi (Aalto University) | Nimelä, Ilkka (Aalto University)

In this article, we give an overview of the answer set programming paradigm, explain its strengths, and illustrate its main features in terms of examples and an application problem. In this article, we give an overview of the answer set programming paradigm, explain its strengths, and illustrate its main features in terms of examples and an application problem.

Janhunen, Tomi (Aalto University) | Nimelä, Ilkka (Aalto University)

Bogaerts, Bart (Aalto University) | Janhunen, Tomi (Aalto University) | Tasharrofi, Shahab (Aalto University)

The formalisms for knowledge representation and reasoning(KR&R) typically have a variety of semantics, each one having its particular application scenarios. However, the KR&Rcommunity cannot readily benefit from such a variety due toa lack of efficient solver technology. This is partly caused bythe fact that solver development is laborious and even accomplishing a working prototype can form a major effort.In this paper, we introduce a new framework that enables us todeclaratively specify a given semantics in second-order logicand to automatically generate a solver from that specification. Hence, KR&R researchers can rapidly develop a solverprototype for their new/existing semantics with a minimal effort. Technically, our framework builds on a recent approachfor nesting SAT solvers based on lazy clause generation.We evaluate our framework in the context of Dung’s argumentation frameworks, logic programming, and propositionallogic subject to standard and non-standard semantics. Weshow for each of those formalisms that one can easily specify its semantics using a few second-order sentences and thatone can effectively obtain a solver for that semantics usingour automated solver generation procedure.For instance, in the case of argumentation frameworks, weobtain 16 different solvers, each solving one of four inference tasks for one of four major argumentation semantics andshow that our solvers (slightly) outperform the best solverfrom the last system competition despite not being tuned forargumentation instances.

Bogaerts, Bart (KU Leuven) | Janhunen, Tomi (Aalto University) | Tasharrofi, Shahab (Aalto University)

We present a new approach towards solving quantifiedBoolean formulas (QBFs) using nested SAT solvers with lazyclause generation. The approach has been implemented ontop of the Glucose solver by adding mechanisms for nestingsolvers as well as clause learning. Our preliminary experiments show that nested SAT solving performs (out of the box)relatively well on QBF, when taking into account that no particular QBF-oriented solving techniques were incorporated.The most important contribution of this work is that it provides a systematic way of lifting advances in SAT solvers toQBFs with low implementation effort.

Koponen, Laura, Oikarinen, Emilia, Janhunen, Tomi, Säilä, Laura

The supertree construction problem is about combining several phylogenetic trees with possibly conflicting information into a single tree that has all the leaves of the source trees as its leaves and the relationships between the leaves are as consistent with the source trees as possible. This leads to an optimization problem that is computationally challenging and typically heuristic methods, such as matrix representation with parsimony (MRP), are used. In this paper we consider the use of answer set programming to solve the supertree construction problem in terms of two alternative encodings. The first is based on an existing encoding of trees using substructures known as quartets, while the other novel encoding captures the relationships present in trees through direct projections. We use these encodings to compute a genus-level supertree for the family of cats (Felidae). Furthermore, we compare our results to recent supertrees obtained by the MRP method.

Gebser, Martin (Aalto University) | Janhunen, Tomi (Aalto University) | Rintanen, Jussi (Aalto University)

Many knowledge representation tasks involve trees or similar structures as abstract datatypes. However, devising compact and efficient declarative representations of such properties is non-obvious and can be challenging indeed. In this paper, we take acyclicity properties into consideration and investigate logic-based approaches to encode them. We use answer set programming as the primary representation language but also consider mappings to related formalisms, such as propositional logic, difference logic, and linear programming.

Janhunen, Tomi, Oikarinen, Emilia, Tompits, Hans, Woltran, Stefan

Practically all programming languages allow the programmer to split a program into several modules which brings along several advantages in software development. In this paper, we are interested in the area of answer-set programming where fully declarative and nonmonotonic languages are applied. In this context, obtaining a modular structure for programs is by no means straightforward since the output of an entire program cannot in general be composed from the output of its components. To better understand the effects of disjunctive information on modularity we restrict the scope of analysis to the case of disjunctive logic programs (DLPs) subject to stable-model semantics. We define the notion of a DLP-function, where a well-defined input/output interface is provided, and establish a novel module theorem which indicates the compositionality of stable-model semantics for DLP-functions. The module theorem extends the well-known splitting-set theorem and enables the decomposition of DLP-functions given their strongly connected components based on positive dependencies induced by rules. In this setting, it is also possible to split shared disjunctive rules among components using a generalized shifting technique. The concept of modular equivalence is introduced for the mutual comparison of DLP-functions using a generalization of a translation-based verification method.

Liu, Guohua (Aalto University) | Janhunen, Tomi (Aalto University) | Niemela, Ilkka (Aalto University)

Answer set programming is a programming paradigm where a given problem is formalized as a logic program whose answer sets correspond to the solutions to the problem. In this paper, we link answer set programming with another widely applied paradigm, viz.~mixed integer programming. As a theoretical result, we establish translations from non-disjunctive logic programs to linear constraints used in mixed integer programming so that the solutions to the constraints correspond to the answer sets of the programs. These translations create the basis for an extended answer set programming language that includes linear constraints as a primitive and enables more compact encodings of problems. On a practical level, we have implemented a prototype system that computes answer sets using a state-of-the-art mixed integer programming solver. The reported experiments demonstrate the effectiveness of this approach applied to a number of optimization problems and problems with variables ranging over large domains.

Oikarinen, Emilia, Janhunen, Tomi

In this paper, a Gaifman-Shapiro-style module architecture is tailored to the case of Smodels programs under the stable model semantics. The composition of Smodels program modules is suitably limited by module conditions which ensure the compatibility of the module system with stable models. Hence the semantics of an entire Smodels program depends directly on stable models assigned to its modules. This result is formalized as a module theorem which truly strengthens Lifschitz and Turner's splitting-set theorem for the class of Smodels programs. To streamline generalizations in the future, the module theorem is first proved for normal programs and then extended to cover Smodels programs using a translation from the latter class of programs to the former class. Moreover, the respective notion of module-level equivalence, namely modular equivalence, is shown to be a proper congruence relation: it is preserved under substitutions of modules that are modularly equivalent. Principles for program decomposition are also addressed. The strongly connected components of the respective dependency graph can be exploited in order to extract a module structure when there is no explicit a priori knowledge about the modules of a program. The paper includes a practical demonstration of tools that have been developed for automated (de)composition of Smodels programs. To appear in Theory and Practice of Logic Programming.