Planning over Integers: Compilations and Undecidability

Abstract

Restricted Tasks (RT) are a special case of numeric planning characterized by numeric conditions that involve one numeric variable per formula and numeric effects that allow only the addition of constants. Despite this, RTs form an expressive class whose planning problem is undecidable. The restricted nature of RTs often makes problem modeling awkward and unnecessarily complicated. We show that this can be alleviated by compiling mathematical operations that are not natively supported into RTs using macro-like action sequences. With that, we can encode many features found in general numeric planning such as constant multiplication, addition of linear formulas, and integer division and residue. We demonstrate how our compilations can be used to capture challenging mathematical problems such as the (in)famous Collatz conjecture. Our approach additionally gives a simple undecidability proof for RTs, and the proof shows that the number of variables needed to construct an undecidable class of RTs is surprisingly low: two numeric and one propositional variable.