{'fraction_non_alphanumeric': 0.03266227004512322, 'fraction_numerical': 0.008712252690038181, 'mean_word_length': 4.527820414428242, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Sparsification for Fast Optimal Multi-Robot Path Planning in Lazy Compilation Schemes

Path planning for multiple robots (MRPP) represents a task of finding non-colliding paths for robots through which they can navigate from their initial positions to specified goal positions. The problem is usually modeled using undirected graphs where robots move between vertices across edges. Contemporary optimal solving algorithms include dedicated search-based methods, that solve the problem directly, and compilation-based algorithms that reduce MRPP to a different formalism for which an efficient solver exists, such as constraint programming (CP), mixed integer programming (MIP), or Boolean satisfiability (SAT). In this paper, we enhance existing SAT-based algorithm for MRPP via spartification of the set of candidate paths for each robot from which target Boolean encoding is derived. Suggested sparsification of the set of paths led to smaller target Boolean formulae that can be constructed and solved faster while optimality guarantees of the approach have been kept.


Introduction and Motivation
Multi-robot path planning in graphs (MRPP) represents fundamental problem in combinatorial motion planning in robotics [21,24,27,28,36]. The task is to navigate each robot in the set of robots R = {r 1 , r 2 , ..., r k } from its initial position to a specified goal position. The environment is modeled as an undirected graph G = (V, E) where vertices represent positions and robots move across edges between vertices. Two requirements make the problem challenging: (1) the robots must not collide with each other, that is they never can share a vertex or traverse an edge in opposite directions and (2) some objective such as total number of actions must be optimized.
Many practical problems from robotics can be interpreted as MRPP. Examples include discrete multi-robot navigation and coordination [20], robot rearrangement in automated warehouses [6], ship collision avoidance [14], or formation maintenance and maneuvering of aerial vehicles [38].
We address the MRPP problem from the perspective of compilation-based techniques. Compilation is one of the most important techniques used across many computing fields ranging from theory to practice. In the context of problem solving in robotics, the compilation approach reduces an input problem instance from its source formalism to a different, usually well established, target formalism for which an efficient solver exists. After obtaining a solution by the solver, it is interpreted back to the input formalism, which altogether constitutes a reduction-solving-interpretation loop.
Target formalisms are often combinatorial optimization frameworks like constraint programming / optimization (CP) [10], mixed integer programming (MIP) [13,23], Boolean satisfiability (SAT) [7], satisfiability modulo theories (SMT) [5], or answer set programming (ASP) [19]. Employing the advancements in solvers for the target formalisms, often accumulated for decades, in solving the input problem represents the key benefit of problem solving via compilation. However, the way how the input instance is reduced to the target formalism and presented to the solver has a great impact on the efficiency of the whole solving process.
Currently compilation-based optimal solvers for MRPP represent a major alternative to search-based solvers, that model and solve the problem directly, and often provide more modular and versatile architecture than search-based solvers while providing competitive performance. Contemporary compilationbased solvers for MRPP include those based on CP [12], MIP [16], SAT/SMT [32,34], as well as ASP-based solvers [11].
We focus in this paper on SMT-based solvers for MRPP. Our contribution consists in a new technique for encoding the MRPP instance as Boolean formulae via sparsification of a set of candidate paths for each robot. The novel encoding is integrated into a modified SMT-CBS [32], an optimal MRPP solving algorithm that uses lazy compilation scheme. Since Boolean formulae, to which the input MRPP instance is reduced in SMT-CBS, are derived from the set of candidate paths, the effect of sparsification of the set is twofold: (1) it leads to smaller target Boolean formulae that can be constructed faster and (2) the satisfiability of formulae can be decided by the SAT solver faster, altogether improving the reduction-solving-interpretation loop in SMT-CBS. At the same time, optimality guarantees in the modified SMT-CBS are kept via maintaining easily verifiable property of the sparse set of candidate paths.
The paper is organized as follows: the MRPP problem and basic compilationbased methods for MRPP are introduced first. Then the concept of lazy compilation schemes is described from which the sparsification technique is derived, the main contribution. The new algorithm based on the sparsification technique, called Sparse-SMT-CBS, is developed next and its experimental evaluation follows.

Background
In this section we introduce the problem of path planning for multiple robots formally and present optimal solving algorithms with focus on compilation-based techniques.

Multi-robot Path Planning
In MRPP, the time is discretized into time steps. The configuration of robots at timestep t is denoted as s t . Each robot r i has a start position s 0 (r i ) ∈ V and a goal position s + (r i ) ∈ V . At each time step a robot can either move to an adjacent location or wait in its current location.
Formally, an MRPP instance is a tuple Σ = (G = (V, E), R, s 0 , s + ) where s 0 : R → V is an initial configuration of robots and s + : R → V is a goal configuration of robots. A solution for Σ is a sequence of configurations S(Σ) = [s 0 , s 1 , ..., s µ ] such that s t+1 results from valid movements from s t for t = 1, 2, ..., µ − 1, and s µ = s + . Orthogonally, the solution can be represented as a set of paths for individual robots.
At each time step a robot can either move to an adjacent location or wait in its current location. The task is to find a sequence of move/wait actions for each robot r i , moving it from s 0 (r i ) to s + (r i ) such that robots do not conflict, i.e., do not occupy the same location at the same time and do not traverse the same edge in opposite directions. An example of MRPP instance and its solution is shown in Figure 1. Often various cumulative objectives are optimized in MRPP. We will develop all concepts in this paper for the sum-of-costs objective, one of the most frequently used, formally defined as follows: Observe that in the sum-of-costs we accumulate the cost of wait actions for robots not yet reaching their goal vertices. A feasible solution of a solvable MRPP instance can be found in polynomial time [15].
Finding an optimal solution with respect to the sum-of-costs objective is NPhard [30,37] and also determining the existence of a solution that differs from the optimum by a factor less than 4/3 is NP-hard too [22]. Therefore designing algorithms based on search and SAT for MRPP is justifiable.

Compilation-based Approaches
The idea behind compilation that uses the SAT paradigm is to construct a Boolean formula whose satisfiability corresponds to existence of a solution of sum-of-costs SoC to a given MRPP Σ. Moreover, the approach is constructive; that is, the formula exactly reflects the MRPP instance and if satisfiable, solution of MRPP can be reconstructed from satisfying assignment of the formula.
There are two ways how to connect satisfiability of the formula and solvability of Σ: using either equivalence or implication.
We say F(SoC ) to be a complete Boolean model of MRPP. Complete Boolean models were the used in makespan optimal SAT-based solvers for MRPP [31] and in MDD-SAT [33], the first sum-of-costs optimal SAT-based solver. A natural relaxation from the complete Boolean model is an incomplete Boolean model where instead of the equivalence between solving MRPP and the formula we require an implication only. Incomplete models are inspired from the SMT paradigm and are used in the recent sum-of-costs optimal solver SMT-CBS [32]. Being able to construct formula F one can obtain optimal MRPP solution by checking satisfiability of F(0), F(1), F(2),... until the first satisfiable F(SoC ) is met. This is possible due to monotonicity of MRPP solvability with respect to increasing values of common cumulative objectives such as 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.
Construction of F(SoC ) relies on the time expansion of underlying graph G. Having SoC , the basic variant of time expansion determines the maximum number of time steps µ (also refered to as a makespan) such that every possible solution of the given MRPP with the sum-of-costs less than or equal to SoC fits within µ timesteps (that is, no robot is outside its goal vertex after µ-th timestep if the sum-of-costs SoC is not to be exceeded).
The time expansion itself makes copies of vertices V for each timestep t = 0, 1, 2, ..., µ. That is, we have vertices v t for each v ∈ V time step t. Edges from G are converted to directed edges interconnecting timesteps in time expansion.
Directed edges (u t , v t+1 ) are introduced for t = 1, 2, ..., µ − 1 whenever there is {u, v} ∈ E. Wait actions are modeled by introducing edges (u t , t t+1 ). A directed path in time expansion corresponds to trajectory of a robot in time. Hence the modeling task now consists in construction of a formula in which satisfying assignments correspond to directed paths from s 0 0 (r i ) to s µ + (r i ) in the time expansion.
Assume that we have time expansion is that it is TRUE if and only if robot r i traverses edge {u, v} between time steps t and t + 1.
Finally constraints are added so that truth assignment are restricted to those that correspond to valid solutions of a given MRPP. Added constraints together ensure that F(SoC ) is a complete propositional model for given MRPP.
We here illustrate the model by showing few representative constraints. For the detailed list of constraints we refer the reader to [33].
Collisions between robots can be eliminated by the following constraint over X t v (a i ) variables for every v ∈ V and timestep t: Next, there is a constraint stating that if robot 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: Other constraints ensure that truth assignments to variables per individual robots form paths. That is if robot r i enters an edge it must leave the edge at the next time step.
A common measure how to reduce the number of decision variables derived from the time expansion is the use of multi-valued decision diagrams (MDDs) [1,26]. The basic observation that holds for MRPP is that an robot 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 robot 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 robot, 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 µ − t timesteps. Time expansion using MDDs is shown in Figure 2. The combination of SAT-based approach and MDD time expansion led to the MDD-SAT algorithm.

CBS and Lazy Compilation
Conflict-based search (CBS) [25] is a popular algorithm for solving MRPP optimally. From the compilation perspective, the CBS algorithm could be understood as a lazy method that tries to solve an underspecified problem and relies on to be lucky to find a correct solution even using this incomplete specification. There is another mechanism that ensures soundness of this lazy approach, the branching scheme. If the CBS algorithm is not lucky, that is, the candidate solution is incorrect in terms of MRPP rules, then the search branches for each possible refinement of discovered MRPP rule violation and the refinement is added to the problem specification in each branch. Concretely, the MRPP rule violations are conflicts of pairs of robots such as collision of a i ∈ A and a j ∈ A in v at time step t and the refinements are conflict avoidance constraints for single robots in the form that a i ∈ A should avoid v at time step t (for a j analogously).
Analogously the avoidance for edge conflicts can be done. For the sake of brevity, all the concepts developed further will be introduced only for vertex conflicts.
The idea of laziness of CBS has been combined with compilation-based approaches in SMT-CBS algorithm presented using pseudo-code as Algorithm 1. The algorithm is divided into two procedures: SMT-CBS representing the main loop and SMT-CBS-Fixed solving the input MRPP for a fixed cost SoC . 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. The incomplete Boolean model is constructed from MDDs by encode-Incomplete that produces encoding from MDD-SAT that ignores specific collisions between robots.
The conflict resolution in standard CBS implemented as high-level branching is here represented by refinement of F(SoC ) with disjunction (line 22). Branching is thus deferred into the SAT solver. The advantage of SMT-CBS is that it builds the formula lazily; that is, it adds constraints on demand after a conflict occurs. Such approach may save resources as solution may be found before all constraint are added.

Sparsification in Lazy Compilation
Although lazy compilation in SMT-CBS is the major factor that reduces the size of generated Boolean formulae during the solving process compared to MDD-SAT, the reduction concerns only the conflict avoidance constraints for pairs of robots (binary disjunctions). The number of nodes as well as the number of directed edges in the MDDs is not reduced by laziness and hence the number of variables and constraints modeling the existence of directed paths in MDDs in the target Boolean formula is the same as in MDD-SAT. For instances that take place on large graphs, the size of MDDs directly reflected in the size of the formula could still be prohibitive.
Therefore we suggest to simplify the formulae by reducing the number of directed paths that are encoded. To do this, we suggest to use sparse sets of candidate paths for each robot that satisfy given sum-of-costs and makespan bounds. That is, instead of considering all such paths as done in MDDs we consider only a relevant subset of them. The sparse set of candidate paths will be denoted Π. Similar concept called the pool of paths has been used in the context of MIP-based compilation for MRPP [12] which however does not explicitly focus on sparsification.
We integrated the sparse paths set reasoning into the SMT-CBS framework, designing a new algorithm we called Sparse-SMT-CBS. The pseudo-code of Sparse-SMT-CBS is shown as Algorithm 2.
Sparse-SMT-CBS uses identical sum-of-costs and makespan bounds increasing scheme as SMT-CBS at the high-level (lines [1][2][3][4][5][6][7][8][9][10][11]. Each iteration at the highlevel resolves a question whether there exists a solution to the input MRPP Σ such that it fits in the current sum-of-costs SoC and makespan µ. This question is compiled as a series of Boolean formulae and consulted with the SAT solver at the lower-level (lines 12-30).
The lower-level in Sparse-SMT-CBS is different from SMT-CBS. In both algorithms it tries to find a non-conflicting set of paths satisfying SoC and µ, but the set of candidate paths from which SMT-CBS selects is fixed in advance in MDD, while Spare-SMT-CBS starts with a minimal set of candidate paths and each time a new conflict is discovered the set of candidate paths is extended to reflect the new conflict. To keep soundness and optimality of the algorithm, the sparse set of candidate paths must be selected to according to the following conditions. Definition 4. (path feasability). Let C be a set of conflicts of the form {r i , v, t} forbidding robot r i ∈ R to reside in v ∈ V at timestep t. We say a path path(r i ) = [p 0 , p 1 , ..., p m ] for robot r i to be feasible with respect to C if and only if {r i , p t , t} / ∈ C for ∀t ∈ {0, 1, ..., m}.
The sparse set of paths for robot r i denoted Π(r i ) with respect to a set of conflicts C and makespan µ must satisfy the following property: -(P1) Π(r i ) contains at least one feasible path with respect to each subset of conflicts C ⊆ C.
The property (P1) must be reflected in implementation of new-Paths function called at line 25. Intuitively said, (P1) ensures that after discovering a new conflict at least one path avoiding the new conflict for each possible combination of previous conflicts is added to Π provided that such path exists for given makespan bound µ.
Algorithm 2: SMT-based optimal MRPP solver with sparsification of the set of candidate paths. The sparse set of candidate paths is used to build an incomplete Boolean MRPP model F(SoC ) (line 14) which is subsequently solved by the SAT solver. If there is no satisfying truth-value assignment for F(SoC ) (line 30), then we can conclude taking into account (P1) that there is no solution of the input MRPP satisfying the SoC and µ bounds and the control returns to the high-level where the bounds are incremented (lines [10][11]. If a satisfying truth-value assignment of F(SoC ) is found (line 16), then it has to be interpreted and checked against MRPP rules, that is, it is checked for collisions between robots (line 18). If there are no collisions, the algorithm can return a valid MRPP solution (line 20). If a collision is detected (lines 21-28), a proper treatment must be applied.
This includes (1) extending the model F(SoC ) with a collision elimination constraint, a disjunction forbidding a pair of conflicting actions to take place at once (lines 21-23) and (2) (new to Sparse-SMT-CBS) and extending the sparse set of candidate paths Π with new paths reflecting newly discovered conflicts (line [24][25][26]. It may however happen that no new path could be found any robot which again together with property (P1) means that there is no solution for current SoC and µ bounds (lines [27][28] and control returns to the high-level to continues with the next iteration. Without proof let us state the following proposition summarizing the soundness and optimality of the Sparse-SMT-CBS algorithm. Let us note that unsolvable input MRPP can be detected in advance by some polynomial-algorithm such as Push-and-Rotate [35]. Proposition 1. Sparse-SMT-CBS finds sum-of-costs optimal solution for a solvable input MRPP Σ provided the sparse set of candidate paths Π satisfies property (P1).
Paths included into Π can be found by various shortest path algorithms like A* that take into account the set of conflicts. Moreover deciding what paths will be preferably included in Π provides a room to integrate MRPP specific heuristics such as cardinal conflict aggregation [17] or symmetry breaking [18] which is known to be difficult for MDD-SAT and SMT-CBS.
Notice also that property (P1) is used is an argument for correct functionality of the algorithm only when it detects non-existence of solution for the current bounds. Except these two moments the property can be relaxed which could provide greater room for integrating MRPP specific heuristics.

Details of the Boolean Model
Eventually it may happen that the sparse set of paths grows during the course of low-level phase so that all possible paths satisfying given sum-of-costs and makespan bounds are eventually included. In such a case, the compression based on MDDs is useful similarly as in SMT-CBS or MDD-SAT. The concept of MDD is useful even for representing sparse sets of paths since often to avoid a new conflict, a new path arriving to the set differs only little from already represented paths.
Therefore we extend the usage of MDDs on sparse sets of candidate paths. To distinguish MDDs representing sparse sets we denote them as sparse MDDs (SMDDs). Given maximum number of steps µ and any (sparse) set of paths Π(r i ) in the time expansion of G of length at most µ, we are able to construct SMDD i that represents Π(r i ). That is, any path from Π(r i ) is represented in SMDD i and every path represented in SMDD i is an element of Π(r i ).
The encoding used in Sparse-SMT-CBS follows MDD-SAT with collision avoidance constraints omitted but instead of deriving decision Boolean variables and constraints from MDDs they are derived from SMDDs. That is, a Boolean variable X (r i ) t v is introduced for each node v t in SMDD i and a variable E(r i ) t u,v is introduced for each edge in SMDD i . Constraints are introduced analogously.
Observe that the sparser the SMDDs are the smaller Boolean model is obtained. SMDDs from the running example are shown in Figure 3. Initially shortest paths are included in Π(r i ) connecting robot's starting vertex and its goal, one shortest path per robot. However, the initial choice of paths is poor leading to a collision in v 5 at timestep 2 which is detected by Sparse-SMT-CBS and alternative paths reflecting the conflict are suggested for each robot by the new-Paths function. The new paths are included in SMDDs as shown in the right part of Figure 3. For these new SMDDs, non-conflicting path can be found.

Experimental Evaluation
We performed an extensive evaluation of the SMT-CBS and Sparse-SMT-CBS algorithms on standard benchmarks from movingai.com [8,26,29]. To provide broader perspective we also include comparison with the CBS algorithm, a search-based algorithm. Representative part of results is presented in this section.

Benchmarks and Setup
We implemented Sparse-SMT-CBS in C++ using the existing implementation of SMT-CBS. Both algorithms are built on top of the Glucose 3.0 SAT solver [2] that still ranks among the best SAT solvers according to recent SAT solver competitions [3]. The search for new candidate paths that reflect new conflict is done via A* algorithm that takes into account the current set of conflicts. Each conflict is both avoided and ignored during the search by A* resulting in finding paths with respect to all subsets of conflicts. Moreover the strategy of path generation is that priority is given to path reflecting fewer conflicts, starting with path for single conflict, while paths reflecting two and more conflicts are considered later. This turned out to be a good heuristic according to preliminary experiments.
As for CBS we used implementation from [4] written in C#. Although this implementation of CBS does not use recent MRPP heuristics like rectangle reasoning [17] we consider it suitable for our experiments as implementations of both Sparse-SMT-CBS and SMT-CBS also do not use any MRPP specific heuristics. Altogether all implementations in the conducted evaluation are based only on the core idea of respective algorithm.
The SAT solver we used supports incremental mode which means that when the formula is extended with new variables and clauses the solver does not need to start from scratch but it can use learned clauses from its previous runs. This incremental mode is highly utilized across the low-level phase of both SMT-CBS and Sparse-SMT-CBS where the target Boolean formula is extended. However, each new iteration of the main loop starts with new instance of the SAT solver since establishing aleviated cost bounds cannot be easily done incrementally.
All experiments were run on system consisting of Xeon 2.8 GHz cores, 32 GB RAM, running Ubuntu Linux 18. 2 The experimental evaluation has been done on diverse instances consisting of 4-connected grid maps ranging in sizes from small to relatively large.
Grid maps are used for discretization of real environments. Robots traverse map using orthogonal movements (diagonal moves are not used) hence unit time per move can be realistically assumed. Moreover this discretization turned out to be sufficient for execution of plans with real robots as shown in our related research on simulations with small mobile robots [9].
We varied the number of robots to obtain instances of various difficulties while initial and goal configurations of robots were generated according to scenarios provided on movingai.com. Depending on the map size, we generated instances with up to 64 (small maps) or 128 (large maps) robots and 25 different instances per number of robots. The time limit in all test was set to 128 seconds. Presented results were obtained from instances solved within this timeout.

Runtime Results
Results are presented in Figures 4, 5, and 6. We present success rate and sorted runtimes. Success rate shows the ratio of instances solved under the time limit of 128 seconds out of 25 instances per number of robots. Sorted runtimes are inspired by the cactus plots from the SAT Competition [3]. The cactus plot for rumtime has been generated by taking runtimes of all instances solved under the time limit by a given algorithm and sorting them along x-axis; so the x-th data-point represents the runtime of x-th easiest instance for the given algorithm. The faster algorithm typically yields to a lower curve in the cactus plot but differences for various regions of the plot can be observed too.
The general trend observable across all maps from success rate and sorted runtimes is that Sparse-SMT-CBS represents a significant improvement over SMT-CBS. The performance gap between SMT-CBS and Sparse-SMT-CBS grows with growing number of robots. The second trend that is observable in the results is that for larger maps (maze-128-128-10 and lak303d) the advantage of Sparse-SMT-CBS is greater than in small maps (empty-16-16 and random-32-32-10). Sorted runtimes comparison also shows that in easy instances the sparsification technique does not help significantly. However as the difficulty of instances grows it starts to be increasingly beneficial.
Comparison with CBS shows an expectable trend that due to its negligible overhead, the CBS algorithm dominates in easy instances where both Sparse-SMT-CBS and SMT-CBS need to deal with complex instance compilation process that eventually does not pay off. As difficulty of instances grow, the advanced learning mechanisms and intelligent space search pruning implemented in SAT solvers has greater impact resulting in better performance of SMT-CBS and Sparse-SMT-CBS in more difficult instances.
The known disadvantage of SMT-CBS is that in large maps like warehouse-10-20-10-2-1 or lak303d it generate a formulae that are too large which causes degradation in performance. According to our experiments it seems that sparsification in SMT-CBS helps the solver especially on large maps. The reason is that the size of MDDs for large maps is often prohibitive and causes significant difficulty for the SAT solver as it needs to deal with a large formula derived from MDD. Sparsification enables choosing few promising paths that are represented in SMDDs which improves both the Boolean formula construction process as well as its solving.

Conclusion
We suggested a technique of sparsification of the set of candidate paths in the context of SAT-based approach to multi-robot path planning (MRPP). The technique aims on currently the most significant drawback of compilation-based approaches to MRPP which is the performance on large graphs. The sparsification technique suggests to construct the target Boolean formula according to a sparse set of candidate paths for each robot which leads to constructing smaller formulae that can be answered by the SAT solver faster. We integrated sparsification into SMT-CBS, a state-of-the-art SAT-based optimal algorithm for MRPP, while keeping its optimality guarantees. According to our experiments on a number of benchmarks, the new algorithm called Sparse-SMT-CBS performs significantly better than SMT-CBS especially on MRPPs with large graphs and outperforms basic search-based CBS.
Another important advantage of sparsification is that it provides a room for integrating domain specific heuristics via giving a preference to some paths being selected into the set of candidate paths for a robot. Integration of heuristics is difficult in previous SAT-based MRPP solvers like MDD-SAT and SMT-CBS.
For future work we plan to further generalize the concept of sparsification for different variants of MRPP.