=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== https://ceur-ws.org/Vol-2495/paper9.pdf
                           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)