Remo Christen

Algorithms are usually shown to be correct on paper, but bugs in their implementations can still lead to incorrect results. In the case of classical planning, it is fortunately straightforward to check whether a computed plan is correct. For optimal planning, however, plans are additionally required to have minimal cost, which is significantly more difficult to verify. While some domain-specific approaches exists, we lack a general tool to verify optimality for arbitrary problems. We bridge this gap and introduce two approaches based on the principle of certifying algorithms, which provide a computer-verifiable certificate of correctness alongside their answer. We show that both approaches are sound and complete, analyze whether they can be generated and verified efficiently, and show how to apply them to concrete planning algorithms. The experimental evaluation shows that verifying optimality comes with a cost, but is still practically feasible. Furthermore, it confirms that the tested planner configurations provide optimal plans on the given instances, as all certificates were verified successfully.

In classical planning, the aim is to find a sequence of deterministic actions leading from the initial to a goal state. In this work, we consider the scenario where a party who knows the solution to a planning task, called the prover, wants to convince a second party, the verifier, that it has the solution without revealing any information about the solution itself. This is relevant in domains where privacy is important, for example when plans contain sensitive information or when the solution should not be revealed upfront. We achieve this by introducing a zero-knowledge protocol for plan existence. By restricting ourselves to tasks with polynomially-bounded plan length, we are able to construct a protocol that can be run efficiently by both prover and verifier. The resulting protocol does not rely on any reduction, has a constant number of rounds, and runs in time polynomial in the size of the task.

While the unsolvability IPC sparked a multitude of planners proficient in detecting unsolvable planning tasks, there are gaps where concise unsolvability arguments are known but no existing planner can capture them without prohibitive computational effort. One such example is the sliding tiles puzzle, where solvability can be decided in polynomial time with a parity argument. We introduce separating functions, which can prove that one state is unreachable from another, and show under what conditions a potential function over any nonzero ring is a separating function. We prove that we can compactly encode these conditions for potential functions over features that are pairs, and show in which cases we can efficiently synthesize functions satisfying these conditions. We experimentally evaluate a domain-independent algorithm that successfully synthesizes such separating functions from PDDL representations of the sliding tiles puzzle, the Lights Out puzzle, and Peg Solitaire.