Simon Dold

Applied combinatorial optimization has witnessed a revolution in performance since the turn of the millennium, but the complexity of modern solvers is making bugs an ever more serious concern. The most promising remedy is to make solvers certifying, so that they use proof logging to generate machine-verifiable proofs of correctness. We present the first example of state-of-the-art certified graph colouring by equipping the solver ZykovColor with VeriPB proof logging. Combined with the formally verified CakePB checker, this provides end-to-end formally certified results. An experimental evaluation shows excellent results with only moderate overhead for proof logging and checking.

Potential functions are a compact and easy way to describe heuristics in classical planning. They are declarative, simple to understand, and clear to explain. Further, they are used as a tool to study the computational complexity of planning problems, and have connections to other concepts such as novelty measures and generalized planning. In this work, we cast potential functions as real-valued multilinear polynomials over the Booleans. While this might seem as a simple syntactic game at first glance, this automatically brings insights to the theory of potential heuristics. For example, we show that the multilinear polynomial representation can be computed using Fourier expansions. This immediately gives us a unique representation for each heuristic function, which allows us to study concepts such as correlation complexity more directly. Moreover, this also connects potential heuristics to a whole new field of computer science -- analysis of Boolean functions -- leading to consequences ranging from learning theory to performance prediction.

There are uncountably many potential heuristics for a given classical planning task and a given set of features. However, if two potential heuristics are sufficiently similar they do not change the behavior of the search algorithm that uses them. For many satisficing planning approaches two heuristics are sufficiently similar if they provide the same weak ordering of the states. In this work, we categorize all potential heuristics of a given task and set of features into equivalence classes. We show that each equivalence class contains one potential heuristic with a representation size polynomial in the number of features. This shows that a non-deterministic Turing Machine is able to guess a potential heuristic from such an equivalence class in polynomial time and closes a small theoretical gap for the complexity of heuristic synthesis for satisficing classical planning Helmert et al. (2022) left.

Existing approaches to delete-relaxation heuristics in classical planning with axioms are based on task transformations, three-valued logic, or answer set programming. We introduce three additional, novel methods that follow the task- transformation approach, internally compiling axioms away. We show that existing task-transformation approaches yield unsafe heuristics and conjecture a well-founded bridge to the three-valued logic approach, resulting in a dominance hierarchy over existing and new methods. Experimental evaluations show that our delete-relaxation methods perform favorably in overall coverage compared to the existing approaches, for both optimal planning with hmax and satisficing planning with hff.

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.

Correlation complexity is a measure of a planning task indicating how hard it is. The introducing work provides sufficient criteria to detect a correlation complexity of 2 on a planning task. It also introduced an example of a planning task with correlation complexity 3. In our work, we introduce a criterion to detect an arbitrary correlation complexity and extend the mentioned example to show with the new criterion that planning tasks with arbitrary correlation complexity exist.

The international planning competition (IPC) is a recurring event that compares the performance of planners and awards the best ones. The evaluation is based on a set of benchmark problems that describe interesting planning problems in PDDL (planning domain definition language). There is a general interest in high-quality benchmarks. Not only for the IPC but for the research of automated planning in general. We explore the possibility of a planning domain modeling competition that produces them. In this work, we discuss the desirable properties of benchmarks and how they could be evaluated.

Classical planning considers a given task and searches for a plan to solve it. Some tasks are harder to solve than others. We can measure the “hardness” of a task with the novelty width and the correlation complexity. In this work, we compare these measures. Additionally, we introduce the river measure, a new measure that is based on potential heuristics and therefore similar to the correlation complexity but also comparable to the novelty width. We show that the river measure is upper bounded by the correlation complexity and by the novelty width +1. Furthermore, we show that we can convert a planning task with a polynomial blowup of the task size to ensure that a heuristic of dimension 2 exists that gives rise to backtrack-free search.