Multi-Agent Path Finding with Capacity Constraints

TL;DR

This paper extends multi-agent path finding (MAPF) to allow multiple agents per vertex by modeling capacity constraints in SAT-based formulations, evaluating their performance and proposing new models.

Contribution

It introduces SAT-based models for MAPF with capacity constraints, extending existing formulations to handle multiple agents per vertex.

Findings

Extended SAT models for MAPF with capacity constraints.

Performance evaluation of new SAT-based formulations.

Comparison of eager and lazy modeling approaches.

Abstract

In multi-agent path finding (MAPF) the task is to navigate agents from their starting positions to given individual goals. The problem takes place in an undirected graph whose vertices represent positions and edges define the topology. Agents can move to neighbor vertices across edges. In the standard MAPF, space occupation by agents is modeled by a capacity constraint that permits at most one agent per vertex. We suggest an extension of MAPF in this paper that permits more than one agent per vertex. Propositional satisfiability (SAT) models for these extensions of MAPF are studied. We focus on modeling capacity constraints in SAT-based formulations of MAPF and evaluation of performance of these models. We extend two existing SAT-based formulations with vertex capacity constraints: MDD-SAT and SMT-CBS where the former is an approach that builds the model in an eager way while the latter relies on lazy construction of the model.

Equations

$$\sum _{a_i\in A|v^t\in V_i}{\mathcal{X}}_v^t(a_i)\le 1$$

$${\mathcal{X}}_u^t(a_i)\Rightarrow \underset{(u^t,v^{t+1})\in E_i}{\bigvee }{\mathcal{E}}_{u,v}^t(a_i),$$

$$\sum _{v^{t+1}|(u^t,v^{t+1})\in E_i}{\mathcal{E}}_{u,v}^t(a_i)\le 1$$

$${\mathcal{E}}_{u,v}^t(a_i)\Rightarrow \underset{a_j\in A|a_j\ne a_i\wedge v^t\in V_j}{\bigwedge }\neg {\mathcal{X}}_v^t(a_j)$$

$${\mathcal{E}}_{u,v}^t(a_i)\Rightarrow {\mathcal{X}}_v^t(a_i)\wedge {\mathcal{X}}_v^{t+1}(a_i)$$

$$\sum _{a_i\in A|v^t\in V_i}{\mathcal{X}}_v^t(a_i)\le c(v)$$

$${\le }_{c(v)}\{{\mathcal{X}}_v^t(a_i)|a_i\in A\wedge v^t\in V_i\}$$

Full text

1 Introduction

In multi-agent path finding (MAPF) [9, 18, 19, 21, 24, 28, 33] 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=\{a_{1},a_{2},...,a_{k}\}$ 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 $\alpha_{0}:A\rightarrow V$ and similarly the goal configuration as $\alpha_{+}:A\rightarrow V$. The task of navigating agents can be expressed as a task of transforming the initial configuration of agents $\alpha_{0}:A\rightarrow V$ into the goal configuration $\alpha_{+}:A\rightarrow 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 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 [29]. We usually denote the configuration of agents at discrete time step $t$ as $\alpha_{t}:A\rightarrow V$. Non-conflicting movements transform configuration $\alpha_{t}$ instantaneously into next configuration $\alpha_{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 [8], large agents [11], or deadlines [14] - see [13] for more variants.

Particularly in this work we are dealing with an extension of MAPF that generalizes the constraint of having at most one agent per vertex. There are many situations where we need to model nodes that could hold more than agent at a time. Such situations include various graph-based evacuation models where for example nodes correspond to rooms in evacuated buildings [10] which naturally can hold more than one agent. Various spatial projections could also lead to having multiple agents per vertex such as upper projection of agents representing aerial drones where a single node corresponds to $x$,$y$-coordinate that could hold multiple agents at different $z$-coordinates [12]. Generally the need to consider nodes capable of containing multiple agents appears in modeling of multi-agent motion planning task at higher levels of granularity.

1.1 Contributions

The contribution of this paper consists in showing how to generalize existing propositional satisfiability (SAT) [4] models of MAPF for finding optimal plans with general capacity constraints that bound the number of agents in vertices. Two existing SAT-based models are generalized: MDD-SAT [32] that builds the propositional model in an eager way and SMT-CBS [30, 31] that builds the model in a lazy way inspired by satisfiability modulo theories (SMT) [16].

The eager style of building the propositional model means that all constraints are posted into the model in advance. Such model is complete that is, it is solvable (satisfiable) if and only if the instance being modeled is solvable. In contrast to this, the lazy style does not add all constraints at once and works with incomplete models. The incomplete model preserve only one-sided implication w.r.t. solvability: if the instance being modeled is solvable then the incomplete model is solvable (satisfiable).

The SMT-CBS algorithm iteratively refines the incomplete model towards the complete one by eliminating conflicts. That is, a candidate solution is extracted from the satisfied incomplete model. The candidate is checked for conflicts - whether any of the MAPF rules is violated - for example if a collision between agents occurred. If there are no conflicts, we are finished as the candidate is a valid solution of the input MAPF instance. If a conflict is detected, then a constraint that eliminates this particular conflict is added to the incomplete model resulting in a new model and the process is repeated. That is, a new candidate solution is extracted from the new model etc. Eventually the process may end up with a complete model after eliminating all possible conflicts. However, we hope that the process finishes before constructing a complete model and we solve the instance with less effort.

In the presented generalization with capacity constraints we need to distinguish between the eager and lazy variant. The capacity constraint concerning given vertex $v$ bounding the number of agents that can simultaneously occupy $v$ by some integer constant say $2$ can be literally translated into the requirement that no $3$ distinct agents can occupy $v$ at the same time. Such a constraint can be directly posted in the eager variant: we either forbid all possible triples of agents in $v$ or post the corresponding cardinality constraint [3, 23].

The situation is different in the lazy variant. To preserve the nature of the lazy approach we cannot post the capacity bound entirely as conceptually at the low level as we are informed only about a particular MAPF rule violation, say for example agents $a_{1}$, $a_{5}$ and $a_{8}$ occurred simultaneously in $v$ which is forbidden in given MAPF. The information that there is a capacity constraint on $v$ bounding the number of agents in $v$ by $2$ may even not be accessible at the low level. Hence we can forbid simultaneous occurrence of only the given triple of agents, $a_{1}$, $a_{5}$ and $a_{8}$ in this case.

The paper is organized as follows. We first introduce the standard multi-agent path finding problem formally including commonly used objectives. Then we introduce two major existing SAT-based encodings. On top of this, we show how to extend these encodings with vertex capacities. Finally we evaluate extended models on standard benchmarks including open grids and large game maps.

2 Formal Definition of MAPF and Vertex Capacities

The Multi-agent path finding (MAPF) problem [24, 18] consists of an undirected graph $G=(V,E)$ and a set of agents $A=\{a_{1},a_{2},...,a_{k}\}$ such that $|A|\leq|V|$. Each agent is placed in a vertex so that at most one agent resides in each vertex. The placement of agents is denoted $\alpha:A\rightarrow V$. Next we are given initial configuration of agents $\alpha_{0}$ and goal configuration $\alpha_{+}$.

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 $a_{i}$, moving it from $\alpha_{0}(a_{i})$ to $\alpha_{+}(a_{i})$ such that agents do not conflict, i.e., do not occupy the same location at the same time nor cross the same edge in opposite directions simultaneously. The following definition formalizes the commonly used movement rule in MAPF.

Definition 1

Valid movement in MAPF. Configuration $\alpha^{\prime}$ results from $\alpha$ if and only if the following conditions hold:

1. (i)

$\alpha(a)=\alpha^{\prime}(a)$ or $\{\alpha(a),\alpha^{\prime}(a)\}\in E$ for all $a\in A$ (agents wait or move along edges); 2. (ii)

for all $a\in A$ it holds ${\alpha(a)\neq\alpha^{\prime}(a)}\Rightarrow{\neg(\exists b\in A)(\alpha(b)=\alpha^{\prime}(a)\wedge\alpha^{\prime}(b)=\alpha(a))}$ (no two agents crosses an edge in opposite directions); 3. (iii)

and for all $a,a^{\prime}\in A$ it holds that ${a\neq a^{\prime}}\Rightarrow{\alpha^{\prime}(a)\neq\alpha^{\prime}(a^{\prime})}$ (no two agents share a vertex in the next configuration).

Solving the MAPF instance is to find a sequence of configurations $[\alpha_{0},\alpha_{1},...,\alpha_{\mu}]$ such that $\alpha_{i+1}$ results using valid movements from $\alpha_{i}$ for $i=1,2,...,\mu-1$, and $\alpha_{\mu}=\alpha_{+}$.

A version of MAPF with vertex capacities generalizes the above definition by adding capacity function $c:V\rightarrow\mathbb{Z}_{+}$ that assigns each vertex a positive integer capacity. The interpretation is that a vertex $v$ can hold up to the specified number of agents $c(v)$ at any time-step.

The definition of the valid movement will change only in point (iii) where instead of permitting at most one agent per vertex we allow any number of agents not exceeding the capacity of the vertex:

Definition 2

Vertex capacities in MAPF.

1. (iii’)

for all $v\in V$ it holds that $|{a\>|\>\alpha^{\prime}(a)=v}|\leq c(v)$ (the number of agents in each vertex does not exceed the capacity in the next configuration).

Using generalized vertex capacities relaxes the problem in fact as illustrated in Figure 1. Intuitively, capacities greater than one induce additional parking place in the environment which we hypothetise to make the problem easier to solve.

2.1 Common Objectives in MAPF

We address here optimal MAPF solving hence we need to introduce objective functions more formally. In case of makespan [29] we just need to minimize $\mu$ in the aforementioned solution sequence. For introducing the sum-of-costs objective [7, 26, 21, 19] we need the following notation:

Definition 3

Sum-of-costs objective is the summation, over all agents, of the number of time steps required to reach the goal vertex. Denoted $\xi$, where $\xi=\sum_{i=1}^{k}{\xi(path(a_{i}))}$, where $\xi(path(a_{i}))$ is an individual path cost of agent $a_{i}$ connecting $\alpha_{0}(a_{i})$ calculated as the number of edge traversals and wait actions. 111The notation $path(a_{i})$ refers to path in the form of a sequence of vertices and edges connecting $\alpha_{0}(a_{i})$ and $\alpha_{+}(a_{i})$ while $\xi$ assigns the cost to a given path.

Observe that in the sum-of-costs we accumulate the cost of wait actions for agents not yet reaching their goal vertices. For the sake of brevity we focus here on the sum-of-costs, but we note that all new concepts can be introduced for different cumulative objectives like the makespan.222Dealing with objectives is out of scope of this paper. We refer the reader to [32] for more detailed discussion.

We note that finding a solution that is optimal (minimal) with respect to the sum-of-costs objective is NP-hard [17]. The same result holds for the variant with capacities as it is a straight generalization of the standard MAPF version.

3 Related Work

Let us now recall existing SAT-based optimal MAPF solvers. We here focus on aspects important for introducing capacities. We recall MDD-SAT the sum-of-costs optimal solver based on eager SAT encoding [32] and SMT-CBS [31], the most recent SAT-based, or more precisely SMT-based, algorithm using lazy encoding.

3.1 SAT-based Approach

The idea behind the SAT-based approach is to construct a propositional formula $\mathcal{F(\xi)}$ such that it is satisfiable if and only if a solution of a given MAPF of sum-of-costs $\xi$ exists [29]. Moreover, the approach is constructive; that is, $\mathcal{F(\xi)}$ exactly reflects the MAPF instance and if satisfiable, solution of MAPF can be reconstructed from satisfying assignment of the formula. We say $\mathcal{F(\xi)}$ to be a complete propositional model of MAPF.

Definition 4

(complete propositional model). Propositional formula $\mathcal{F(\xi)}$ is a complete propositional model of MAPF $\Sigma$ if the following condition holds:

$\mathcal{F(\xi)}$ is satisfiable $\Leftrightarrow$ $\Sigma$ has a solution of sum-of-costs $\xi$.

Being able to construct such formula $\mathcal{F}$ one can obtain optimal MAPF solution by checking satisfiability of $\mathcal{F}(0)$, $\mathcal{F}(1)$, $\mathcal{F}(2)$,… until the first satisfiable $\mathcal{F(\xi)}$ is met. This is possible due to monotonicity of MAPF solvability with respect to increasing values of common cumulative objectives like the sum-of-costs. In practice it is however impractical to start at 0; lower bound estimation is used instead - sum of lengths of shortest paths can be used in the case of sum-of-costs. The framework of SAT-based solving is shown in pseudo-code in Algorithm 1.

3.2 Details of the MDD-SAT Encoding

Construction of $\mathcal{F(\xi)}$ as used in the MDD-SAT solver relies on time expansion of underlying graph $G$. Having $\xi$, the basic variant of time expansion determines the maximum number of time steps $\mu$ (makespan) such that every possible solution of the given MAPF with the sum-of-costs less than or equal to $\xi$ fits within $\mu$ timesteps. Given $\xi$ we can calculate $\mu$ as $max_{i=1}^{k}\{\xi_{0}(a_{i})\}+\xi-\xi_{0}$ where $\xi_{0}(a_{1})$ is the length of the shortest path connecting $\alpha_{0}(a_{i})$ and $\alpha_{+}(a_{i})$; $\xi_{0}=\sum_{i=1}^{k}{\xi_{0}(a_{i})}$. The detailed justification of this equation is given in [32].

Time expansion itself makes copies of vertices $V$ for each timestep $t=0,1,2,...,\mu$. That is, we have vertices $v^{t}$ for each $v\in V$ and time step $t$. Edges from $G$ are converted to directed edges interconnecting timesteps in the time expansion. Directed edges $(u^{t},v^{t+1})$ are introduced for $t=1,2,...,\mu-1$ whenever there is $\{u,v\}\in E$. Wait actions are modeled by introducing edges $(u^{t},t^{t+1})$. A directed path in the time expansion corresponds to trajectory of an agent in time. Hence the modeling task now consists in construction of a formula in which satisfying assignments correspond to directed paths from $\alpha_{0}^{0}(a_{i})$ to $\alpha_{+}^{\mu}(a_{i})$ in the time expansion.

Assume that we have time expansion $TEG_{i}=(V_{i},E_{i})$ for agent $a_{i}$. Propositional variable $\mathcal{X}_{v}^{t}(a_{j})$ is introduced for every vertex $v^{t}$ in $V_{i}$. The semantics of $\mathcal{X}_{v}^{t}(a_{i})$ is that it is $\mathit{TRUE}$ if and only if agent $a_{i}$ resides in $v$ at time step $t$. Similarly we introduce $\mathcal{E}_{u},v^{t}(a_{i})$ for every directed edge $(u^{t},v^{t+1})$ in $E_{i}$. Analogously the meaning of $\mathcal{E}_{u,v}^{t}(a_{i})$ is that is $\mathit{TRUE}$ if and only if agent $a_{i}$ traverses edge $\{u,v\}$ between time steps $t$ and $t+1$.

Constraints are added so that truth assignment are restricted to those that correspond to valid solutions of a given MAPF. Added constraints together ensure that $\mathcal{F(\xi)}$ is a complete propositional model for given MAPF.

We here illustrate the model by showing few representative constraints. We omit here constraints that concern objective function. For the detailed list of constraints we again refer the reader to [32].

Collisions among agents are eliminated by the following constraint for every $v\in V$ and timestep $t$ expressed on top of $\mathcal{X}_{v}^{t}(a_{i})$ variables:

[TABLE]

There are various ways how to translate the constraint using propositional clauses. One efficient way is to introduce $\neg\mathcal{X}^{t}_{v}(a_{i})\vee\neg\mathcal{X}^{t}_{v}(a_{j})$ for all possible pairs of $a_{i}$ and $a_{j}$.

Next, there is a constraint stating that if agent $a_{i}$ appears in vertex $u$ at time step $t$ then it has to leave through exactly one edge $(u^{t},v^{t+1})$. This can be established by following constraints:

[TABLE]

[TABLE]

Similarly, the target vertex of any movement except wait action must be empty. This is ensured by the following constraint for every $(u^{t},v^{t+1})\in E_{i}$:

[TABLE]

Other constraints ensure that truth assignments to variables per individual agents form paths. That is if agent $a_{i}$ enters an edge it must leave the edge at the next time step.

[TABLE]

A common measure how to reduce the number of decision variables derived from the time expansion is the use of multi-value decision diagrams (MDDs) [21]. The basic observation that holds for MAPF is that an agent can reach vertices in the distance $d$ (distance of a vertex is measured as the length of the shortest path) from the current position of the agent no earlier than in the $d$-th time step. Analogical observation can be made with respect to the distance from the goal position.

Above observations can be utilized when making the time expansion of $G$. For a given agent, we do not need to consider all vertices at time step $t$ but only those that are reachable in $t$ timesteps from the initial position and that ensure that the goal can be reached in the remaining $\mu-t$ timesteps.

3.3 Resolving Conflicts Lazily in SMT-CBS

SMT-CBS is inspired by search-based algorithm CBS [22, 20] that 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. SMT-CBS follows the high-level framework of CBS but rephrases the process into propositional satisfiability in a similar way as done in formula satisfiability testing in satisfiability modulo theory paradigm [16, 15, 5].

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.\mathit{constraints}$ - a set of triples $(a_{i},v,t)$ forbidding occurrence of agent $a_{i}$ in vertex $v$ at time step $t$, a solution $N.paths$ - a set of $k$ paths for individual agents, and the total cost $N.\xi$ 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.\mathit{constraints}$. For a given agent $a_{i}$, this is a standard single source shortest path search from $\alpha_{0}(a_{i})$ to $\alpha_{+}(a_{i})$ that avoids a set of vertices $\{v\in V|(a_{i},v,t)\in N.\mathit{constraints}\}$ 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.\mathit{paths}$ represent paths that are valid with respect to MAPF movements rules - that is, $N.\mathit{paths}$ are checked for collisions. If there is no collision, the algorithms returns valid MAPF solution $N.\mathit{paths}$. Otherwise the search branches by creating a new pair of nodes in CT - successors of $N$. Assume that a collision occurred between agents $a_{i}$ and $a_{j}$ in vertex $v$ at time step $t$. This collision can be avoided if either agent $a_{i}$ or agent $a_{j}$ does not reside in $v$ at timestep $t$. These two options correspond to new successor nodes of $N$ - $N_{1}$ and $N_{2}$ that inherit the set of conflicts from $N$ as follows: $N_{1}.\mathit{conflicts}=N.\mathit{conflicts}\cup\{(a_{i},v,t)\}$ and $N_{2}.\mathit{conflicts}=N.\mathit{conflicts}\cup\{(a_{j},v,t)\}$. $N_{1}.\mathit{paths}$ and $N_{1}.\mathit{paths}$ inherit paths from $N.\mathit{paths}$ except those for agents $a_{i}$ and $a_{j}$ respectively. Paths for $a_{i}$ and $a_{j}$ are recalculated with respect to extended sets of conflicts $N_{1}.\mathit{conflicts}$ and $N_{2}.\mathit{conflicts}$ respectively and new costs for both agents $N_{1}.\xi$ and $N_{2}.\xi$ are determined. After this, $N_{1}$ and $N_{2}$ are inserted into the priority queue Open.

SMT-CBS compresses CT into a single branch in which the propositional model taken from MDD-SAT is iteratively refined. The high-level branching from CBS is deferred to the low level of SAT solving. In the MDD-SAT encoding collision avoidance constraints are omitted initially, only constraints ensuring that assignments form valid paths interconnecting starting positions with goals are be preserved. This will result in an incomplete propositional model denoted $\mathcal{H}(\xi)$. The important component of SMT-CBS is a paths validation procedure that reports back the set of conflicts found in the current solution that are used for making model refinements. SMT-CBS is shown in pseudo-code as Algorithm 2.

The algorithm is divided into two procedures: SMT-CBS representing the main loop and SMT-CBS-Fixed solving the input MAPF for fixed cost $\xi$. 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 $\mathcal{H}(\xi)$.

The conflict resolution in the standard CBS implemented as high-level branching is here represented by refinement of $\mathcal{H}(\xi)$ 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.

4 Handling Capacity Constraints in MAPF

To adapt the SAT-based approach for MAPF with capacities we need minor modifications only in both MDD-SAT and SMT-CBS. However in each algorithm the integration of capacity constraints in profoundly different. While in MDD-SAT we integrate capacity constraints eagerly in the line with the original design of the algorithm (that is, the constraint in introduced as a whole), in SMT-CBS we integrate capacity constraint lazily which means part by part as new conflicts appear.

4.1 Details of the Encoding with Capacities

We need only a small modification of the MDD-SAT encoding to handle vertex capacities. We need to replace constraint 1 with the following constraint that is again posted for every vertex $v$ and time step $t$:

[TABLE]

Unlike in the standard MAPF we need here a more sophisticated translation of the constraint to propositional clauses. Using the approach of forbidding individual $c(v)+1$-tuples can be highly inefficient especially in cases when $c(v)$ is large. Therefore we use cardinality constraints encodings commonly used in SAT [3, 25, 23]. Generally the cardinality constraint over set of propositional variables $\{\mathcal{X}_{1},\mathcal{X}_{2},...,\mathcal{X}_{n}\}$ permits at most a specified number of variables from the set to be $\mathit{TRUE}$, denoted ${\leq}_{k}\{\mathcal{X}_{1},\mathcal{X}_{2},...,\mathcal{X}_{n}\}$ means that at most k variables from the set can be $\mathit{TRUE}$.

In our case of MAPF with capacities we need to introduce following cardinality constraints for every vertex $v$ and time step $t$. The practical implementation of cardinaliy constraints is done through encoding adder circuits inside the formula [23].

[TABLE]

4.2 Capacities in SMT-CBS

Capacities in SMT-CBS are resolved lazily as well. That is, the capacity constraint is not posted entirely as a cardinality constraint but instead individual sets of agents that violate the capacity are forbidden one by one as they appear. That is for example if a generalized conflict occurs with agents $a_{i_{1}}$, $a_{i_{2}}$, …, $a_{i_{m}}$ in vertex $v$ (in other words if $m>c(v)$) we post a conflict elimination clause concerning the colliding set of agents: $\neg\mathcal{X}_{v}^{t}(a_{i_{1}})\vee\neg\mathcal{X}_{v}^{t}(a_{i_{2}})\vee...\vee\neg\mathcal{X}_{v}^{t}(a_{i_{m}})$.

Hence in the SMT-CBS algorithm we modify only lines 20 and 21 that handle generalized vertex conflicts. Also we need to modify the validate procedure called at line 15 to reflect generalized vertex capacities.

5 Experimental Evaluation

To evaluate the performance of capacity handling in context of SAT-based algorithms we performed an extensive evaluation on both standard synthetic benchmarks [6, 21] and large maps from games [27].

5.1 Setup of Experiments and Benchmarks

We took the existing implementations of MDD-SAT and SMT-CBS written in C++. Both implementations are built on top of the Glucose 4 SAT solver [1, 2]. In the implementations we modified the capacity constraint from the original at-most-one to generalized variants as mentioned above. All experiments were run on a Ryzen 7 CPU 3.0 Ghz under Kubuntu linux 16 with 16GB RAM. The timeout in all experiments was set to 500 seconds. Presented are only results finished within this time limit.

The second part of experimental evaluation took place on large 4-connected maps taken from Dragon Age [19, 27]. We took three structurally different maps focusing on various aspects such as narrow corridors, large almost isolated rooms, or topologically complex open space. In contrast to small instances, these were only sparsely populated with agents. Initial and goal configuration were generated at random again. Up to 80 agents were used in these instances and uniform capacities of 1, 2, and 3. On large maps we measured the runtime.

5.2 Results on Small Grids

Results obtained for small open grids are presented in Figures 2 and 3. We can see that in comparison with the standard MAPF capacities bring significant reduction of difficulty of instances. This difference can be seen in both MDD-SAT and SMT-CBS. The starkest performance difference is between $c=1$ and $c=2$. The least performance difference is between $c=3$ and $c=4$. The similar picture can be seen in for the number of clauses.

5.3 Results on Large Maps

Results for large game maps are shown in Figures 4 and 5. A different picture can be seen here. Adding capacities does not cause any significant simplification except the brc202d map which consists of narrow corridors. The interpretation is that adding extra parking place through capacities may lead to simplification only when it is not available normally. Otherwise generalized capacity constraints lead to harder instances.

6 Discussion and Conclusion

We introduced multi-agent path finding problem with vertex capacity constraints. We modified two existing state-of-the-art SAT-based optimal MAPF solvers to reflect vertex capacities, the MDD-SAT solver using the eager encoding and the SMT-CBS solver using the lazy encoding.

In both solvers we observed that adding an extra room by increasing the capacity of vertices dramatically reduces the difficulty of instances. However adding further capacity does has less significant effect. In large maps using higher capacities even lead to performance degradation which we attribute to more complex constraints.

In the future work we would like to apply the MAPF formulation with capacities in the real-life multi-robot problem.