Author name cluster

Michael Morak

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

18 papers

2 author rows

KR Conference 2025 Conference Paper

Non-deterministic Action Reversibility: Complexity Results

Jakub Med
Michael Morak
Lukáš Chrpa
Wolfgang Faber

With the recent interest in the reversibility of action effects, i. e. , whether the effects of the action can be undone by applying other actions, the question arose how hard it is to reverse an action in a non-deterministic domain. With the use of phi-reversibility, the paper investigates the computational complexity of weak and strong non-deterministic action reversibility in fully observable non-deterministic domains, showing PSPACE-completeness for all weak variants in question and EXP-hardness and EXP, or NEXP memberships for strong variants.

PDF Details DOI

ICAPS Conference 2024 Conference Paper

Weak and Strong Reversibility of Non-deterministic Actions: Universality and Uniformity

Jakub Med
Lukás Chrpa
Michael Morak
Wolfgang Faber 0001

Classical planning looks for a sequence of actions that transform the initial state of the environment into a goal state. Studying whether the effects of an action can be undone by a sequence of other actions, that is, action reversibility, is beneficial, for example, in determining whether an action is safe to apply. This paper deals with action reversibility of non-deterministic actions, i. e. , actions whose application might result in different outcomes. Inspired by the established notions of weak and strong plans in non-deterministic (or FOND) planning, we define the notions of weak and strong reversibility for non-deterministic actions. We then focus on the universality and uniformity of action reversibility, that is, whether we can always undo all possible effects of the action by the same means (i. e. , policy), or whether some of the effects can never be undone. We show how these classes of problems can be solved via classical or FOND planning and evaluate our approaches on FOND benchmark domains.

Details

AAAI Conference 2023 Conference Paper

Evaluating Epistemic Logic Programs via Answer Set Programming with Quantifiers

Wolfgang Faber
Michael Morak

In this paper we introduce a simple way to evaluate epistemic logic programs by means of answer set programming with quantifiers, a recently proposed extension of answer set programming. The method can easily be adapted for most of the many semantics that were proposed for epistemic logic programs. We evaluate the proposed transformation on existing benchmarks using a recently proposed solver for answer set programming with quantifiers, which relies on QBF solvers.

PDF Details DOI

AIJ Journal 2023 Journal Article

Solving Projected Model Counting by Utilizing Treewidth and its Limits

Johannes K. Fichte
Markus Hecher
Michael Morak
Patrick Thier
Stefan Woltran

In this paper, we introduce a novel algorithm to solve projected model counting (PMC). PMC asks to count solutions of a Boolean formula with respect to a given set of projection variables, where multiple solutions that are identical when restricted to the projection variables count as only one solution. Inspired by the observation that the so-called “treewidth” is one of the most prominent structural parameters, our algorithm utilizes small treewidth of the primal graph of the input instance. More precisely, it runs in time O ( 2 2 k + 4 n 2 ) where k is the treewidth and n is the input size of the instance. In other words, we obtain that the problem PMC is fixed-parameter tractable when parameterized by treewidth. Further, we take the exponential time hypothesis (ETH) into consideration and establish lower bounds of bounded treewidth algorithms for PMC, yielding asymptotically tight runtime bounds of our algorithm. While the algorithm above serves as a first theoretical upper bound and although it might be quite appealing for small values of k, unsurprisingly a naive implementation adhering to this runtime bound suffers already from instances of relatively small width. Therefore, we turn our attention to several measures in order to resolve this issue towards exploiting treewidth in practice: We present a technique called nested dynamic programming, where different levels of abstractions of the primal graph are used to (recursively) compute and refine tree decompositions of a given instance. Further, we integrate the concept of hybrid solving, where subproblems hidden by the abstraction are solved by classical search-based solvers, which leads to an interleaving of parameterized and classical solving. Finally, we provide a nested dynamic programming algorithm and an implementation that relies on database technology for PMC and a prominent special case of PMC, namely model counting (#Sat). Experiments indicate that the advancements are promising, allowing us to solve instances of treewidth upper bounds beyond 200.

Details DOI

KR Conference 2021 Short Paper

Sticky Existential Rules and Disjunction are Incompatible

Michael Morak

Stickiness is one of the well-known properties in the literature that guarantees decidability of query answering under sets of existential rules, that is, Datalog rules extended with existential quantification in rule heads. In this note, we investigate whether this remains true in the case when rule heads are allowed to be disjunctive. We answer this question in the negative, providing a strong undecidability result that shows that the concept of stickiness cannot be extended to disjunctive existential rules, even when considering only fixed atomic queries and a fixed set of rules. This provides evidence that, in order to keep query answering decidable, a stronger property than stickiness is needed in the disjunctive case.

PDF Details DOI

KR Conference 2021 Short Paper

Universal and Uniform Action Reversibility

Lukáš Chrpa
Wolfgang Faber
Michael Morak

The problem of action reversibility studies whether effects of a given action can be reversed (or undone) by a sequence of (other) actions. For example, actions whose effects can be reversed cannot lead to dead-ends. In the usual settings, the problem of action reversibility is PSPACE-complete, that is, as hard as deciding plan existence. In this paper, we focus on subclasses of the action reversibility problem, universal and uniform action reversibility, where the former considers all states in which the action in question is applicable, while the latter requires a single reverting action sequence, independent of the considered states. Specifically, we study the relations between projection abstractions and the subclasses of the action reversibility problem and we show that universal uniform reversibility of a given action can be decided on projection consisting of only the variables present in the schema of the action in question.

PDF Details DOI

KR Conference 2020 Conference Paper

On the Reversibility of Actions in Planning

Michael Morak
Lukas Chrpa
Wolfgang Faber
Daniel Fišer

Checking whether action effects can be undone is an important question for determining, for instance, whether a planning task has dead-ends. In this paper, we investigate the reversibility of actions, that is, when the effects of an action can be reverted by applying other actions, in order to return to the original state. We propose a broad notion of reversibility that generalizes previously defined versions and investigate interesting properties and relevant restrictions. In particular, we propose the concept of uniform reversibility that guarantees that an action can be reverted independently of the state in which the action was applied, using a so-called reverse plan. In addition, we perform an in-depth investigation of the computational complexity of deciding action reversibility. We show that reversibility checking with polynomial-length reverse plans is harder than polynomial-length planning and that, in case of unrestricted plan length, the PSPACE-hardness of planning is inherited. In order to deal with the high complexity of solving these tasks, we then propose several incomplete algorithms that may be used to compute reverse plans for a relevant subset of states.

PDF Details DOI

AAAI Conference 2020 Conference Paper

Structural Decompositions of Epistemic Logic Programs

Markus Hecher
Michael Morak
Stefan Woltran

Epistemic logic programs (ELPs) are a popular generalization of standard Answer Set Programming (ASP) providing means for reasoning over answer sets within the language. This richer formalism comes at the price of higher computational complexity reaching up to the fourth level of the polynomial hierarchy. However, in contrast to standard ASP, dedicated investigations towards tractability have not been undertaken yet. In this paper, we give ﬁrst results in this direction and show that central ELP problems can be solved in linear time for ELPs exhibiting structural properties in terms of bounded treewidth. We also provide a full dynamic programming algorithm that adheres to these bounds. Finally, we show that applying treewidth to a novel dependency structure—given in terms of epistemic literals—allows to bound the number of ASP solver calls in typical ELP solving procedures.

PDF Details

JAIR Journal 2020 Journal Article

The Impact of Treewidth on Grounding and Solving of Answer Set Programs

Bernhard Bliem
Michael Morak
Marius Moldovan
Stefan Woltran

In this paper, we aim to study how the performance of modern answer set programming (ASP) solvers is influenced by the treewidth of the input program and to investigate the consequences of this relationship. We first perform an experimental evaluation that shows that the solving performance is heavily influenced by treewidth, given ground input programs that are otherwise uniform, both in size and construction. This observation leads to an important question for ASP, namely, how to design encodings such that the treewidth of the resulting ground program remains small. To this end, we study two classes of disjunctive programs, namely guarded and connection-guarded programs. In order to investigate these classes, we formalize the grounding process using MSO transductions. Our main results show that both classes guarantee that the treewidth of the program after grounding only depends on the treewidth (and the maximum degree, in case of connection-guarded programs) of the input instance. In terms of parameterized complexity, our findings yield corresponding FPT results for answer-set existence for bounded treewidth (and also degree, for connection-guarded programs) of the input instance. We further show that bounding treewidth alone leads to NP-hardness in the data complexity for connection-guarded programs, which indicates that the two classes are fundamentally different. Finally, we show that for both classes, the data complexity remains as hard as in the general case of ASP.

PDF Details DOI

AAAI Conference 2019 Conference Paper

Strong Equivalence for Epistemic Logic Programs Made Easy

Wolfgang Faber
Michael Morak
Stefan Woltran

Epistemic Logic Programs (ELPs), that is, Answer Set Programming (ASP) extended with epistemic operators, have received renewed interest in recent years, which led to a flurry of new research, as well as efficient solvers. An important question is under which conditions a sub-program can be replaced by another one without changing the meaning, in any context. This problem is known as strong equivalence, and is well-studied for ASP. For ELPs, this question has been approached by embedding them into epistemic extensions of equilibrium logics. In this paper, we consider a simpler, more direct characterization that is directly applicable to the language used in state-of-the-art ELP solvers. This also allows us to give tight complexity bounds, showing that strong equivalence for ELPs remains coNP-complete, as for ASP. We further use our results to provide syntactic characterizations for tautological rules and rule subsumption for ELPs.

PDF Details

SAT Conference 2018 Conference Paper

Exploiting Treewidth for Projected Model Counting and Its Limits

Johannes Klaus Fichte
Markus Hecher
Michael Morak
Stefan Woltran

Abstract In this paper, we introduce a novel algorithm to solve projected model counting ( PMC ). PMC asks to count solutions of a Boolean formula with respect to a given set of projected variables, where multiple solutions that are identical when restricted to the projected variables count as only one solution. Our algorithm exploits small treewidth of the primal graph of the input instance. It runs in time \({\mathcal O}(2^{2^{k+4}} n^2)\) where k is the treewidth and n is the input size of the instance. In other words, we obtain that the problem PMC is fixed-parameter tractable when parameterized by treewidth. Further, we take the exponential time hypothesis (ETH) into consideration and establish lower bounds of bounded treewidth algorithms for PMC, yielding asymptotically tight runtime bounds of our algorithm.

Details

IJCAI Conference 2018 Conference Paper

Single-Shot Epistemic Logic Program Solving

Manuel Bichler
Michael Morak
Stefan Woltran

Epistemic Logic Programs (ELPs) are an extension of Answer Set Programming (ASP) with epistemic operators that allow for a form of meta-reasoning, that is, reasoning over multiple possible worlds. Existing ELP solving approaches generally rely on making multiple calls to an ASP solver in order to evaluate the ELP. However, in this paper, we show that there also exists a direct translation from ELPs into non-ground ASP with bounded arity. The resulting ASP program can thus be solved in a single shot. We then implement this encoding method, using recently proposed techniques to handle large, non-ground ASP rules, into a prototype ELP solving system. This solver exhibits competitive performance on a set of ELP benchmark instances.

PDF Details

IJCAI Conference 2017 Conference Paper

Making Cross Products and Guarded Ontology Languages Compatible

Pierre Bourhis
Michael Morak
Andreas Pieris

Cross products form a useful modelling tool that allows us to express natural statements such as "elephants are bigger than mice", or, more generally, to define relations that connect every instance in a relation with every instance in another relation. Despite their usefulness, cross products cannot be expressed using existing guarded ontology languages, such as description logics (DLs) and guarded existential rules. The question that comes up is whether cross products are compatible with guarded ontology languages, and, if not, whether there is a way of making them compatible. This has been already studied for DLs, while for guarded existential rules remains unanswered. Our goal is to give an answer to the above question. To this end, we focus on the guarded fragment of first-order logic (which serves as a unifying framework that subsumes many of the aforementioned ontology languages) extended with cross products, and we investigate the standard tasks of satisfiability and query answering. Interestingly, we isolate relevant fragments that are compatible with cross products.

PDF Details

IJCAI Conference 2017 Conference Paper

The Impact of Treewidth on ASP Grounding and Solving

Bernhard Bliem
Marius Moldovan
Michael Morak
Stefan Woltran

PDF Details

LOPSTR Conference 2016 Conference Paper

lpopt: A Rule Optimization Tool for Answer Set Programming

Manuel Bichler
Michael Morak
Stefan Woltran

Abstract State-of-the-art answer set programming (ASP) solvers rely on a program called a grounder to convert non-ground programs containing variables into variable-free, propositional programs. The size of this grounding depends heavily on the size of the non-ground rules, and thus, reducing the size of such rules is a promising approach to improve solving performance. To this end, in this paper we announce lpopt, a tool that decomposes large logic programming rules into smaller rules that are easier to handle for current solvers. The tool is specifically tailored to handle the standard syntax of the ASP language (ASP-Core) and makes it easier for users to write efficient and intuitive ASP programs, which would otherwise often require significant hand-tuning by expert ASP engineers. It is based on an idea proposed by Morak and Woltran (2012) that we extend significantly in order to handle the full ASP syntax, including complex constructs like aggregates, weak constraints, and arithmetic expressions. We present the algorithm, the theoretical foundations on how to treat these constructs, as well as an experimental evaluation showing the viability of our approach.

Details

IJCAI Conference 2013 Conference Paper

The Impact of Disjunction on Query Answering under Guarded-Based Existential Rules

Pierre Bourhis
Michael Morak
Andreas Pieris

We study the complexity of conjunctive query answering under (weakly-)(frontier-)guarded disjunctive existential rules, i. e. , existential rules extended with disjunction, and their main subclasses, linear rules and inclusion dependencies (IDs). Our main result states that conjunctive query answering under a fixed set of disjunctive IDs is 2EXPTIME-hard. This quite surprising result together with a 2EX- PTIME upper bound for weakly-frontier-guarded disjunctive rules, obtained by exploiting recent results on guarded negation first-order logic, gives us a complete picture of the computational complexity of our problem. We also consider a natural subclass of disjunctive IDs, namely frontier-one (only one variable is propagated), for which the combined complexity decreases to EXPTIME. Finally, we show that frontier-guarded rules, combined with negative constraints, are strictly more expressive than DL-LiteH bool, one of the most expressive languages of the DL-Lite family. We also show that query answering under DL-LiteH bool is 2EXPTIMEcomplete in combined complexity.

PDF Details DOI

MFCS Conference 2012 Conference Paper

On the Complexity of Ontological Reasoning under Disjunctive Existential Rules

Georg Gottlob
Marco Manna
Michael Morak
Andreas Pieris

Abstract Ontology-based data access is an emerging yet powerful technology that allows to enhance a classical relational database with an ontology in order to infer new intensional knowledge. Recently, Datalog+/- was introduced with the purpose of providing tractable reasoning algorithms for expressive ontology languages. In this framework, Datalog is extended by features such as existential quantification in rule heads, and at the same time the rule syntax is restricted to guarantee decidability, and also tractability, of relevant reasoning tasks. In this paper, we enrich Datalog even more by allowing not only existential quantification but also disjunction in rule heads, and we investigate the complexity of reasoning under the obtained formalism.

Details

JELIA Conference 2010 Conference Paper

A Dynamic-Programming Based ASP-Solver

Michael Morak
Reinhard Pichler
Stefan Rümmele
Stefan Woltran

Abstract We present a novel system for propositional Answer-Set Programming (ASP). This system, called dynASP, is based on dynamic programming and thus significantly differs from standard ASP-solvers which implement techniques stemming from SAT or CSP.

Details