Homomorphisms and Embeddings of STRIPS Planning Models

TL;DR

The paper studies formal relationships between STRIPS planning models through homomorphisms, introducing SI (STRIPS Isomorphism) and proving it is $GI$-complete, with quasi-polynomial-time theoretical solvability. It then defines SSI and SSI-H (subinstance homomorphisms) as well as SE (embedding), proving their decision problems are $NP$-complete and providing algorithms to find mappings when they exist. The core contribution is a unified, SAT-based approach augmented by constraint-propagation preprocessing that can efficiently detect subinstance isomorphisms and embeddings, supported by extensive experiments showing preprocessing substantially speeds up SAT solving and improves coverage on benchmark domains. The work highlights practical benefits for plan compilation, unsolvability certification, and potential macro-operator learning, while connecting the theory to symmetry considerations and abstractions in planning.

Abstract

Determining whether two STRIPS planning instances are isomorphic is the simplest form of comparison between planning instances. It is also a particular case of the problem concerned with finding an isomorphism between a planning instance $P$ and a sub-instance of another instance $P_0$ . One application of such a mapping is to efficiently produce a compiled form containing all solutions to P from a compiled form containing all solutions to $P_0$. We also introduce the notion of embedding from an instance $P$ to another instance $P_0$, which allows us to deduce that $P_0$ has no solution-plan if $P$ is unsolvable. In this paper, we study the complexity of these problems. We show that the first is GI-complete, and can thus be solved, in theory, in quasi-polynomial time. While we prove the remaining problems to be NP-complete, we propose an algorithm to build an isomorphism, when possible. We report extensive experimental trials on benchmark problems which demonstrate conclusively that applying constraint propagation in preprocessing can greatly improve the efficiency of a SAT solver.

Figures (5)

• Figure 1: A pair of Rubik's cubes. For both of these puzzles, each face can be rotated 90 degrees, clockwise or counter-clockwise, any number of times. The goal is to reach a configuration where for all six colors, all facets of that color are on the same face, so that faces have a homogeneous color. Note that the respective configurations of the corner pieces of these cubes are similar: any sequence of moves that solves the 3x3x3 cube also solves the 2x2x2 cube.
• Figure 2: Top view of the 2x2x2 cube presented earlier, as well as the resulting configuration after the right face is rotated of a quarter of turn clockwise. Below both configurations, we partially represent the associated state resulting from a formalisation into STRIPS of the puzzle. For instance, the fluent , which is true in the first state, represents the fact that, on the upper face of the cube, the top right facet is blue. After some operator (which, in this case, rotates the right face clockwise) is applied to the state, the facet is no longer blue, but has been replaced by a yellow one, as reflected in the resulting state.
• Figure 3: Two Rubik's cubes of the same shape, that are isomorphic. The one on the right is a copy of the left one, except that colors have been replaced consistently.
• Figure 4: Through an invariance argument, it can be proven that the 2x2x2 cube on the left can not be solved. This cube can be embedded into the 4x4x4 cube on the right: the corners of the 2x2x2 cube can be mapped onto the corners of the 4x4x4 cube. When one only considers these parts of the 4x4x4 cube, we end up with a puzzle where each move that has an effect on the corner pieces can be mimicked on the smaller cube, and where the goal is to correctly position the corners. Other moves are ignored: for instance, moves that rotate one of the center slices leave the corners in place and are of no interest in this case. As no solution exists for the 2x2x2 cube, no sequence of moves exists that would correctly position the corner pieces on the 4x4x4, as we would end up with a contradiction otherwise. Thus, the 4x4x4 cube presented here can not be solved.
• Figure 5: Number of SSI (top), SSI-H (middle) and SE (bottom) instances that can be solved by our implementation, as a function of the time cutoff. Blue/orange (upper/lower) curves correspond respectively to with/without pruning (constraint propagation preprocessing). The left column reports positive instances (for which a homomorphism could be found), while the right column reports negative instances (for which no homomorphism exists).

Theorems & Definitions (31)

• Definition 1
• Proposition 1: Zemlyachenko et al. 1985zemlyachenko1985graph, Ch. 4, Sec. 15
• Definition 2
• Proposition 2: Zemlyachenko et al. 1985zemlyachenko1985graph, Ch. 4, Sec. 15
• Definition 3: Isomorphism between STRIPS instances
• Proposition 3
• Lemma 1
• proof
• Lemma 2
• proof