Simple Numeric Planning with Two Variables Is Decidable

Abstract

It is known that a simple numeric planning problem (SNP) with one numeric variable is decidable but undecidable with three (Helmert 2002). A more recent result (Gnad et. al 2023) showed undecidability for two numeric and one propositional variable. In this paper, we show the decidability of SNP with exactly two numeric variables. For this, we first partition the state space into a finite number of regions and demonstrate the decidability of SNP when restricted to any of these regions. Afterwards, we develop a correct search algorithm that abstracts from these regions by tracking an infinite number of states following an arithmetic progression pattern. Finally, we prove termination of the search and draw conclusions about the reasons for undecidability for general SNP.