On the Tour Towards DPLL(MAPF) and Beyond

Abstract

We discuss milestones on the tour towards DPLL(MAPF), a multiagent path finding (MAPF) solver fully integrated with the Davis-Putnam-Logemann-Loveland (DPLL) propositional satisfiability testing algorithm through satisfiability modulo theories (SMT). The task in MAPF is to navigate agents in an undirected graph in a non-colliding way so that each agent eventually reaches its unique goal vertex. At most one agent can reside in a vertex at a time. Agents can move instantaneously by traversing edges provided the movement does not result in a collision. Recently attempts to solve MAPF optimally w.r.t. the sumof-costs or the makespan based on the reduction of MAPF to propositional satisfiability (SAT) have appeared. The most successful methods rely on building the propositional encoding for the given MAPF instance lazily by a process inspired in the SMT paradigm. The integration of satisfiability testing by the SAT solver and the high-level construction of the encoding is however relatively loose in existing methods. Therefore the ultimate goal of research in this direction is to build the DPLL(MAPF) algorithm, a MAPF solver where the construction of the encoding is fully integrated with the underlying SAT solver. We discuss the current state-of-the-art in MAPF solving and what steps need to be done to get DPLL(MAPF). The advantages of DPLL(MAPF) in terms of its potential to be alternatively parametrized with MAPFR, a theory of continuous MAPF with geometric agents, are also discussed.

Keywords

• multi agent path finding (MAPF)
• propositional satisfiability (SAT)
• Davis-Putnam-Logemann-Loveland (DPLL)
• satisfiability modulo theories(SMT)

Introduction

In multi-agent path finding (MAPF) [ 11,18,19,20,22,24,30 ] the task is to navigate agents from given starting positions to given individual goals. The standard version of the problem takes place in undirected graph G = (V; E) where agents from set A = fa1; a2; :::; akg are placed in vertices with at most one agent per vertex. The initial configuration of agents in vertices of the graph can be written as 0 : A ! V and similarly the goal configuration as + : A ! V . The task of navigating agents can be expressed as a task of transforming the initial configuration of agents 0 : A ! V into the goal configuration + : A ! V .

Movements of agents are instantaneous and are possible across edges into neighbor vertices assuming no other agent is entering the same target vertex. This formulation Copyright c 2019 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). permits agents to enter vertices being simultaneously vacated by other agents. Trivial case when a pair of agents swaps their positions across an edge is forbidden in the standard formulation. We note that different versions of MAPF exist where for example agents always move into vacant vertices [ 26 ]. We usually denote the configuration of agents at discrete time step t as t : A ! V . Non-conflicting movements transform configuration t instantaneously into next configuration t+1. We do not consider what happens between t and t + 1 in this discrete abstraction. Multiple agents can move at a time hence the MAPF problem is inherently parallel.

In order to reflect various aspects of real-life applications variants of MAPF have been introduced such as those considering kinematic constraints [ 9 ], large agents [ 12 ], or deadlines [ 15 ] - see [ 14 ] for more variants. 1.1

Lazy Construction of SAT Encodings

This paper summarizes the development SMT-CBS [ 28 ], a novel optimal MAPF algorithm that unifies two major approaches to solving MAPF optimally: a search-based approach represented by conflict-based search (CBS) [ 19 ] and a compilation-based approach represented by reducing MAPF to propositional satisfiability (SAT) [ 4 ] in the MDD-SAT algorithm [ 29 ]. The SMT-CBS algorithm rephrases ideas of CBS in the terms of satisfiability modulo theories (SMT) [ 5 ] at the high-level. While at the lowlevel it uses the SAT encoding from MDD-SAT.

Unlike the original CBS that resolves conflicts between agents by branching the search, SMT-CBS refines the propositional model with a disjunctive constraint to resolve the conflict. SMT-CBS hence does not branch at the high-level but instead incrementally extends the propositional model that is consulted with the external SAT solver similarly as it has been done in MDD-SAT. In contrast to MDD-SAT where the propositional model is fully constructed in a single-shot, the propositional model is being built lazily in SMT-CBS as new conflicts appear.

The hypothesis behind the design of SMT-CBS is that in many cases we do not need to add all constraints to form the complete propositional model while still be able to obtain a conflict-free solution. Intuitively we expect that such cases where the incomplete propositional model will suffice are represented by sparsely occupied instances with large environments. The expected benefit in contrast to MDD-SAT is that incomplete model can be constructed and solved faster. On the other hand we expect that the superior performance of MDD-SAT in environments densely populated with agents will be preserved as SMT-CBS will quickly converge the model towards the complete one. 1.2

Towards DPLL(MAPF) / CDCL(MAPF)

SMT-CBS represents a milestone towards an optimal MAPF solver where the SAT solver and the high-level construction of the propositional model are fully integrated, an algorithm we denote DPLL(MAPF). DPLL(T) [ 16 ] commonly denotes an algorithm integrating the SAT solver [ 2 ] with a decision procedure for the conjunctive fragment of some first-order theory T . Similarly as in SMT-CBS the SAT solver decides what literals in a given formula should be set to TRUE in order to satisfy the formula. Subsequently, the decision procedure for the conjunctive fragment checks if the suggested truth value assignment is consistent with T . In our case, the theory is represented by movement rules of MAPF and the formula encodes a question if there is a solution of given MAPF of specified value of the objective.

DPLL stands here for the standard search-based SAT solving procedure (DavisPutnam-Logemann–Loveland) [ 6 ] but in fact we use its more modern variants known as CDCL (Conflict-Driven Clause Learning) [ 21 ], hence precisely our algorithm should be denoted CDCL(MAPF) however we will keep the more common notation DPLL(MAPF) used in the literature.

The organization of the paper is as follows: We first introduce MAPF formally. Then the combination of CBS and MDD-SAT, the recent optimal MAPF algorithm SMT-CBS is recalled. On top of this we discuss the future perspective of DPLL(MAPF) in more details. 2

Multi-Agent Path Finding Formally

The Multi-agent path finding (MAPF) problem [ 22,18 ] consists of an undirected graph G = (V; E) and a set of agents A = fa1; a2; :::; akg such that jAj jV j. Each agent is placed in a vertex so that at most one agent resides in each vertex. The placement of agents is denoted : A ! V . Next we are given initial configuration of agents 0 and goal configuration +.

At each time step an agent can either move to an adjacent vertex or wait in its current vertex. The task is to find a sequence of move/wait actions for each agent ai, moving it from 0(ai) to +(ai) such that agents do not conflict, i.e., do not occupy the same vertex at the same time nor cross the same edge in opposite directions simultaneously. The following definition formalizes the commonly used movement rule in MAPF. An example of MAPF instance is shown in Figure 1.

A a1 B

α0 C

D a2 E a3 F

A B

C a1 α1

D a2

E a3 F

A B a1 α2 = α+ C D a2 a3

E F Definition 1. Valid movement in MAPF. Configuration 0 results from if the following conditions hold: if and only (i) (a) =

edges); (ii) for all a 2 A it holds (a) 6= 0(a) ) :(9b 2 A)( (b) = 0(a) ^ 0(b) = (no two agents crosses an edge in opposite directions); (iii) and for all a; a0 2 A it holds that a 6= a0 ) 0(a) 6= vertex in the next configuration).

0(a) or f (a); 0(a)g 2 E for all a 2 A (agents wait or move along 0(a0) (no two agents share a (a))

Solving MAPF is to find a sequence of configurations [ 0; 1; :::; ] such that i+1 results using valid movements from i for i = 1; 2; :::; 1, and = +. A feasible solution of a solvable MAPF instance can be found in polynomial time [ 32,11 ]; precisely the worst case time complexity of most practical algorithms for finding feasible solutions is O(jV j3) [ 13,31 ].

We are often interested in optimal solutions. In case of the makespan [ 26 ] we just need to minimize in the aforementioned solution sequence. For introducing the sumof-costs objective [ 8,23,20 ] we need more notation as follows: Definition 2. Sum-of-costs objective is the summation, over all k agents, of the number of time steps required to reach the goal vertex. Denoted , where = Pik=1 (path(ai)) and (path(ai)) is an individual path cost of agent ai connecting 0(ai) and +(ai) calculated as the number of edge traversals and wait actions. 1

We note that finding a solution that is optimal (minimal) with respect to either the makespan or the sum-of-costs objective is NP-hard [ 17,25 ]. 3

Unifying Search-based and Compilation-based Approaches

Before introducing SMT-CBS, a unification between the search-based and the compilationbased approach we will briefly discuss both approaches themselves. 3.1

Conflict-based Search

CBS is a representative of search-based approach. CBS uses the idea of resolving conflicts lazily; that is, a solution of MAPF instance is not searched against the complete set of movement constraints that forbids collisions between agents but with respect to initially empty set of collision forbidding constraints that gradually grows as new conflicts appear. The advantage of CBS is that it can find a valid solution before all constraints are added.

The high-level of CBS searches a constraint tree (CT) using a priority queue in breadth first manner. CT is a binary tree where each node N contains a set of collision avoidance constraints N:constraints - a set of triples (ai; v; t) forbidding occurrence of agent ai in vertex v at time step t, a solution N:paths - a set of k paths for individual agents, and the total cost N: of the current solution.

The low-level process in CBS associated with node N searches paths for individual agents with respect to set of constraints N:constraints . For a given agent ai, this is a standard single source shortest path search from 0(ai) to +(ai) that avoids a set of vertices fv 2 V j(ai; v; t) 2 N:constraints g whenever working at time step t. For details see [ 19 ].

CBS stores nodes of CT into priority queue OPEN sorted according to the ascending costs of solutions. At each step CBS takes node N with the lowest cost from OPEN and checks if N:paths represent paths that are valid with respect to MAPF movements 1 The notation path(ai) refers to path in the form of a sequence of vertices and edges connecting 0(ai) and +(ai) while assigns the cost to a given path. Algorithm 1: CBS algorithm for MAPF solving 1 CBS (G = (V; E); A; 0; +) 2 R:constraints ; 3 R:paths fshortest path from 0(ai) to +(ai)ji = 1; 2; :::; kg 4 R: Pik=1 (N:paths(ai)) 5 insert R into OPEN 6 while OPEN 6= ; do 7 N min(OPEN) 8 remove-Min(OPEN) 9 collisions validate(N:paths) 10 if collisions = ; then 11 return N:paths rules - that is, N:paths are checked for collisions. If there is no collision, the algorithms returns valid MAPF solution N:paths. Otherwise the search branches by creating a new pair of nodes in CT - successors of N . Assume that a collision occurred between agents ai and aj in vertex v at time step t. This collision can be avoided if either agent ai or agent aj does not reside in v at timestep t. These two options correspond to new successor nodes of N - N1 and N2 that inherit the set of conflicts from N as follows: N1:con icts = N:con icts [ f(ai; v; t)g and N2:con icts = N:con icts [ f(aj ; v; t)g. N1:paths and N1:paths inherit paths from N:paths except those for agents ai and aj respectively. Paths for ai and aj are recalculated with respect to extended sets of conflicts N1:con icts and N2:con icts respectively and new costs for both agents N1: and N2: are determined. After this, N1 and N2 are inserted into the priority queue OPEN.

The pseudo-code of CBS is listed as Algorithm 1. One of crucial steps occurs at line 16 where a new path for colliding agents ai and aj is constructed with respect to the extended set of conflicts. N:paths(a) refers to path of agent a. The major alternative to CBS is represented by compilation of MAPF to propositional satisfiability (SAT) [ 29,26 ]. The idea follows SAT-based planning [ 10 ] where the existence of a plan for a fixed number time steps is modeled as SAT. We similarly construct propositional formula F ( ) such that it is satisfiable if and only if a solution of a given MAPF of sum-of-costs exists. Moreover, the approach is constructive; that is, F ( ) exactly reflects the MAPF instance and if satisfiable, solution of MAPF can be reconstructed from satisfying assignment of the formula. We say F ( ) to be a complete propositional model of MAPF.

Definition 3. (complete propositional model). Propositional formula F ( ) is a com

plete propositional model of MAPF if the following condition holds: F ( ) is satisfiable ,

has a solution of sum-of-costs .

Being able to construct such formula F one can obtain optimal MAPF solution by checking satisfiability of F ( 0), F ( 0 + 1), F ( 0 + 2),... until the first satisfiable F ( ) is met ( 0 is the lower bound for the sum-of-costs calculated as the sum of lengths of shortest paths). This is possible due to monotonicity of MAPF solvability with respect to increasing values of common cumulative objectives. Details of F are given in [ 29 ].

The advantage of the SAT-based approach is that state-of-the-art SAT solvers can be used for determining satisfiability of F ( ) [ 3 ]. 4

Combining SMT and CBS

A natural relaxation from the complete propositional model is an incomplete propositional model where instead of the equivalence between solving MAPF and the formula we require an implication only.

Definition 4. (incomplete propositional model). Propositional formula H( ) is an

incomplete propositional model of MAPF if the following condition holds: H( ) is satisfiable (

has a solution of sum-of-costs .

A close look at CBS reveals that it operates similarly as problem solving in satisfiability modulo theories (SMT) [ 5 ]. SMT divides satisfiability problem in some complex theory T into an abstract propositional part that keeps the Boolean structure of the decision problem and a simplified decision procedure DECIDET that decides fragment of T restricted on conjunctive formulae. A general T -formula is transformed to a propositional skeleton by replacing atoms with propositional variables. The SAT solver then decides what variables should be assigned TRUE in order to satisfy the skeleton - these variables tells what atoms hold in . DECIDET then checks if the conjunction of atoms assigned TRUE is valid with respect to axioms of T . If so then satisfying assignment is returned. Otherwise a conflict from DECIDET (often called a lemma) is reported back and the skeleton is extended with a constraint forbidding the conflict.

The above observation led us to the idea to rephrase CBS in terms of SMT. The abstract propositional part working with the skeleton will be taken from MDD-SAT provided that only constraints ensuring that assignments form valid paths interconnecting starting positions with goals will be preserved. Other constraints for collision avoidance will be omitted initially. This will result in an incomplete propositional model.

The paths validation procedure will act as DECIDET and will report back the set of conflicts found in the current solution. Hence axioms of T will be represented by the movement rules of MAPF. We call the resulting algorithm SMT-CBS and it is shown in pseudo-code as Algorithm 2.

Algorithm 2: SMT-CBS algorithm for MAPF solving = (G = (V; E); A; 0; +))

; fpath (ai) a shortest path from 0(ai) to +(ai)ji = 1; 2; :::; kg 1 SMT-CBS ( 2 con icts 3 paths 4 5 6 7 8

Pik=1 (paths(ai)) while TRUE do (paths; con icts) SMT-CBS-Fixed(con icts; ; ) if paths 6= UNSAT then

return paths 9

The algorithm is divided into two procedures: SMT-CBS representing the main loop and SMT-CBS-Fixed solving the input MAPF for fixed cost . The major difference from the standard CBS is that there is no branching at the high-level. The high-level SMT-CBS roughly correspond to the main loop of MDD-SAT. The set of conflicts is iteratively collected during the entire execution of the algorithm. Procedure encode from MDD-SAT is replaced with encode-Basic that produces encoding that ignores specific movement rules (collisions between agents) but in contrast to encode it encodes collected conflicts into H( ).

The conflict resolution in the standard CBS implemented as high-level branching is here represented by refinement of H( ) with disjunction (line 20). The presented SMT-CBS can eventually build the same formula as MDD-SAT but this is done lazily in SMT-CBS. 5

From SMT-CBS to DPLL(MAPF) and Beyond

Although the performed experimental evaluation presented in [ 28 ] shows that SMTCBS significantly outperforms both the CBS algorithm and MDD-SAT we conjecture that there is still room for improving the idea behind SMT-CBS. SMT-CBS as shown in Algorithm 2 implements very basic variant of SMT-based problem solving. More advanced SMT-based algorithms for deciding formulae in first order theories integrates the SAT solver and DECIDET more tightly. DECIDET is invoked not only for the fully assigned formulae (line 13 produces a full assignment) but also for partial assignments. Such algorithms are usually denoted DPLL(T) [ 16 ].

Whenever the SAT-solving search loop in DPLL (or CDCL) assigns new propositional variable, DECIDET is invoked to check if the extended partial assignment is consistent with respect to T (or MAPF in our case). If so the main loop continues with assigning the next variable. Otherwise DECIDET return a lemma forbidding the current assignment, translated in MAPF terms this corresponds to a case when DECIDEMAPF discovers a conflict and returns the conflict elimination constraint.

DECIDET (DECIDEMAPF ) can do much more in the consistent case. The procedure can derive new assignments that is to perform a form of MAPF constraint propagation. Such propagation could work in tandem with the standard unit propagation [ 7 ] integrated in the CDCL-based SAT solvers. Moreover DPLL(MAPF) algorithm can be further parametrized with variable and value selection heuristics that can take into account axioms of the MAPF theory.

5.1 Implications for MAPF with Continuous Time and Geometric Agents

Recently generalizations of MAPF considering continuous time and geometric agents have appeared [ 1 ]. The continuous variant denoted MAPFR assigns each vertex of the underlying graph from the standard MAPF coordinates in the Euclidean space. Agents are geometric objects such as circles, spheres, polygons etc. and can move along straight lines connecting vertices of the underlying graph (agents cannot move outside these predefined lines). For simplicity agents are assumed to have constant speeds but the algorithmic concepts generalize for non-constant models too.

Collisions between agents are defined as any overlap between their bodies. The task is to find a collision free temporal plan. An adaptation of CBS algorithm denoted CBSR for the continuous variant has been proposed [ 1 ]. We rephrased CBSR in terms of SMT similarly as it has been done with CBS. The resulting algorithm SMT-CBSR [ 27 ] differs from SMT-CBS mostly in the aspect of decision variable generation. In case of the standard MAPF, decision variables can be determined statically in advance but this is not applicable in the continuous version since the continuity has potential to spawn infinitely many decisions. Decision variables need to be generated dynamically in response to discoveries of new conflicts in MAPFR.

Naturally the future step in the development of SMT-CBSR is DPLL(MAPFR) where also partial assignments will be checked for consistency. 6

Discussion and Conclusion

We recalled the new MAPF solving method called SMT-CBS that combines searchbased CBS and SAT-based MDD-SAT through concepts from satisfiability modulo theories (SMT). Although SMT-CBS represent state-of-the-art in optimal MAPF solving as shown in [ 28 ] we identified certain deficiencies of the algorithm. Namely the fact that it checks for consistency with respect to MAPF rules only fully assigned propositional encodings. We therefore theoretically suggest DPLL(MAPF), a new algorithm that will also check for consistency partial assignments. We further suggest future work in which DPLL(MAPF) will be generalized for MAPF with continuous time and geometric agents, an analogous next step beyond the existing SMT-CBSR algorithm [ 27 ].

Acknowledgements

This research has been supported by GACˇ R - the Czech Science Foundation, grant registration number 19-17966S.

References

1. Andreychuk , A. , Yakovlev , K. , Atzmon , D. , Stern , R. : Multi-agent pathfinding (MAPF) with continuous time . CoRR abs/ 1901 .05506 ( 2019 ), http://arxiv.org/abs/ 1901 .05506

2. Audemard , G. , Lagniez , J. , Simon , L. : Improving glucose for incremental SAT solving with assumptions: Application to MUS extraction . In: SAT . pp. 309 - 317 ( 2013 )

3. Audemard , G. , Simon , L. : Predicting learnt clauses quality in modern SAT solvers . In: IJCAI . pp. 399 - 404 ( 2009 )

4. Biere , A. , Biere , A. , Heule , M., van Maaren, H. , Walsh , T. : Handbook of Satisfiability: Volume 185 Frontiers in Artificial Intelligence and Applications . IOS Press ( 2009 )

5. Bofill , M. , Palah´ı, M. , Suy , J. , Villaret , M.: Solving constraint satisfaction problems with SAT modulo theories . Constraints 17 ( 3 ), 273 - 303 ( 2012 )

6. Davis , M. , Logemann , G. , Loveland , D.W.: A machine program for theorem-proving . Commun. ACM 5 ( 7 ), 394 - 397 ( 1962 ). https://doi.org/10.1145/368273.368557, https://doi.org/ 10.1145/368273.368557

7. Dowling , W.F. , Gallier , J.H. : Linear-time algorithms for testing the satisfiability of propositional horn formulae . J. Log. Program . 1 ( 3 ), 267 - 284 ( 1984 ). https://doi.org/10.1016/ 0743 - 1066 ( 84 ) 90014 - 1 , https://doi.org/10.1016/ 0743 - 1066 ( 84 ) 90014 - 1

8. Dresner , K. , Stone , P.: A multiagent approach to autonomous intersection management . JAIR 31 , 591 - 656 ( 2008 )

9. Ho¨nig, W., Kumar , T.K.S. , Cohen , L. , Ma , H., Xu , H. , Ayanian , N. , Koenig , S. : Summary: Multi-agent path finding with kinematic constraints . In: Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence , IJCAI 2017 . pp. 4869 - 4873 ( 2017 )

10. Kautz , H.A. , Selman , B. : Unifying sat-based and graph-based planning . In: Proceedings of the Sixteenth International Joint Conference on Artificial Intelligence , IJCAI 1999 . pp. 318 - 325 ( 1999 )

11. Kornhauser , D. , Miller , G.L. , Spirakis , P.G. : Coordinating pebble motion on graphs, the diameter of permutation groups, and applications . In: FOCS, 1984 . pp. 241 - 250 ( 1984 )

12. Li , J. , Surynek , P. , Felner , A. , Ma , H., Koenig , S.: Multi-agent path finding for large agents . In: AAAI . AAAI Press ( 2019 )

13. Luna , R. , Bekris , K.E. : Push and swap: Fast cooperative path-finding with completeness guarantees . In: IJCAI . pp. 294 - 300 ( 2011 )

14. Ma , H., Koenig , S. , Ayanian , N. , Cohen , L. , Ho¨nig, W., Kumar , T.K.S. , Uras , T. , Xu , H. , Tovey , C.A. , Sharon , G. : Overview: Generalizations of multi-agent path finding to real-world scenarios . CoRR abs/1702 .05515 ( 2017 ), http://arxiv.org/abs/1702.05515

15. Ma , H., Wagner , G. , Felner , A. , Li , J. , Kumar , T.K.S. , Koenig , S.: Multi-agent path finding with deadlines . In: Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI 2018, July 13-19 , 2018 , Stockholm, Sweden. pp. 417 - 423 ( 2018 )

16. Nieuwenhuis , R. , Oliveras , A. , Tinelli , C. : Solving SAT and SAT modulo theories: From an abstract davis-putnam-logemann-loveland procedure to dpll(T) . J. ACM 53 ( 6 ), 937 - 977 ( 2006 )

17. Ratner , D. , Warmuth , M.K. : Finding a shortest solution for the N x N extension of the 15- puzzle is intractable . In: AAAI . pp. 168 - 172 ( 1986 )

18. Ryan , M.R.K. : Exploiting subgraph structure in multi-robot path planning . J. Artif. Intell. Res. (JAIR) 31 , 497 - 542 ( 2008 )

19. Sharon , G. , Stern , R. , Felner , A. , Sturtevant , N.: Conflict-based search for optimal multiagent pathfinding . Artif. Intell . 219 , 40 - 66 ( 2015 )

20. Sharon , G. , Stern , R. , Goldenberg , M. , Felner , A. : The increasing cost tree search for optimal multi-agent pathfinding . Artif. Intell . 195 , 470 - 495 ( 2013 )

21. Silva , J.P.M. , Sakallah , K.A. : GRASP: A search algorithm for propositional satisfiability . IEEE Trans. Computers 48 ( 5 ), 506 - 521 ( 1999 ). https://doi.org/10.1109/12.769433, https: //doi.org/10.1109/12.769433

22. Silver , D. : Cooperative pathfinding . In: AIIDE . pp. 117 - 122 ( 2005 )

23. Standley , T. : Finding optimal solutions to cooperative pathfinding problems . In: AAAI. pp. 173 - 178 ( 2010 )

24. Surynek , P.: A novel approach to path planning for multiple robots in bi-connected graphs . In: ICRA 2009 . pp. 3613 - 3619 ( 2009 )

25. Surynek , P.: An optimization variant of multi-robot path planning is intractable . In: AAAI 2010 . AAAI Press ( 2010 )

26. Surynek , P. : Time-expanded graph-based propositional encodings for makespan-optimal solving of cooperative path finding problems . Ann. Math. Artif. Intell. 81 ( 3-4 ), 329 - 375 ( 2017 )

27. Surynek , P.: Multi-agent path finding with continuous time viewed through satisfiability modulo theories (SMT) . CoRR abs/ 1903 .09820 ( 2019 ), http://arxiv.org/abs/ 1903 .09820

28. Surynek , P. : Unifying search-based and compilation-based approaches to multi-agent path finding through satisfiability modulo theories . In: Proceedings of the 28th International Joint Conference on Artificial Intelligence , IJCAI 2019 . in press ( 2019 )

29. Surynek , P. , Felner , A. , Stern , R. , Boyarski , E.: Efficient SAT approach to multi-agent path finding under the sum of costs objective . In: ECAI . pp. 810 - 818 ( 2016 )

30. Wang , K. , Botea , A. : MAPP: a scalable multi-agent path planning algorithm with tractability and completeness guarantees . JAIR 42 , 55 - 90 ( 2011 )

31. de Wilde , B., ter Mors , A. , Witteveen , C. : Push and rotate: a complete multi-agent pathfinding algorithm . JAIR 51 , 443 - 492 ( 2014 )

32. Wilson, R.M.: Graph puzzles, homotopy, and the alternating group . Journal of Combinatorial Theory, Series B 16 ( 1 ), 86 - 96 ( 1974 )