Thomas Krennwallner

ICAPS Conference 2019 Conference Paper

Exact Methods for Extended Rotating Workforce Scheduling Problems

• Lucas Kletzander
• Nysret Musliu
• Johannes Gärtner
• Thomas Krennwallner
• Werner Schafhauser

In many professions daily demand for different shifts varies during the week. The rotating workforce scheduling problem deals with the creation of repeating schedules for such demand and is therefore of high practical relevance. This paper investigates solving this real-life problem with several new practically relevant features. This includes early recognition of certain infeasibility criteria, complex rest time constraints regarding weekly rest time, and optimization goals to deal with optimal assignments of free weekends. We introduce a state-of-the-art constraint model and evaluate it with different extensions. The evaluation shows that many real-life instances can be solved to optimality using a constraint solver. Our approach is under deployment in a state-of-the-art commercial solver for rotating workforce scheduling.

AIJ Journal 2016 Journal Article

Domain expansion for ASP-programs with external sources

• Thomas Eiter
• Michael Fink
• Thomas Krennwallner
• Christoph Redl

Answer set programming (ASP) is a popular approach to declarative problem solving which for broader usability has been equipped with external source access. The latter may introduce new constants to the program (known as value invention), which can lead to infinite answer sets and non-termination; to prevent this, syntactic safety conditions on programs are common which considerably limit expressiveness (in particular, recursion). We present liberal domain-expansion (lde) safe programs, a novel generic class of ASP programs with external source access and value invention that enjoy finite restrictability, i. e. , equivalence to a finite ground version. They use term bounding functions as a parametric notion of safety, which can be instantiated with syntactic, semantic or combined safety criteria; this empowers us to generalize and integrate many other notions of safety from the literature, and modular composition of criteria makes future extensions easy. Furthermore, we devise a grounding algorithm for lde-safe programs which in contrast to traditional algorithms can ground any such program directly without the need for program decomposition. While we present our approach on top of a proposed formalism in order to make the formalization precise, the general concepts carry over to related formalisms and important special cases as well. An experimental evaluation of lde-safety on various applications confirms the practicability of our approach.

JAIR Journal 2015 Journal Article

Distributed Evaluation of Nonmonotonic Multi-context Systems

• Minh Dao-Tran
• Thomas Eiter
• Michael Fink
• Thomas Krennwallner

Multi-context Systems (MCSs) are a formalism for systems consisting of knowledge bases (possibly heterogeneous and non-monotonic) that are interlinked via bridge rules, where the global system semantics emerges from the local semantics of the knowledge bases (also called “contexts”) in an equilibrium. While MCSs and related formalisms are inherently targeted for distributed set- tings, no truly distributed algorithms for their evaluation were available. We address this short- coming and present a suite of such algorithms which includes a basic algorithm DMCS, an ad- vanced version DMCSOPT that exploits topology-based optimizations, and a streaming algorithm DMCS-STREAMING that computes equilibria in packages of bounded size. The algorithms be- have quite differently in several respects, as experienced in thorough experimental evaluation of a system prototype. From the experimental results, we derive a guideline for choosing the appropriate algorithm and running mode in particular situations, determined by the parameter settings.

AIJ Journal 2014 Journal Article

FLP answer set semantics without circular justifications for general logic programs

• Yi-Dong Shen
• Kewen Wang
• Thomas Eiter
• Michael Fink
• Christoph Redl
• Thomas Krennwallner
• Jun Deng

The answer set semantics presented by Faber et al. [27] has been widely used to define so called FLP answer sets for different types of logic programs. However, it was recently observed that when being extended from normal to more general classes of logic programs, this approach may produce answer sets with circular justifications that are caused by self-supporting loops. The main reason for this behavior is that the FLP answer set semantics is not fully constructive by a bottom up construction of answer sets. In this paper, we overcome this problem by enhancing the FLP answer set semantics with a level mapping formalism such that every answer set I can be built by fixpoint iteration of a one-step provability operator (more precisely, an extended van Emden–Kowalski operator for the FLP reduct f Π I ). This is inspired by the fact that under the standard answer set semantics, each answer set I of a normal logic program Π is obtainable by fixpoint iteration of the standard van Emden–Kowalski one-step provability operator for the Gelfond–Lifschitz reduct Π I, which induces a level mapping. The enhanced FLP answer sets, which we call well-justified FLP answer sets, are thanks to the level mapping free of circular justifications. As a general framework, the well-justified FLP answer set semantics applies to logic programs with first-order formulas, logic programs with aggregates, description logic programs, hex-programs etc. , provided that the rule satisfaction is properly extended to such general logic programs. We study in depth the computational complexity of FLP and well-justified FLP answer sets for general classes of logic programs. Our results show that the level mapping does not increase the worst-case complexity of FLP answer sets. Furthermore, we describe an implementation of the well-justified FLP answer set semantics, and report about an experimental evaluation, which indicates a potential for performance improvements by the level mapping in practice.

AAAI Conference 2013 Conference Paper

Liberal Safety for Answer Set Programs with External Sources

• Thomas Eiter
• Michael Fink
• Thomas Krennwallner
• Christoph Redl

Answer set programs with external source access may introduce new constants that are not present in the program, which is known as value invention. As naive value invention leads to programs with infinite grounding and answer sets, syntactic safety criteria are imposed on programs. However, traditional criteria are in many cases unnecessarily strong and limit expressiveness. We present liberal domain-expansion (de-) safe programs, a novel generic class of answer set programs with external source access that has a finite grounding and allows for value invention. De-safe programs use so-called term bounding functions as a parameter for modular instantiation with concrete—e. g. , syntactic or semantic or both—safety criteria. This ensures extensibility of the approach in the future. We provide concrete instances of the framework and develop an operator that can be used for computing a finite grounding. Finally, we discuss related notions of safety from the literature, and show that our approach is strictly more expressive.

JELIA Conference 2012 Conference Paper

Exploiting Unfounded Sets for HEX-Program Evaluation

• Thomas Eiter
• Michael Fink 0001
• Thomas Krennwallner
• Christoph Redl
• Peter Schüller

Abstract HEX programs extend logic programs with external computations through external atoms, whose answer sets are the minimal models of the Faber-Leone-Pfeifer-reduct. As already reasoning from Horn programs with nonmonotonic external atoms of polynomial complexity is on the second level of the polynomial hierarchy, answer set checking needs special attention; simply computing reducts and searching for smaller models does not scale well. We thus extend an approach based on unfounded sets to HEX and integrate it in a Conflict Driven Clause Learning framework for HEX program evaluation. It reduces the check to a search for unfounded sets, which is more efficiently implemented as a SAT problem. We give a basic encoding for HEX and show optimizations by additional clauses. Experiments show that the new approach significantly decreases runtime.

JELIA Conference 2012 Conference Paper

Inconsistency Management for Traffic Regulations: Formalization and Complexity Results

• Harald Beck
• Thomas Eiter
• Thomas Krennwallner

Abstract Smart Cities is a vision driven by the availability of governmental data that fosters many challenging applications. One of them is the management of inconsistent traffic regulations, i. e. , the handling of inconsistent traffic signs and measures in urban areas such as wrong sign posting, or errors in data acquisition in traffic sign administration software. We investigate such inconsistent traffic scenarios and formally model traffic regulations using a logic-based approach for traffic signs and measures, and logical theories describe emerging conflicts on a graph-based street model. Founded on this model, we consider major reasoning tasks including consistency testing, diagnosis, and repair, and we analyze their computational complexity for different logical representation formalisms. Our results provide a basis for an ongoing implementation of the approach.

JELIA Conference 2010 Conference Paper

Decomposition of Distributed Nonmonotonic Multi-Context Systems

• Seif El-Din Bairakdar
• Minh Dao-Tran
• Thomas Eiter
• Michael Fink 0001
• Thomas Krennwallner

Abstract Multi-Context Systems (MCS) are formalisms that enable the interlinkage of single knowledge bases, called contexts, via bridge rules. Recently, a fully distributed algorithm for evaluating heterogeneous, nonmonotonic MCS was described in [7]. In this paper, we continue this line of work and present a decomposition technique for MCS which analyzes the topology of an MCS. It applies pruning techniques to get economically small representations of context dependencies. Orthogonal to this, we characterize minimal interfaces for information exchange between contexts, such that data transmissions can be minimized. We then present a novel evaluation algorithm that operates on a query plan which is compiled with topology pruning and interface minimization. The effectiveness of the optimization techniques is demonstrated by a prototype implementation, which uses an off-the-shelf SAT solver and shows encouraging experimental results.

KR Conference 2010 Conference Paper

Distributed Nonmonotonic Multi-Context Systems

• Minh Dao-Tran
• Thomas Eiter
• Michael Fink
• Thomas Krennwallner

We present a distributed algorithm for computing equilibria of heterogeneous nonmonotonic multi-context systems (MCS). The algorithm can be parametrized to compute only partial equilibria, which can be used for reasoning tasks like query answering or satisfiability checking that need only partial information and not whole belief states. Furthermore, caching is employed to cut redundant solver calls. As a showcase, we instantiate the MCS framework with answer set program contexts. To characterize equilibria of such MCS, we develop notions of loop formulas that enable reductions to the classical satisfiability problem (SAT). Notably, loop formulas for bridge rules between contexts and for the local contexts can be combined to a uniform encoding of an MCS into a (distributed) SAT instance. As a consequence, we can use SAT solvers for belief set building. We demonstrate this approach by an experimental prototype implementation, which uses an off-the-shelf SAT solver.

JELIA Conference 2010 Conference Paper

The DMCS Solver for Distributed Nonmonotonic Multi-Context Systems

• Seif El-Din Bairakdar
• Minh Dao-Tran
• Thomas Eiter
• Michael Fink 0001
• Thomas Krennwallner

Abstract The DMCS system is an implementation of the equilibrium semantics for heterogeneous and nonmonotonic multi-context systems (MCS) [3], which feature contexts with heterogeneous and possibly nonmonotonic logics. Each context in an MCS comprises of two parts: a local knowledge base and a set of bridge rules that can access the beliefs of other contexts and add new information to the knowledge base. In this setting, contexts are loosely coupled, and may model distributed information linkage applications; thus it is natural to have a system that allows for the distributed evaluation of MCS.

IJCAI Conference 2009 Conference Paper

• Thomas Eiter
• Michael Fink
• Thomas Krennwallner

We present a method to decompose a declarative knowledge base, given by a logic program under Answer Set Semantics with access to external sources. It overcomes the ineffectiveness of current methods due to a lack of structural information about these sources, viewed as black boxes, by exploiting independency information in accesses to them. To this end, we develop a generic notion of domain independence that allows to restrict the evaluation domain and, as a consequence, to prune unnecessary dependency assumptions between atoms. This leads to increased decomposability; we demonstrate this by an evaluation method for HEX-programs based on program rewriting, which may yield large performance gains. While developed for a particular formalism, the notions and ideas of this paper might be adapted to related formalisms as well.