Problem Compilation for Multi-Agent Path Finding: a Survey

1 Introduction

Compilation is one of the most prominent technique used in computing. In the context of problem solving in artificial intelligence, compilation is represented by a reduction of an input instance from its source formalism to a different usually well established formalism for which an efficient solver exists. The reduction is often fast so that obtaining the instance in the target formalism and interpreting the solution back to the source formalism consumes only a small portion of the total time while the most of time is spent by the solver. The key idea behind using compilation in problem solving is that the solving process benefits from the advancements in the solver for the target formalism, often accumulated over decades.

The compilation-based solving approach has been applied successfully in solving combinatorial problems like planning [Ghallab et al., 2004], verification [Bradley and Manna, 2007], or scheduling [Blazewicz et al., 2004] where the target formalism is often represented by Boolean satisfiability (SAT) [Biere et al., 2021], mixed integer linear programming (MILP) [J¨unger et al., 2010; Rader, 2010], answer set programming (ASP) [Lifschitz, 2019] or constraint satisfaction (CSP) [Dechter, 2003], all being at the NP-hard level w.r.t. the computational complexity perspective. Significant advancements have been achieved in compilation-based approaches in specific domains, namely in multi-agent path finding (MAPF) [Silver, 2005; Ryan, 2008; Standley, 2010] that we are focusing on in this survey.

The standard MAPF is the problem of finding collisionfree paths for a set of agents from their starting positions to individual goal positions (Figure 1). Agents move in a discrete environment which is modeled as an undirected graph G = (V, E), where vertices represent positions and edges the possibility of moving between the positions. Agents are often denoted A = {a1, a2, ..., ak}, k ≤ |V |, placed in vertices of the graph, moving instantaneously between vertices provided that there is always at most one agent in a vertex and no two agents traverse an edge in opposite directions 1 .

There are numerous applications of MAPF in warehouse logistics [Li et al., 2020b], traffic optimization [Mohanty et al., 2020], multi-robot systems [Preiss et al., 2017], and computer games [Snape et al., 2012] to name few.

Relatively simple formulation of MAPF is an important factor that made it accessible for various solving methods including compilation-based approaches. The simultaneous existence of diverse methods for MAPF has fostered mutual cross-fertilization and deeper understanding. Current state-of-the-art compilation-based solvers for MAPF go even beyond the standard single shot reduction-solvinginterpretation loop coined for classical planning by the SATPlan algorithm [Kautz and Selman, 1992] where SAT has been used as the target formalism. Intensive crossfertilization between the dedicated search-based methods for MAPF, that solve the problem directly, and compilation techniques led to numerous improvements in encodings of MAPF in target formalisms but also in how the solver is used, treating it less like a black-box.

1 Different movement rules exist such as permitting the move into a vacant vertex only. There is also large body of works dealing with related problems like pebble motion in graphs [Kornhauser et al., 1984], token swapping, and token permutation in graphs [Bonnet et al., 2018] using similar movement primitives.

The effort culminated recently in a combination of compilation and lazy collision elimination introduced in Conflictbased search algorithm (CBS) [Sharon et al., 2015] resulting in approaches that construct the target encoding lazily in close cooperation with the solver. The solver in these lazy schemes suggests solutions for incomplete encodings of the input instance that do not specify it fully. After checking the interpreted solution against the original specification, that is if it is a valid MAPF solution (agents do not collide, do not jump, do not disappear, and do not appear spontaneously, etc.), the high-level part of the MAPF solver suggests a refinement of the encoding and the process is repeated. This lazy scheme has been implemented using SAT [Surynek, 2019], CSP [Gange et al., 2019], and MILP [Lam et al., 2019] as target formalisms while important differences exist between these approaches.

We summarize how the research in compilation for MAPF came to this point and describe major compilation-based approaches in a simplified and unified way so that core ideas are easily identifiable and accessible for a wider audience.

This survey aims to complement existing surveys on the MAPF topic, namely [Felner et al., 2017] that focuses on MAPF from the point of view of heuristic search, and [Stern, 2019] that focuses more on the MAPF problem itself and its generalizations.

2 An Overview of Target Formalisms

We will first give a brief overview of popular formalisms that are often used as the target of the compilation process.

Constraint satisfaction problem (CSP) is a tuple (X, D, C) where X is a finite set of variables, D is a finite domain of values that can be assigned to variables, and C is a set of constraints in the form of arbitrary relations over the variables, that is a constraint is a subset of the Cartesian product D × D × ...D (the arity corresponds to how many variables participate in the constraint). A solution of CSP is an evaluation of all variables by values from D such that all constraints from C are satisfied.

In MAPF, we can express positions of agents ai at time step t using a variable Xt i ∈ V (indicating that the domain is V ) [Ryan, 2010]. Then constraints expressing the MAPF rules such as: Xt i ̸= Xt+1 i → {Xt i , Xt+1 i } ∈ E, agents use edges (do not skip); and Distinct(Xt1 ,Xt2 , ...,X tk ), agents do not collide in vertices, etc. are added.

The CSP paradigm provides powerful complete search algorithms coupled with constraint propagation and domain filtering techniques that prune the search space [Dechter, 2003]. One of the most significant advantages of CSP in contrast to other paradigms are global constraints, dedicated filtering algorithms often based on matchings for special relations like Distinct (variables should take different values) or more general cardinality constraints, that enforce consistency across large sets of variables [R´egin, 1994]. Using global constraints it is easy to detect that Distinct(Xt1 ,Xt2 ,Xt3 ) cannot be satisfied when D = {v1, v2} but it is hard to see it looking on the individual inequalities Xt i ̸=Xt j separately.

A linear program (LP) is a finite list of linear inequalities plus linear objective, the task is to minimize the objective such that the inequalities hold. Geometrically, the inequalities define a polytope and the objective function defines a gradient so the task is to find some boundary point of the polytope that minimizes the gradient. Formally, the task is to minimize c⊤x subject to Px ≤ b, x ≥ 0, where x is a real vector representing the decision variables, P is a matrix of real coefficients of linear inequalities, and b is another realvalued vector. An optimal solution to linear program can be found in polynomial time however LP is not suitable for discrete decision problems like MAPF due to possible fractional assignment of decision variables.

That is why often some or all decision variables are declared to be integers turning LP into an mixed integer linear program (MILP) or integer linear program (ILP) respectively. Introducing integer decision variables improves the expressive power for discrete problems but on the contrary in makes the problem NP-hard. The important advantage of MIP is natively supported arithmetic hence optimizing with respect to various cumulative objectives used in MAPF can be modeled easily when MILP is used as the target formalism.

Boolean satisfiability (SAT) problem consists in deciding whether there exists a truth-value assignment of variables that satisfies a given Boolean formula. The formula is often specified using the conjunctive normal form (CNF), it is a conjunction of clauses where each clause is a disjunction of literals, where a literal is either a variable or a negation of a variable. SAT is often considered to be a canonical NP-complete problem [Cook, 1971]. A formula in CNF can be regarded through the CSP formalism so that clauses represent individual constraints. Such view actually catalyses mutual cross fertilization between solving algorithms for SAT and CSP. Modern SAT solvers are based on the conflictdriven clause learning algorithm [E´en and S¨orensson, 2003; Audemard and Simon, 2018] that implements constraint propagation and back-jumping techniques known from CSP.

The significant challenge when SAT is used as the target formalism is bridging the original representation of the problem and the yes/no environment of SAT. In the context of MAPF, it is often difficult to handle the objectives that use arithmetic.

The disadvantage in the lack of expressiveness, caused by the fact that Boolean formulae are often far from being human readable, is well balanced by the efficiency of SAT solvers enabled by numerous techniques such as learning, restarts, etc.

The difficulty of encoding problems in the SAT formalism at the low-level led to the development of various high-level languages that enable encoding of problems more intuitively.

One such notable higher level approach used in MAPF is answer set programming (ASP) [Erdem et al., 2013]. The problem in ASP is described as a logic program that is automatically translated to a Boolean formula. The formula is solved by the SAT solver and the outcome is propagated back at the logic program level where it is translated to the human readable form.

We show a part of the ASP program for MAPF to illustrate how the ASP paradigm works, see [Erdem et al., 2013] for the full program. We have atoms path(i, t, v) whose interpretation is that agent ai ∈ A is at vertex v at time step t. These atoms are defined recursively using the rules of a logic program:

The program says that agents' paths start at starting positions 1 and then either traverse an edge or wait in a vertex 2. Ones around the rule specify the number of atoms selected for the answer of the rule, the lower and the upper bounds are specified. Here one of the two instances of path is selected.

ASP allows for specifying constraints which are the rules without the head, eliminating answers that satisfy the body. Constraints can be used to eliminate conflicts in vertices for MAPF as follows:← path(i, t, v), path(j, t, v) (3)

The ASP program is solved via reduction to SAT and by calling the SAT solver. The important advantage of ASP in contrast to plain SAT-based approach is that ASP provides high level language to describe problems and one does not need to construct the target Boolean formula.

3 FromClassical Planning toMAPF

One of the pioneering works that used compilation for problem solving is the SATPlan algorithm reducing the classical planning problem to Boolean satisfiability [Kautz and Selman, 1992]. Classical planning is the task of finding a sequence of actions that transforms a given initial state of some abstract world to a desired goal state. States are described as finite sets of atoms. Actions can add and remove atoms in states provided their preconditions are satisfied.

SATPlan is the important milestone in non-trivial compilation schemes since there is no one-to-one correspondence between the planning instance and the target SAT instance. Instead, a bounded decision variant of the input problem is introduced in which the number of time steps is bounded. The SAT solver is consulted with a sequence of yes/no questions on the bounded variant, whether there exists a plan consisting of a specified number of time steps tmax.

3.1 Time Expansion

Another important concept significantly used by SATPlan is a time expansion that enables representing states at individual time steps inside the target formalism. Decision variables representing atoms are indexed with time steps up to tmax; the variable indexed with 0 < t ≤ tmax is set to TRUE if and only if the corresponding atom holds at time step t.

1 SATPlan(planning problemP) assignment ← consult-SAT-Solver(F )

2 tmax ← 1 3 while TRUE do 4 F ← encode-SAT(P,tmax ) 5 6 if assignment ̸= UNSAT then 7 plan ← interpret(P,assignmnet ) 8 return plan 9 tmax ← tmax + 1

In addition to state variables, there are action variables for each time step t indicating whether given action takes place at t. Constraints ensure that if an action variable at t is set to TRUE then precondition atoms must hold in state variables at time step t and effects must hold in state variables at time step t + 1.

Consider an action that moves agent a from vertex v1 to vertex v2: precond(move) = {at(a, v1)}, effect +(move) = {at(a, v2)}, effect -(move) = {at(a, v1)} for which we need to add the following constraints ∀t ∈ {1, ..., tmax - 1}:

Such encoding can be easily constructed as well as read off in the interpretation phase. The simplified pseudo-code of SATPlan is shown as Algorithm 1.

3.2 Encodings of MAPF

The early compilation-based approaches for MAPF were rooted in the CSP formalism [Ryan, 2010]. Even early SAT-based approaches used CSP-like variables for expressing the positions of agents with domains consisting of all vertices [Surynek, 2012]. These decision variables were represented as a vector consisting of the logarithmic number of bits (Boolean variables) with respect to the size of the domain logspace encoding [Prestwich, 2003]. The disadvantage of logspace encodings in the context of MAPF seems to be weak Boolean constraint propagation and the fact that reachability analysis does not prune out variables from the encoding (removing values from decision variables corresponds to forbidding certain combination of settings of bit vectors but the Boolean variables representing the bits remain).

This is why all following SAT-based compilations of MAPF used direct encoding [Walsh, 2000] where there is a single Boolean variable X t i,v for each agent ai ∈ A, each vertex v ∈ V , and relevant time step t. Despite these decision variables are somewhat redundant they provide a good support for constraint propagation and the reachability analysis can completely remove them from the formula.

4 Milestones inMAPF Compilation

Although modern SAT solvers are powerful they alone are not sufficient and the way how the MAPF instance is presented to the SAT solver is equally important. From my personal perspective, there are two milestones that made the compilation for MAPF a competitive alternative to search-based methods: (1) reachability analysis and (2) lazy refinements.

4.1 Reachability Analysis

The disadvantage of SAT-based compilation for planning is often the big size of the target formula since variables for all ground atoms and all ground actions must be included. Reachability analysis via planning graphs [Blum and Furst, 1997] mitigates this difficulty. The planning graph is a structure representing time expansion of the set of possibly valid atoms across discrete time steps. Starting with the initial state at the first time step, atoms for the next time step are generated first by considering all applicable actions in the previous time step and by adding their positive effects together with atoms from the previous time step. To reduce the growth of the set of atoms, mutual exclusions (mutex) for pairs of atoms and actions are introduced. Whenever two atoms are mutex they cannot satisfy the preconditions of an action and the action is hence pruned out.

Reachability analysis analogous to planning graphs in the domain of MAPF is done via multi-valued decision diagrams (MDDs) [Andersen et al., 2007]. MDDs were surprisingly not used in MAPF compilation for the first time but they were originally applied in the Increasing-cost Tree Search algorithm (ICTS) [Sharon et al., 2013]. The idea of MDD is to represent all paths of the specified cost.

The compilation introduced in the MDD-SAT algorithm [Surynek et al., 2016] is analogous to the more advanced variant of SATPlan with planning graphs [Kautz and Selman, 1999]. Both algorithms use eager compilation, that is, the resulting Boolean formula is constructed in one shot and the SAT solver is regarded as a black-box. The incremental scheme to find a step-optimal plan is also similar to SATPlan.

The role of planning graphs for reachability analysis is substituted by multi-valued decision diagrams (MDDs). MDDi is constructed for each agent ai ∈ A and contains a copy of the underlying graph G for every relevant time step where nodes that are not reachable because they are too far from the starting vertex or from the goal vertex are removed. Directed edges in MDDs represent move and wait actions, that is, they interconnect nodes at consecutive time steps in MDD whose corresponding vertices are either identical or connected in G. A directed path in MDDi corresponds to a plan for agent ai.

Decision Boolean variables X t i,v and E t i,u,v are introduced for each node (v, t) and edge [(u, t); (v, t + 1)] in MDDi respectively. The variables are TRUE iff the agent uses the corresponding vertex or edge at given time step.

To encode MAPF rules, constraints are introduced over these variables. We list here few examples only, for the complete list of constraints see [Surynek et al., 2016]. Collisions in vertices can be ruled out by the following constraint for every v ∈ V and time step t:

The following constraints ensure that directed paths are taken in MDDs. If agent ai appears in u ∈ V at time step t then it must leave through exactly one edge connected to u:

Algorithm 2: SMT-CBS: MAPF via SAT.

1 SMT-CBS(MAPFM) 2 SoC ← lower-Bound(M) 3 conflicts ← ∅ 4 while TRUE do 5 paths ← Bounded-SMT-CBS(M, SoC) 6 if paths ̸= UNSAT then 7 return paths 8 SoC ← SoC + 1 9 Bounded-SMT-CBS(M,SoC) 10 F ←encode-SAT(M,SoC,conflicts) 11 while TRUE do 12 assignment ← consult-SAT-Solver(F ) 13 if assignment ̸= UNSAT then 14 (paths , conflicts ′ ) ← check(M,assignment ) 15 if conflicts ′ = ∅ then 16 return paths 17 for each (ai, aj , v, t) ∈ conflicts ′ do 18 F ← F ∪ (¬X t i,v ∨ ¬X t i,v ) 19 conflicts ← conflicts ∪ conflicts ′ 20 return UNSAT

4.2 Lazy Refinements

Conflict-based search (CBS) [Sharon et al., 2015] is currently the most popular approach for MAPF. It is due to its simple and elegant idea which enables to implement the algorithm relatively easily, its good performance, and openness to various improvements via using heuristics.

From the compilation perspective, the CBS algorithm should be understood as a lazy method that tries to solve an underspecified problem and relies on being lucky to find a correct solution even using this incomplete specification. The completeness of the lazy approach is ensured by incremental additions of refinements that eliminate counterexamples obtained from unlucky solving. Similar concepts of incomplete problem specification and refinement can be found e.g. in logic-based Benders's decomposition [Cir´e et al., 2013] or in Counter Example Abstraction Refinement (GEGAR) [Clarke et al., 2000; Clarke, 2003].

The refinement in the CBS algorithm is carried out by a branching scheme. If the candidate solution is incorrect in terms of MAPF rules, that is, if it is a counterexample, then the search branches for each possible refinement of discovered MAPF rule violation and the refinement is added to the problem specification in each branch. Concretely, the MAPF rule violations are conflicts of pairs of agents such as collision of ai ∈ A and aj ∈ A in v at time step t and the refinements are conflict avoidance constraints for single agents in the form that ai ∈ A should avoid v at time step t (for aj analogously).

While in CBS, the branching scheme must be explicitly implemented, in the compilation-based approach, we can just eliminate MAPF rule violation by adding a new constraint into the problem specification and leave branching to the solver for the target formalism. The CBS inspired SAT-based compilation algorithm SMT-CBS is shown as Algorithm 2. In SMT-CBS, a conflict can be eliminated by adding the following disjunctive constraint (line 18):

In this way, the encoding of MAPF (or any other problem) is built dynamically and eventually may end up by the complete specification of the problem as done in MDD-SAT (or in SATPlan in the context of classical planning).

This approach is commonly known as lazy encoding and is often used in satisfiability modulo theories (SMT) [Katz et al., 2016] as well as in LP, ILP, and MILP where it corresponds to the row generation technique [Muter et al., 2013]. In SMT, we are interested in decision procedures for some complex logic theory T , that is decomposed into the Boolean part given to the SAT solver and decision procedure for the conjunctive fragment of T, denoted DECIDET . The SAT solver and DECIDET cooperate in solving logic formula in T. The SAT solver chooses literals to be set TRUE and DECIDET checks if the chosen combination of literals is feasible and suggests refinements. In this sense, CBS is analogous to this approach where the role of DECIDET is represented by conflict checking procedure (line 14).

As shown by experiments a solution or a proof of that it does not exists is often found for incomplete specification (that is, well before all constraints are added to the encoding). Surprisingly intuitive explanation why this is possible comes from the geometry of linear programming. The finite set of inequalities define a polytope of feasible solutions as an intersection of half-spaces, the boundary of the polytope is made by planes. An optimal feasible solution is an element of some of the planes defining the boundary but not an element of all of them (in other words, some inequalities are satisfied because the optimal solution is deep inside their half-space). Hence, to specify the optimal solution, one does not need all the constraints. Similarly if there is no solution, the polytope is empty. Again this may happen by intersecting only some of the half-spaces.

5 Beyond Simple Time Expansion

Modern MAPF compilation techniques to CSP and MILP do not rely on explicit time expansion. Instead, the target encoding or the parts of it are generated on demand.

5.1 Lazy Conflict-based Search

Lazy-CBS [Gange et al., 2019] uses CSP as a target formalism but in contrast to SMT-CBS it uses variables to establish interaction between the search spaces of individual agents rather than disjunctive clauses as done in SMT-CBS. From the LP perspective, this approach is analogous to column generation [Desaulniers et al., 2005]. A simplified pseudo-code of Lazy-CBS is shown as Algorithm 3.

Lazy-CBS starts with finding individual shortest paths which are found by the CSP solver (line 2). Then similarly as in SMT-CBS, the paths are validated with respect to potential collisions (line 14). If there is no collision, then the path represent valid optimal solution of MAPF. Otherwise,

Algorithm 3: Lazy CBS: MAPF via CSP.

1 Lazy-CBS(MAPFM) 2 costs = (c1, c2, ..., cn) ← lower-Bounds(M) 3 variables ← ∅ 4 while TRUE do 5 paths ←Bounded-LCBS(M, costs) 6 if paths ̸= FAIL then 7 return paths 8 (c1, c2, ..., cn) ← update-Bounds(costs , variables ) 9 Bounded-LCBS(M,costs) 10 (X, D, C) ← encode-CSP(M,costs ,variables ) 11 while TRUE do 12 evaluation ← consult-CSP-Solver((X, D, C)) 13 if evaluation ̸= FAIL then 14 (paths , conflicts ) ← check(M,evaluation) 15 if conflicts = ∅ then 16 return paths 17 for each (ai, aj , v, t) ∈ conflicts do 18 X ← X ∪ {pv,t ∈ A} 19 variables ← variables ∪ {pv,t} 20 return FAIL

there is a collision, say between agents ai and aj in vertex v at time step t. The algorithm introduces a fresh CSP variable pv,t ∈ A plus corresponding constraints indicating which agent is permitted to occupy v at time step t (line 1819). Clearly, the need to evaluate the pv,t variable with a single value effectively eliminates the collision being found (the collision would imply evaluation of the variable with two values). After introducing all variables for eliminating the conflicts, the CSP solver is consulted to find new paths w.r.t. pv,t variables.

In addition, to the conflict elimination mechanism, the Lazy-CBS algorithm introduces cost bounds c1, c2, ..., cn on individual agents rather than having the cumulative cost bound. The individual cost bounds are updated similarly as done in the ICTS algorithm, that is, if the CSP solver concludes that no solution can be found for say agents ai and aj to simultaneously achieve their goals within costs ci and cj respectively, the costs bounds are increased by 1 (line 8).

It is important to note, that the state of the CSP solver can be kept between its invocations (line 12). Hence if a new pv,t variable does not affect already existing agent's path, then the path is kept.

5.2 BCP: Branch Cut and Price

MILP as the target formalism allows for reasoning about both integer and real-valued decision variables which opens opportunities to use decision variables with completely different meaning than in CSP and SAT. Bounding linear objectives is also easier in MILP than in SAT.

The model suggested in the Branch Cut and Price algorithm (BCP) [Lam et al., 2019], simplified pseudo-code shown as Algorithm 4, considers a large but finite pool of paths Π(ai) for each agent ai ∈ A connecting its start and goal vertex (line 2). Decision variables λi,π ∈ [0, 1] determine the proportion of path π ∈ Π(ai) being selected by the agent. Constraints ensure that agents use at least one path and the overall cost of path is minimized resulting in the following initial linear program LP:

The program represents an incomplete encoding of the input instance as collisions between the agents are not forbidden initially. Collision resolution is done lazily similarly as in SMT-CBS and Lazy CBS. Once a vertex collision in v ∈ V is detected in current (fractional) solution {λi,π}, that is the following inequality holds for v:

where sπv ∈ {0, 1} indicates selection of vertex v by path π (1 means the vertex is selected), corresponding collision elimination constraint for vertex v is included into the encoding; that is, the following constraint is added (lines 23-24):

Then cost penalties are introduced for agents using vertex v where the collision happened and the pool of paths is extended with at least one better path for each agent considering the paths' costs and the penalties (lines 25-27). Compared to the SAT-based approach, the extension of the set of candidate paths is more general, more fine grained, and provides a room to integrate heuristics that include more promising paths first. The SAT-based compilation increases the bound of the objective instead, which allows for considering more paths satisfying the bound in future iterations, but such extension adds many new paths all at once without distinguishing if some of them are more promising than others.

On the other hand, the MILP-based approach compared to SAT-based compilation requires to deal with fractional solutions (lines 15-19), which adds non-trivial complexity to the high level solving process. As shown in Algorithm 4, elimination of fractionality of solutions requires to implement branch-and-bound search represented in the code by a nondeterministic choice (line 17).

Experiments show that the method performs well even in its vanilla variant. This can be attributed to the strength of the target MILP solver and to the design of decision variables that are suitable for it.

6 SAT vs. CSP vs. MILP for MAPF

As the pseudo-codes of the SAT-based, the CSP-based, and the MILP-based compilation scheme suggest there are different opportunities how to enhance each approach with MAPF specific heuristics and pruning techniques such as symmetry breaking [Li et al., 2020a] or mutex reasoning [Zhang et al., 2020] etc. In this regard, MILP-based scheme is one the most open for integration of domain specific improvements Algorithm 4: Branch Cut and Price: MAPF via

MILP. 1 BPC-MAPF(MAPFM) 2 Π← initialize-Paths-Pool(M) 3 constraints ← ∅ 4 while TRUE do 5 (paths , Π′ ) ← BCP-Using-Path-Pool(M, Π) 6 if paths ̸= FAIL then 7 return paths 8 Π ← Π′ 9 BPC-Using-Path-Pool(M,Π) 10 while TRUE do 11 LP ← encode-MILP(M, Π, constraints) 12 {λi,π}ai∈A,π∈Π(aa) ← consult-MILP-Solver(LP) 13 conflicts ← check(M,{λi,π}) 14 if conflicts = ∅ then 15 if ∃π ∈ Π, ai ∈ A such that λi,π > 0 ∧ λi,π < 1 then 16 resolvers ← resolve-Fractions({λi,π}) 17 let r ∈ resolvers /* non-deterministic */ 18 constraints ← constraints∪ {r} 19 return (FAIL, Π) 20 else 21 paths ← interpret(M,{λi,π}) 22 return (paths , Π) 23 for each c ∈ conflicts do 24 constraints ← constraints∪ eliminate(c) 25 for i = 1, 2, ..., k do 26 Πbetter ← better-Paths(i,{λi,π},constraints ) 27 Π(ai) ← Π(ai) ∪ Πbetter

as more decisions are made at the high-level, namely branching strategy where heuristics can be included, paths pool refinement that could further guide the search can be modified at the high level.

In contrast to this, SAT-based and CSP-based approaches, leave lot of decisions on general purpose solver into which it is difficult to include any MAPF specific heuristics without changing the implementation of the solver. Hence, the role of the solver is bigger as it solves without any intervention from the high-level the entire NP-hard component of the problem.

7 Conclusion

We believe that the existence of compilation-based MAPF solvers based on diverse formalisms calls for further crossfertilization between them. There is still an open room for integrating MAPF specific heuristics in a more efficient way into the compilation framework. Moreover, we believe that the cooperation of the main MAPF solver and the solver for the target formalism can be much closer such as in the case of DPLL(T) solvers [Katz et al., 2016].

Acknowledgments

This research has been supported by GA ˇCR - the Czech Science Foundation, grant registration number 22-31346S.