Exploiting Search in Symbolic Numeric Planning with Patterns

In this paper, we present a procedure for numeric planning based on Symbolic Pattern Planning (SPP). Given a numeric planning problem Π, a pattern \prec is a sequence of actions used to define a formula encoding the subsequences of \prec executable from a starting state S. Cardellini, Giunchiglia, and Maratea (2024a) follow the Planning as Satisfiability approach by defining, at each step n \ge 0, a formula Π^\prec_n in which (i) the pattern \prec is computed only for n=0 in the initial state I of Π, and then exploited at each step n, (ii) the starting state S is set to I, and (iii) the set G of goals is required to hold in the last state that can be reached by one of the subsequences of \prec concatenated n times. The procedure begins with n=0, terminates as soon as Π^\prec_n is satisfiable, and otherwise proceeds by incrementing n. In this paper, possibly at each step, (i) we symbolically search for an intermediate state P reachable from I, closer to a goal state, (ii) dynamically recompute the pattern \prec_h -- to be used in the next step -- in P, (iii) refine the pattern \prec_g used to reach P, and (iv) start the new search from the state S which can be either the initial state I or the last computed intermediate state P, exploiting the computed patterns \prec_g and \prec_h to define the pattern \prec to be used in the search. In particular, at each step, we define a formula Π^{\prec}_{S,P} encoding the existence of a state P' closer than P to a goal state, with P' reachable from the starting state S when using the pattern \prec. We present different techniques for producing such formulas, each corresponding to a different strategy for exploring the search space. We prove their correctness and completeness, the latter under certain conditions.