Conflict Handling Framework in Generalized Multi-agent Path Finding: Advantages and Shortcomings of Satisfiability Modulo Approach

摘要

We address conflict reasoning in generalizations of multi-agent path finding (MAPF). We assume items placed in vertices of an undirected graph with at most one item per vertex. Items can be relocated across edges while various constraints depending on the concrete type of MAPF must be satisfied. We recall a general problem formulation that encompasses known types of item relocation problems such as multi-agent path finding (MAPF) and token swapping (TSWAP). We show how to express new types of relocation problems in the general problem formulation. We thoroughly evaluate a novel solving method for item relocation that combines satisfiability modulo theory (SMT) with conflict-based search (CBS). CBS is interpreted in the SMT framework where we start with the basic model and refine the model with a collision resolution constraint whenever a collision between items occurs. The key difference between the standard CBS and the SMT-based modification of CBS (SMT-CBS) is that the standard CBS branches the search to resolve the collision while SMT-CBS iteratively adds a single disjunctive collision resolution constraint. Our experimental evaluation revealed that although SMT-CBS performs better than CBS in small densely occupied instances of variants of MAPF, it is outperformed on large sparsely occupied environments. The performed analysis shows that individual paths in large environments of relocation instances can be found faster using simple A*-based algorithm than by the SMT solver. On the other hand the SMT solver performs better when many conflicts between items need to be resolved.