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 Pi, 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 ≥ 0, a formula Pi^precn in which (i) the pattern prec is computed only for n=0 in the initial state I of Pi, 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 Pi^precn 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 prech -- to be used in the next step -- in P, (iii) refine the pattern precg 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 precg and prech to define the pattern prec to be used in the search. In particular, at each step, we define a formula PiprecS,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.