Analysis of Planning Instances Without Search

In order to prove classical planning instances unsolvable, state-of-the-art planners resort to a state space search. However, we show here that an incomplete, yet computationally efficient criterion is sometimes sufficient to immediately identify as unsolvable a wide range of planning instances. Based on linear and integer programming, we show in this paper how it can be leveraged, should it fail at first. This criterion is the keystone of various techniques we propose to rewrite and enhance the STRIPS model, so as to gather new information about it. If the newly found bits of information is not sufficient to identify the instance as unsolvable, they still constitute human-readable bits of information that can provide additional insight on the planning instance.