We introduce lower-bound certificates for classical planning tasks, which can be used to prove the unsolvability of a task or the optimality of a plan in a way that can be verified by an independent third party. We describe a general framework for generating lower-bound certificates based on pseudo-Boolean constraints, which is agnostic to the planning algorithm used. As a case study, we show how to modify the A* algorithm to produce proofs of optimality with modest overhead, using pattern database heuristics and hmax as concrete examples. The same proof logging approach works for any heuristic whose inferences can be efficiently expressed as reasoning over pseudo-Boolean constraints.

Standard automated planning employs first-order formulas under closed-world semantics to achieve a goal with a given set of actions from an initial state. We follow a line of research that aims to incorporate background knowledge into automated planning problems, for example by means of ontologies, which are usually interpreted under open-world semantics. We present a new approach for planning with DL-Lite ontologies that combines the advantages of ontology-based action conditions provided by explicit-input knowledge and action bases (eKABs) and ontology-aware action effects under the coherence update semantics. We show that the complexity of the resulting formalism is not higher than that of previous approaches, and provide an implementation via a polynomial compilation into classical planning. An evaluation on existing and new benchmarks examines the performance of a planning system on different variants of our compilation.

Learning-based planning systems learn domain-specific knowledge that helps them to solve unseen tasks from the same planning domain. For this purpose they require a diverse set of training instances. A recent proposal for formal specifications of planning domains allows us to exactly characterize which instances are legal for a domain. We automatically generate planning tasks from such formal specifications by means of a translation to answer set programming. We experimentally examine the scalability of the approach and the suitability for learning-based planning, following the setup of the learning track of the International Planning Competition.

Planning domains are an important notion, e.g. when it comes to restricting the input for generalized planning or learning approaches. However, domains as specified in PDDL cannot fully capture the intuitive understanding of a planning domain. We close this semantic gap and propose using PDDL axioms to characterize the (typically infinite) set of legal tasks of a domain. A minor extension makes it possible to express all properties that can be determined in polynomial time. We demonstrate the suitability of the approach on established domains from the International Planning Competition.

The merge-and-shrink framework is a powerful tool for computing abstraction heuristics for optimal classical planning. Merging is one of its name-giving transformations. It entails computing the product of two factors of a factored transition system. To decide which two factors to merge, the framework uses a merge strategy. While there exist many merge strategies, it is generally unclear what constitutes a strong merge strategy, and a previous analysis shows that there is still lots of room for improvement with existing merge strategies. In this paper, we devise a new scoring function for score-based merge strategies based on answering the question whether merging two factors has any benefits over computing saturated cost partitioning heuristics over the factors instead. Our experimental evaluation shows that our new merge strategy achieves state-of-the-art performance on IPC benchmarks.

Cost-optimal planning is at the heart of planning research, with many existing planners that produce provably optimal solutions. While some applications pose additional restrictions, such as producing shortest (in the number of actions) among the cost-optimal plans, standard cost-optimal planning does not provide such a guarantee. We discuss two possible approaches to produce provably the shortest among the cost-optimal plans, one corresponding to an instantiation of cost-algebraic A∗, the other based on a cost transformation. We formally prove that the new cost-transformation method indeed produces the shortest among the cost-optimal plans and empirically compare the performance of the approaches in different configurations.

Optimal cost partitioning of classical planning heuristics has been shown to lead to excellent heuristic values but is often prohibitively expensive to compute. We analyze the application of Lagrangian decomposition, a classical tool in mathematical programming, to cost partitioning of operator-counting heuristics. This allows us to view the computation as an iterative process that can be seeded with any cost partitioning and that improves over time. In the case of non-negative cost partitioning of abstraction heuristics the computation reduces to independent shortest path problems and does not require an LP solver.

Stubborn sets are an optimality-preserving pruning technique for factored state-space search, for example in classical planning. Their applicability is limited by their computational overhead. We describe a new algorithm for computing stubborn sets that is based on the state variables of the state space, while previous algorithms are based on its actions. Typical factored state spaces tend to have far fewer state variables than actions, and therefore our new algorithm is much more efficient than the previous state of the art, making stubborn sets a viable technique in many cases where they previously were not.

If a planning system outputs a solution for a given problem, it is simple to verify that the solution is valid. However, if a planner claims that a task is unsolvable, we currently have no choice but to trust the planner blindly. We propose a sound and complete class of certificates of unsolvability which can be verified efficiently by an independent program. To highlight their practical use, we show how these certificates can be generated for a wide range of state-of-the-art planning techniques with only polynomial overhead for the planner.

While it is easy to verify that an action sequence is a solution for a classical planning task, there is no such verification capability if a task is reported unsolvable. We are therefore interested in certificates that allow an independent verification of the absence of solutions. We identify promising concepts for certificates that can be generated by a wide range of planning approaches. We present a first proposal of unsolvability certificates and sketch ideas how the underlying concepts can be used as part of a more flexible unsolvability proof system.

We propose techniques for efficiently determining optimal solutions to large logistics planning domain problems. We map a problem instance to a directed graph and show that no more than one vehicle per weakly connected component of the graph is needed for an optimal solution. We propose techniques for efficiently finding the vehicles which must be employed for an optimal solution. Also we develop a strong admissible heuristic based on the analysis of a directed graph, the cycles of which represent situations in the problem state in which a vehicle must visit a location more than once. To the best of our knowledge, ours is the first method that determines optimal solutions for large logistics instances (including the largest instances in the IPC 1998 and IPC 2000 problem sets).

Operator cost partitioning is a well-known technique to make admissible heuristics additive by distributing the operator costs among individual heuristics. Planning tasks are usually defined with non-negative operator costs and therefore it appears natural to demand the same for the distributed costs. We argue that this requirement is not necessary and demonstrate the benefit of using general cost partitioning. We show that LP heuristics for operator-counting constraints are cost-partitioned heuristics and that the state equation heuristic computes a cost partitioning over atomic projections. We also introduce a new family of potential heuristics and show their relationship to general cost partitioning.

We suggest the use of linear temporal logic (LTL) for expressing declarative information about optimal solutions of search problems. We describe a general framework that associates LTLf formulas with search nodes in a heuristic search algorithm. Compared to previous approaches that integrate specific kinds of path information like landmarks into heuristic search, the approach is general, easy to prove correct and easy to integrate with other kinds of path information.

The LM-Cut heuristic is currently the most successful heuristic in optimal STRIPS planning but it cannot be applied in the presence of conditional effects. Keyder, Hoffmann and Haslum recently showed that the obvious extensions to such effects ruin the nice theoretical properties of LM-Cut. We propose a new method based on context splitting that preserves these properties.

List of organizers of the Sixth International Symposium on Combinatorial Search.

This volume contains the papers accepted for presentation at SoCS 2013, the Sixth Annual Symposium on Combinatorial Search, held in Leavenworth, WA, USA on July 11–13, 2013. SoCS 2013 was held in cooperation with AAAI and collocated with the Twenty-Seventh AAAI Conference (AAAI 2013) and the 10th Symposium on Abstraction, Reformulation, and Approximation (SARA 2013).

Optimal solutions for multi-agent pathfinding problems are often too expensive to compute. For this reason, suboptimal approaches have been widely studied in the literature. Specifically, in recent years a number of efficient suboptimal algorithms that are complete for certain subclasses have been proposed at highly-rated robotics and AI conferences, all mentioning that it is an open problem which subclasses of non-optimal multi-agent pathfinding are tractable. However, it turns out that this problem has already been completely solved in another research community in the 1980s by a constructive proof that provides a polynomial algorithm that is complete for the entire class of problems. In this paper, we would like to bring this earlier related work to the attention of the robotics and AI communities.

The pancake problem is a famous search problem where the objective is to sort a sequence of objects (pancakes) through a minimal number of prefix reversals (flips). The best approaches for the problem are based on heuristic search with abstraction (pattern database) heuristics. We present a new class of abstractions for the pancake problem called relative-order abstractions. Relative-order abstractions have three advantages over the object-location abstractions considered in previous work. First, they are size-independent, i.e., do not need to be tailored to a particular instance size of the pancake problem. Second, they are more compact in that they can represent a larger number of pancakes within abstractions of bounded size. Finally, they can exploit symmetries in the problem specification to allow multiple heuristic lookups, significantly improving search performance over a single lookup. Our experiments show that compared to object-location abstractions, our new techniques lead to an improvement of one order of magnitude in runtime and up to three orders of magnitude in the number of generated states.