Detecting Unsolvability Based on Separating Functions

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.