Detecting Unsolvability Based on Separating Functions


  • Remo Christen University of Basel
  • Salomé Eriksson University of Basel
  • Florian Pommerening University of Basel
  • Malte Helmert University of Basel


Classical Planning, Unsolvability, Parity, Potential Heuristics


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.




How to Cite

Christen, R., Eriksson, S., Pommerening, F., & Helmert, M. (2022). Detecting Unsolvability Based on Separating Functions. Proceedings of the International Conference on Automated Planning and Scheduling, 32(1), 44-52. Retrieved from