Recent work has shown that classical planning tasks can be compactly factored into deterministic finite automata and solved optimally with constraint programming (CP). In this setting, finding a plan reduces to finding a word accepted by all automata through Regular constraints. So far, however, these automata have had to be carefully handcrafted from PDDL tasks. In this paper, we show that they can instead be generated automatically and used as the basis of CP models. We also show that the resulting framework is easily extensible with additional constraints from the planning literature that strengthen propagation. Our approach solves more tasks than the state of the art in end-to-end CP for classical planning in almost all domains.

As reinforcement learning (RL) agents are deployed in increasingly complex environments, ensuring that their behavior complies with the user's needs has become a central challenge in eXplainable RL (XRL). An agent's policy may solve a given problem, but some of its choices can seem counter-intuitive or surprising to the user, who may have wished to see the agent accomplish its goal in a different way, and may wonder: what if the agent acted with a different intent in mind? Scenarios that answer this question are called counterfactual policies. In this work, we propose a framework that allows the user to request these alternative policies by formulating preferences about the behavior of the agent. These preferences are expressed in Linear Temporal Logic on finite traces (LTLf), a formal yet intuitive language that allows reasoning about deterministic sequences of actions. We synthesize the corresponding counterfactual policies using a multi-objective reinforcement learning algorithm, which produces a diverse set of alternative strategies balancing the agent's original policy with the one envisioned by the user. By comparing these strategies, our framework sheds light on the rationale behind the agent's decisions. Experimental trials show that such a set of policies can be synthesized in reasonable time.

We consider the problem of synthesizing interpretable models that recognize the behaviour of an agent compared to other agents, on a whole set of similar planning tasks expressed in PDDL. Our approach consists in learning logical formulas, from a small set of examples that show how an agent solved small planning instances. These formulas are expressed in a version of First-Order Temporal Logic (FTL) tailored to our planning formalism. Such formulas are human-readable, serve as (partial) descriptions of an agent’s policy, and generalize to unseen instances. We show that learning such formulas is computationally intractable, as it is an NP-hard problem. As such, we propose to learn these behaviour classifiers through a topology-guided compilation to MaxSAT, which allows us to generate a wide range of different formulas. Experiments show that interesting and accurate formulas can be learned in reasonable time.

ABSTRACT Determining whether two STRIPS planning instances are isomorphic is the simplest form of comparison between planning instances. It is also a particular case of the problem concerned with finding an isomorphism between a planning instance and a sub‐instance of another instance . One application of such a mapping is to efficiently produce a compiled form containing all solutions to from a compiled form containing all solutions to . We also introduce the notion of embedding from an instance to another instance , which allows us to deduce that has no solution‐plan if is unsolvable. In this paper, we study the complexity of these problems. We show that the first is GI‐complete and can thus be solved, in theory, in quasi‐polynomial time. While we prove the remaining problems to be NP‐complete, we propose an algorithm to build an isomorphism when possible. We report extensive experimental trials on benchmark problems that demonstrate conclusively that applying constraint propagation in preprocessing can greatly improve the efficiency of a SAT solver.

Abstract Dynamic Belief Update is a model checking problem in Dynamic Epistemic Logic concerning the effect of applying a number of epistemic actions on an initial epistemic model. It can also be considered as a plan verification problem in epistemic planning. The problem is known to be PSPACE-hard. To better understand the source of complexity of the problem, previous research has investigated the complexity of 128 parameterized versions of the problem with parameters such as number of agents and size of epistemic actions. The complexity of many parameter combinations has been determined, but previous research left 14 parameter combinations open. In this paper, we solve all of these open problems. Most of the parameter combinations turns out to be fixed-parameter intractable, except for 3 that are fixed-parameter tractable.

Determining whether two STRIPS planning instances are isomorphic is the simplest form of comparison between planning instances. It is also a particular case of the problem concerned with finding an isomorphism between a planning instance P and a sub-instance of another instance P'. One application of such an isomorphism is to efficiently produce a compiled form containing all solutions to P from a compiled form containing all solutions to P'. In this paper, we study the complexity of both problems. We show that the former is GI-complete, and can thus be solved, in theory, in quasi-polynomial time. While we prove the latter to be NP-complete, we propose an algorithm to build an isomorphism, when possible. We report extensive experimental trials on benchmark problems which demonstrate conclusively that applying constraint propagation in preprocessing can greatly improve the efficiency of a SAT solver.