=Paper=
{{Paper
|id=Vol-2495/paper9
|storemode=property
|title=On the Tour Towards DPLL(MAPF) and Beyond
|pdfUrl=https://ceur-ws.org/Vol-2495/paper9.pdf
|volume=Vol-2495
|authors=Pavel Surynek
|dblpUrl=https://dblp.org/rec/conf/aiia/Surynek19
}}
==On the Tour Towards DPLL(MAPF) and Beyond==
On the Tour Towards DPLL(MAPF) and Beyond Pavel Surynek1[0000−0001−7200−0542] Faculty of Information Technology Czech Technical University in Prague Thákurova 9, 160 00 Praha 6, Czech Republic pavel.surynek@fit.cvut.cz Abstract. We discuss milestones on the tour towards DPLL(MAPF), a multi- agent path finding (MAPF) solver fully integrated with the Davis–Putnam-Lo- gemann–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 sum- of-costs or the makespan based on the reduction of MAPF to propositional sat- isfiability (SAT) have appeared. The most successful methods rely on building the propositional encoding for the given MAPF instance lazily by a process in- spired 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 ge- ometric agents, are also discussed. Keywords: multi agent path finding (MAPF), propositional satisfiability (SAT), Davis–Putnam-Logemann–Loveland (DPLL), satisfiability modulo theories(SMT) 1 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 = {a1 , a2 , ..., ak } 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). On the Tour Towards DPLL(MAPF) and Beyond 75 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 algo- rithm 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 low- level 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 re- solve the conflict. SMT-CBS hence does not branch at the high-level but instead incre- mentally 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 proposi- tional 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 ob- tain 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 supe- rior 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. Sub- sequently, the decision procedure for the conjunctive fragment checks if the suggested 76 Pavel Surynek 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 (Davis- Putnam-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 = {a1 , a2 , ..., ak } such that |A| ≤ |V |. 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 α0 a2 E A α1 E A α2 = α+ E C D C D C D a1 a2 a2 a3 B a3 F B a3 F B a1 F Fig. 1: A MAPF instance with three agents a1 , a2 , and a3 . A two-step solution is shown too. Definition 1. Valid movement in MAPF. Configuration α0 results from α if and only if the following conditions hold: (i) α(a) = α0 (a) or {α(a), α0 (a)} ∈ E for all a ∈ A (agents wait or move along edges); (ii) for all a ∈ A it holds α(a) 6= α0 (a) ⇒ ¬(∃b ∈ A)(α(b) = α0 (a) ∧ α0 (b) = α(a)) (no two agents crosses an edge in opposite directions); (iii) and for all a, a0 ∈ A it holds that a 6= a0 ⇒ α0 (a) 6= α0 (a0 ) (no two agents share a vertex in the next configuration). On the Tour Towards DPLL(MAPF) and Beyond 77 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]; pre- cisely the worst case time complexity of most practical algorithms for finding feasible 3 solutions is O(|V | ) [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 sum- of-costs objective [8,23,20] we need more notation as follows: Definition 2. Sum-of-costs objective is the summation, over all k agents,Pkof the num- ber of time steps required to reach the goal vertex. Denoted ξ, where ξ = i=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 compilation- based 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 {v ∈ V |(ai , v, t) ∈ N.constraints} whenever working at time step t. For details see [19]. CBS stores nodes of CT into priority queue O PEN sorted according to the ascending costs of solutions. At each step CBS takes node N with the lowest cost from O PEN 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. 78 Pavel Surynek Algorithm 1: CBS algorithm for MAPF solving 1 CBS (G = (V, E), A, α0 , α+ ) 2 R.constraints ← ∅ 3 R.paths ← {shortest path from α0 (ai ) to α+ (ai )|i = 1, 2, ..., k} R.ξ ← ki=1 ξ(N.paths(ai )) P 4 5 insert R into O PEN 6 while O PEN 6= ∅ do 7 N ← min(O PEN) 8 remove-Min(O PEN) 9 collisions ← validate(N.paths) 10 if collisions = ∅ then 11 return N.paths 12 let (ai , aj , v, t) ∈ collisions 13 for each a ∈ {ai , aj } do 14 N 0 .constraints ← N.constraints ∪ {(a, v, t)} 15 N 0 .paths ← N.paths 16 update(a, N 0 .paths, N 0 .constraints) N 0 .ξ ← ki=1 ξ(N 0 .paths(ai )) P 17 18 insert N 0 into O PEN 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 .conflicts = N.conflicts ∪ {(ai , v, t)} and N2 .conflicts = N.conflicts ∪ {(aj , v, t)}. 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 .conflicts and N2 .conflicts respectively and new costs for both agents N1 .ξ and N2 .ξ are determined. After this, N1 and N2 are inserted into the priority queue O PEN. 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. 3.2 Compilation to Propositional Satisfiability 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 ex- istence of a plan for a fixed number time steps is modeled as SAT. We similarly con- struct 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 On the Tour Towards DPLL(MAPF) and Beyond 79 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 proposi- tional 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 satisfia- bility 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 de- cision 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 ab- stract propositional part working with the skeleton will be taken from MDD-SAT pro- vided 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. 80 Pavel Surynek Algorithm 2: SMT-CBS algorithm for MAPF solving 1 SMT-CBS (Σ = (G = (V, E), A, α0 , α+ )) 2 conflicts ← ∅ 3 paths ← {path ∗ (ai ) a shortest path from α0 (ai ) to α+ (ai )|i = 1, 2, ..., k} ξ ← ki=1 ξ(paths(ai )) P 4 5 while TRUE do 6 (paths, conflicts) ← SMT-CBS-Fixed(conflicts, ξ, Σ) 7 if paths 6= UNSAT then 8 return paths 9 ξ ←ξ+1 10 SMT-CBS-Fixed(conf licts, ξ, Σ) 11 H(ξ) ← encode-Basic(conflicts, ξ, Σ) 12 while TRUE do 13 assignment ← consult-SAT-Solver(H(ξ)) 14 if assignment 6= UNSAT then 15 paths ← extract-Solution(assignment) 16 collisions ← validate(paths) 17 if collisions = ∅ then 18 return (paths, conflicts) 19 for each (ai , aj , v, t) ∈ collisions do 20 H(ξ) ← H(ξ) ∪ {¬Xvt (ai ) ∨ ¬Xvt (aj )} 21 conflicts ← conflicts ∪ {[(ai , v, t), (aj , v, t)]} 22 return (UNSAT,conflicts) 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 it- eratively 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 col- lected 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 SMT- CBS 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 On the Tour Towards DPLL(MAPF) and Beyond 81 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 assign- ments. Such algorithms are usually denoted DPLL(T) [16]. Whenever the SAT-solving search loop in DPLL (or CDCL) assigns new propo- sitional 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 contin- ues with assigning the next variable. Otherwise DECIDET return a lemma forbid- ding 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 proce- dure can derive new assignments that is to perform a form of MAPF constraint prop- agation. 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 search- based CBS and SAT-based MDD-SAT through concepts from satisfiability modulo the- ories (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 82 Pavel Surynek that it checks for consistency with respect to MAPF rules only fully assigned propo- sitional 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 geo- metric agents, an analogous next step beyond the existing SMT-CBSR algorithm [27]. Acknowledgements This research has been supported by GAČ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: Vol- ume 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. Com- mun. 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 proposi- tional 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. Hö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 di- ameter 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., Hö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 On the Tour Towards DPLL(MAPF) and Beyond 83 15. Ma, H., Wagner, G., Felner, A., Li, J., Kumar, T.K.S., Koenig, S.: Multi-agent path find- ing 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 multi- agent 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)