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.

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.

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.

Extending programming languages with stochastic behaviour such as probabilistic choices or random sampling has a long tradition in computer science. A recent development in this direction is a declarative probabilistic programming language, proposed by Barany et al. in 2017, which operates on standard relational databases. In particular, Barany et al. proposed generative Datalog, a probabilistic extension of Datalog that allows sampling from discrete probability distributions. Intuitively, the output of a generative Datalog program P on an input database D is a probability space over the minimal models of D and P, the so-called possible outcomes. This is a natural generalization of the (deterministic) semantics of Datalog, where the output of a program on a database is their unique minimal model. A natural question to ask is how generative Datalog can be enriched with the useful feature of negation, which in turn leads to a strictly more expressive declarative probabilistic programming language. In particular, the challenging question is how the probabilistic semantics of generative Datalog with negation can be robustly defined. Our goal is to provide an answer to this question by interpreting negation according to the stable model semantics.

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.

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.

Abstract In the context of planning and reasoning about actions and change, we call an action reversible when its effects can be reverted by applying other actions, returning to the original state. Renewed interest in this area has led to several results in the context of the PDDL language, widely used for describing planning tasks. In this paper, we propose several solutions to the computational problem of deciding the reversibility of an action. In particular, we leverage an existing translation from PDDL to Answer Set Programming (ASP), and then use several different encodings to tackle the problem of action reversibility for the STRIPS fragment of PDDL. For these, we use ASP, as well as Epistemic Logic Programming (ELP), an extension of ASP with epistemic operators, and compare and contrast their strengths and weaknesses.

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 first 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.

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.

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.

Abstract 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 the prototype ELP solving system “selp,” which we present in this paper. This solver exhibits competitive performance on a set of ELP benchmark instances.

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.

Abstract Epistemic Logic Programs (ELPs) extend Answer Set Programming (ASP) with epistemic negation and have received renewed interest in recent years. This led to the development of new research and efficient solving systems for ELPs. In practice, ELPs are often written in a modular way, where each module interacts with other modules by accepting sets of facts as input, and passing on sets of facts as output. An interesting question then presents itself: under which conditions can such a module be replaced by another one without changing the outcome, for any set of input facts? This problem is known as uniform equivalence, and has been studied extensively for ASP. For ELPs, however, such an investigation is, as of yet, missing. In this paper, we therefore propose a characterization of uniform equivalence that can be directly applied to the language of state-of-the-art ELP solvers. We also investigate the computational complexity of deciding uniform equivalence for two ELPs, and show that it is on the third level of the polynomial hierarchy.

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.

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 the 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 define the class of connection-guarded programs, which guarantees that the treewidth of the program after grounding only depends on the treewidth (and the degree) of the input instance. In order to obtain this result, we formalize the grounding process using MSO transductions.

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.

Normal tuple-generating dependencies (NTGDs) are TGDs enriched with default negation, a.k.a. negation as failure. Query answering under NTGDs, where negation is interpreted according to the stable model semantics, is an intriguing new problem that gave rise to flourishing research activity in the database and KR communities. So far, all the existing works that investigate this problem, except for one recent paper that adopts an operational semantics based on the chase, follow the so-called logic programming (LP) approach. According to the LP approach, the existentially quantified variables are first eliminated via Skolemization, which leads to a normal logic program, and then the standard stable model semantics for normal logic programs is applied. However, as we discuss in the paper, Skolemization is not appropriate in the presence of default negation since it fails to capture the intended meaning of NTGDs, while the operational semantics mentioned above fails to overcome the limitations of the LP approach. This reveals the need to adopt an alternative approach to stable model semantics that is directly applicable to NTGDs with existentially quantified variables. We propose such an approach based on a recent characterization of stable models in terms of second-order logic, which indeed overcomes the limitations of the LP approach. We then perform an in-depth complexity analysis of query answering under prominent classes of NTGDs based on the main decidability paradigms for TGDs, namely weak-acyclicity, guardedness and stickiness. Interestingly, weakly-acyclic NTGDs give rise to robust and highly expressive query languages that allow us to solve in a declarative way problems in the second level of the polynomial hierarchy.

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.

We perform an in-depth complexity analysis of query answering under guarded-based classes of disjunctive tuple-generating dependencies (DTGDs), focusing on (unions of) conjunctive queries ((U)CQs). We show that the problem under investigation is very hard, namely 2E xp T ime -complete, even for fixed sets of dependencies of a very restricted form. This is a surprising lower bound that demonstrates the enormous impact of disjunction on query answering under guarded-based tuple-generating dependencies, and also reveals the source of complexity for expressive logics such as the guarded fragment of first-order logic. We then proceed to investigate whether prominent subclasses of (U)CQs (i.e., queries of bounded treewidth and hypertree-width, and acyclic queries) have a positive impact on the complexity of the problem under consideration. We show that queries of bounded treewidth and bounded hypertree-width do not reduce the complexity of our problem, even if we focus on predicates of bounded arity or on fixed sets of DTGDs. Regarding acyclic queries, although the problem remains 2E xp T ime -complete in general, in some relevant settings the complexity reduces to E xp T ime -complete. Finally, with the aim of identifying tractable cases, we focus our attention on atomic queries. We show that atomic queries do not make the query answering problem easier under classes of guarded-based DTGDs that allow more than one atom to occur in the body of the dependencies. However, the complexity significantly decreases in the case of dependencies that can have only one atom in the body. In particular, we obtain a P time -completeness if we focus on predicates of bounded arity, and AC 0 -membership when the set of dependencies and the query are fixed. Interestingly, our results can be used as a generic tool for establishing complexity results for query answering under various description logics.

Abstract Answer set programming (ASP) is a well-established logic programming language that offers an intuitive, declarative syntax for problem solving. In its traditional application, a fixed ASP program for a given problem is designed and the actual instance of the problem is fed into the program as a set of facts. This approach typically results in programs with comparably short and simple rules. However, as is known from complexity analysis, such an approach limits the expressive power of ASP; in fact, an entire NP-check can be encoded into a single large rule body of bounded arity that performs both a guess and a check within the same rule. Here, we propose a novel paradigm for encoding hard problems in ASP by making explicit use of large rules which depend on the actual instance of the problem. We illustrate how this new encoding paradigm can be used, providing examples of problems from the first, second, and even third level of the polynomial hierarchy. As state-of-the-art solvers are tuned towards short rules, rule decomposition is a key technique in the practical realization of our approach. We also provide some preliminary benchmarks which indicate that giving up the convenient way of specifying a fixed program can lead to a significant speed-up.

Abstract In this work, we propose Answer-Set Programming (ASP) as a tool for rapid prototyping of dynamic programming algorithms based on tree decompositions. In fact, many such algorithms have been designed, but only a few of them found their way into implementation. The main obstacle is the lack of easy-to-use systems which (i) take care of building a tree decomposition and (ii) provide an interface for declarative specifications of dynamic programming algorithms. In this paper, we present D-FLAT, a novel tool that relieves the user of having to handle all the technical details concerned with parsing, tree decomposition, the handling of data structures, etc. Instead, it is only the dynamic programming algorithm itself which has to be specified in the ASP language. D-FLAT employs an ASP solver in order to compute the local solutions in the dynamic programming algorithm. In the paper, we give a few examples illustrating the use of D-FLAT and describe the main features of the system. Moreover, we report experiments which show that ASP-based D-FLAT encodings for some problems outperform monolithic ASP encodings on instances of small treewidth.

A promising approach to tackle intractable problems is given by combining decomposition methods with dynamic programming algorithms. One such decomposition concept is tree decomposition. In this paper, we provide a new algorithm using this combined approach for solving reasoning problems in propositional answer set programming.