Reduced Time-Expansion Graphs and Goal Decomposition for Solving Cooperative Path Finding Sub-Optimally

1 Introduction and Motivation

The problem of cooperative path-finding (CPF) [Kornhauser et al., 1984; Silver, 2005, Ryan, 2008] is a graph theoretical abstraction for many real life problems where the task is to cooperatively relocate a group of robots or other movable objects in a collision free manner. Each agent of the group is given its initial and goal position in the environment. The problem consists in constructing a spatial temporal plan for each agent by which it can relocate from its initial position to the given goal. The environment where agents move is modeled as an undirected graph [Kornhauser et al., 1984] where vertices represent locations and edges represent possibility of relocation between two locations.

Agents are represented as abstract items placed in vertices while at most one agent is located in each vertex. An agent can instantaneously relocate itself to the neighboring vertex assumed the target vertex is unoccupied and no other agent is trying to enter the same target vertex.

In this research, we further develop solving of CPF by translating it to propositional satisfiability (SAT) [Biere et al., 2009]. Recent propositional encodings [Surynek, 2012a, 2012b, 2013, 2014] of CPF are based on time expansion of the graph modeling the environment so that the encoding is able to represent arrangements of agents over the graph at all the time steps up to the final one. Since there may be many time-steps before all the agents reach their goals, these encodings may become extremely large and hence unsolvable in reasonable time. We are trying to overcome this limitation by reducing the expansion of the graph in this work.

1.1 Context of Related Works

The approach to solve CPF by reducing it to SAT has multiple alternatives. There exist algorithms based on search that find makespan optimal or near optimal solutions. The seminal work in this category is represented by Silver's WHCA* algorithm [Silver, 2005]. Recent contributions include OD+ID [Standley and Korf, 2011], which is a combination of A* and powerful agent independence detection heuristics, and ICTS [Sharon et al., 2013] which employs the concept of increasing cost tree (instead of makespan, the total cost of solution is optimized). Other approaches resolve conflicts among robot trajectories when avoidance is necessary [Čáp et al., 2013; Barer et al., 2014; Wagner and Choset, 2015].

Fast polynomial time algorithms for generating makespan suboptimal solutions include PUSH-AND-ROTATE [de Wilde et al., 2014]. The drawback of these algorithms is that their solutions are dramatically far from the optimum.

Translation of CPF to a different formalism, namely to answer set programming (ASP), has been suggested in [Erdem et al., 2013]. Integer programming (IP) as the target formalism has been also used [Yu and LaValle, 2013]. The choice of SAT as the target formalism is very common in domain independent planning where the idea of time expansion [Kautz and Selman, 1999; Huang et al., 2010] and its reductions [Wehrle and Rintanen, 2007] are studied.

2 Formal Definition of CPF

to used be can ሻܧ ǡܸሺ ൌ ܩ An arbitrary undirected graph model the environment where agents are moving. The placement of agents in the environment is modeled by ǥǡ ǡʹܽ ǡͳܽሼ ൌ ܣ assigning them vertices of the graph. Let agents of arrangement an then, agents, of set finite a be ሽ ߤܽ location a by described fully is ܩ in vertices of graph in located be can agent one most At .ܸืܣ ǣߙ function invertible. uniquely is ߙ each vertex; that is

Definition 1 (COOPERATIVE PATH FINDING). An instance of ൌ ܩሾ cooperative path-finding problem is a quadruple ȭ ൌ define ൅ߙ and Ͳߙ functions location where ሿ൅ߙ ǡͲߙ ǡܣ ǡሻܧ ǡܸሺ ܩ in ܣ the initial and the goal arrangement of a set of agents respectively. □

The dynamicity of the model supposes a discrete time time ht-݅ the at ݅ߙ divided into time steps. An arrangement step can be transformed by a transition action which instantaneously moves agents in the non-colliding way to ݅ߙ between transition The .ͳ൅݅ߙ form a new arrangement conditions: validity following the satisfy must ͳ൅݅ߙ and

• ܧ א ሽሻܽሺͳ൅݅ߙ ǡሻܽሺ݅ߙሼ or ሻܽሺͳ൅݅ߙ ൌ ሻܽሺ݅ߙ either ܣ א ܽ׊ ♥ (agents move along edges or not move at all), (1)
• (agents move to vacant vertices only), and (2)
• ሻܾሺͳ൅݅ߙ ് ሻܽሺͳ൅݅ߙ ֜ ܾ ് ܽ ܣ א ܾ ǡܽ׊ ♥ (no two agents enter the same target/unique invertibility of resulting arrangement). (3)

൯ሻܽሺͳ൅݅ߙ ് ሻܾሺ݅ߙ ܣ א ܾ׊൫ ֜ ሻܽሺͳ൅݅ߙ ് ሻܽሺ݅ߙ ܣ א ܽ׊ ♥

Ͳߙ The task in cooperative path finding is to transform CPF of illustration An .൅ߙ using above valid transitions to and its solution is depicted in Figure 1.

Definition 2 (SOLUTION, MAKESPAN). A solution of a ൌ ȭ instance finding path cooperative a to ݉ makespan ൌ റݏ arrangements of sequence a is ሿ൅ߙ ǡͲߙ ǡܣ ǡܩሾ of result a is ͳ൅݅ߙ and ൅ߙ ൌ ݉ߙ where ሿ݉ߙ ǥǡ ǡʹߙ ǡͳߙ ǡͲߙሾ □ . ͳ െ݉ǡ ǥ ͳǡʹǡ ൌ ݅ every for ݅ߙ valid transition from

It is known that finding makespan optimal solution to CPF is ��-hard [Ratner and Warmuth, 1986].

3 (Sub)optimization in CPF via SAT

The approach we are suggesting here to obtain parameter optimal solutions is to employ propositional satisfiability (SAT) solving as the key technology. This approach has been already successfully applied in obtaining makespan optimal plans in domain-independent planning [Kautz and Selman, 1999; Huang et al., 2010] as well as in CPF [Surynek, 2013].

that such ሻߟ ǡȭሺܨ In case of CPF, a propositional formula it is satisfiable if and only if a given CPF ȭ with makespan to able Being constructed. be can solvable is ߟ bound optimal the obtain can one ሻߟ ǡȭሺܨ construct such a formula makespan for the given CPF ȭ by asking multiple queries different with satisfiable is ሻߟ ǡȭሺܨ whether formula .ߟ makespan bounds Various strategies of the parameter for queries exist for getting the parameter optimal solution. The simplest is to try the to equal is ߟ until ǥ ͳǡʹǡ ൌ ߟ sequentially makespans optimum (minimum). This strategy will be further referred as sequential increasing. Pseudo-code of the strategy is listed as Algorithm 1.

Algorithm 1. SAT-based parameter optimal CPF solving - sequential increasing strategy. The algorithm sequentially finds encoding propositional a that for ߟ the smallest possible makespan solvable. is ሻ൅ߙ ǡͲߙ ǡܣ ǡܩሺ of a given CPF ȭ ൌ

input: ȭ - a CPF instance

output: a pair consisting of the optimal parameter and

corresponding parameter optimal solution

pair :ሻሻ൅ߙ ǡͲߙ ǡܣ function Find-Optimal-Parameter ሺȭ ൌ ሺ�ǡ ͳ ՚ ߟ 1: 2 loop 3: ሻߟ ǡߑሺ ՚Encode-CPF-as-SAT ሻߟ ǡȭሺܨ 4: then ሻሻߟ ǡȭሺܨሺ if Solve-SAT 5: ሻߟ ǡȭሺܨ of valuation satifying a be ݂ let 6: ሻ݂ ǡߟሺ return 7: ͳ ൅ ߟ ՚ ߟ ሻ׎ 8: return ሺλǡ

4 Reduced Time Expansion Graph

The main drawback of makespan optimal CPF solving via SAT is the large size of the formulae that encode the optimization questions [Surynek, 2013, 2014]. The size of encoding formulae becomes especially prohibitive when they encode questions if a solution with a large makespan exists. This is due to the fact that existing encodings expands the graph modeling the environment over the time the of step time each At .ߟ up to the given makespan bound expansion arrangement of agents over the graph is represented and constraints ensure that only transitions conforming to validity conditions are possible between arrangements at consecutive time steps.

Our idea hence was to reduce the time expansion with possible relaxation of the requirement of makespan optimality of the solution. The key observation is that if there is no need of any complex avoidance between agents (there is no need to visit a single vertex multiple times), no time expansion of the graph is necessary at all. The question if there is a solution (not necessarily makespan optimal) can be stated as a question of existence of vertex disjoint paths connecting initial positions of agents with their goals in the original graph. Translating of this question into SAT is possible as well.

Nevertheless, in real situations movement interactions among agents require complex avoidance. A single vertex may need to be visited multiple times. This led us to the suggestion of a concept of reduced time expansion graph, which combines the expansion reduction with ability to represent complex avoidance.

Definition 3 (REDUCED TIME EXPANSION GRAPH - and graph undirected an be ሻܧ ǡܸሺ ൌ ܩ Let .)ሻߴ ǡܩ”�š’�ሺ layers time ߴ with graph expansion time reduced A Գ. א ߴ ൈ ܸሺ ൌ ሻߴ ǡܩ”�š’�ሺ graph directed a is ܩ associated with ൌ ݈ Ǣܧ א ሽݒ ǡݑሼȁሻሿ݈ ǡݒሾ ǡሿ݈ ǡݑሼሺሾ ൌ Ԣܧ where ሻԢܧ ǡሽߴ ሼͳǡʹǡǥǡ □ ͳሽ. െ ߴ ǥǡ ͳǡʹǡ ൌ ݈ ȁ ൅ͳሿሻ ݈ ǡݒሾ ǡሿ݈ ǡݒሼሺሾ ׫ ሽߴ ͳǡʹǡ ǥ ǡ

Note, that for each original undirected edge there are two directed arcs in both directions in the reduced time expansion graph. A time-layer in the reduced time ሻߴ ǡܩ”�š’�ሺ expansion graph is an induced sub-graph of .ሽߴ ǡ ǥ ሼͳǡʹǡ א ݈ given a for ሽ݈ሼ ൈ ܸ over the set of vertices

a as viewed be can ሿ൅ߙ ǡͲߙ ǡܣ ǡܩሾ Solving of CPF ȭ ൌ connect that ሻߴ ǡܩ”�š’�ሺ search for vertex disjoint paths in initial positions and goals in the first and the last time-layer is ߴ respectively provided that the number of time-layers sufficiently high. The idea is illustrated in Figure 2.

Encoding Propositional DEXALER-ࣖ 4.1

The correspondence between the existence of vertex disjoint paths and the existence of a solution of CPF established in the previous section provides a guide how to design required propositional encoding. We merely need to design a propositional formula preferably in conjunctive normal form (CNF) [Biere et al., 2009] that is satisfiable if and only if vertex disjoint paths connecting initial position and goals ԳǤ א ߴ for ሻߴ ǡܩ”�š’�ሺ exist in

Intuitivelly, the size and the structure of the resulting formula matters when it is solved by a SAT solver. Our choice was to design an encoding that is space efficient and contains short clauses. Note that short clauses support unit propagation [Biere et al., 2009].

The encoding is separated into two parts. The first part is purely propositional and consists of variables that express selection of vertices and edges into paths - this can be also regarded as occupancy/selection of path by a flow of commodity. The inspiration for this design comes from the theory of network flows [Ahuja et al., 1993]. The absence of necessity to distinguish between individual agents enables expressing the requirement that paths should be vertex disjoint as simple capacity constraints.

The distinguishable agents are treated in the second part of the model where a bit vector using binary encoding is what express to ሻߴ ǡܩ”�š’�ሺ associated with each vertex in agent is occupying that. The benefit of using bit-vectors is that equality can be easily expressed over them. Both parts are put together by introducing a constraint that requires occupation by the same agent at both ends of a selected -ߴ edges. Formally, the encoding - which we called RELAXED - is introduced in the following definition.

Let .)ሻȭሺܧܴെߴܨ - encoding DEXALER-ߴ( Definition 4 DEXALER-ߴ A .ሻܧ ǡܸሺ ൌ ܩ with CPF a be ሿ൅ߙ ǡͲߙ ǡܣ ǡܩሾ ȭ ൌ encoding for CPF ȭ consists of the following collections of domain finite :ሽߴ ሼͳǡʹǡǥǡ א ݈ variables for every time layer are (that ܸ א ݒ every for ሽߤ ǥǡ ሼͲǡͳǡ א ݈ݒࣛ variables every for ݈ݒࣲ encoded as bit vectors), propositional variables ݒǡݑࣟ variables propositional and ,ܸ א ݒ ordered every for ݈ edge single a for is, (that ܧ א ሽݒ ǡݑሼ that such ݒ ǡݑ pair ݒǡݑࣟ variables propositional two have we ݈ and ܧ א ሽݒ ǡݑሼ ݈ ݑǡݒࣟ and propositional of set a is there Additionally, ). ݈ ͳሽ െ ߴ ǡ ǥ ሼͳǡʹǡ א ݈ and ܸ א ݒ every every for ݈ݒࣟ variables representing interconnections between time layers. follows: as are encoding DEXALER-ߴ Constraints of

(if an edge within a time layer or between time layers is non-empty then its both ends are non-empty)

(for every source vertex at the first time layer all the incoming directed edges are empty)

(for every destination vertex at the last time layer all the outgoing directed edges are empty)

(if an edge is non-empty then there is the same agent at its both endpoints)

σ ݒǡ ݑࣟ ݈ ͳ ൑ ݈ݑࣟ൅ ܧאሽݒǡݑሼȁݒ the last one then exactly one of its outgoing edges is (12)

(if a vertex is non-empty at a time layer other than non-empty as well)

(if a non-destination vertex at the last time layer is non-empty as well)

ݒǡ ݑࣟ ݑ ് ሻܽሺ൅ߙሻܣ א ܽ׊ሺ ͳ ൑ ܧאሽݒǡݑሼȁݒ non-empty then exactly one of its outgoing edges is

(if a vertex is non-empty at a time layer other than the first one then exactly one of its incoming edges is non-empty as well).

then exactly one of its incoming edges is non-empty as

ݒǡ ݑࣟ ͳ ൑ ͳെ݈ݒࣟ൅ ܧאሽݒǡݑሼȁݑ ڀ ֜ ͳݒࣲ ͳ well). □

Initial and goal arrangements are expressed as constraints over variables of the first and the last time layer. Note that some agents do not need to be assigned any goal if we do not care about their final positions.

the in encoding DEXALER-ߴ The resulting formula of the let proof Without .ሻȭሺܧܴെߴܨ CNF form will be denoted as us summarize the size of the encoding.

The SIZE). ENCODING DEXALER-ࣖ( Proposition 1 ή ߴሺࣩ is ሻߑሺܧܴെߴܨ number of propositional variables in is clauses of number the and ሻሻȁܧȁ ൅ ۀͳሻ ൅ ߤሺʹ‰‘Žڿ ή ȁܸሺȁ � ሻሻ. ͵ȁܸȁ ൅ ۀ൅ͳሻ ߤሺʹ‰‘Žڿ ή ሻȁܧȁ ൅ ȁܸሺሺȁ ή ߴሺࣩ

in paths disjoint vertex of ሽ ߤߨ ǡ ǥǡʹߨ ǡͳߨሼ ൌ ߎ A set ሿߴ ǡሻ݅ܽሺ൅ߙሾ with ሿͳǡሻ݅ܽሺͲߙሾ connects ݅ߨ ”�š’�ሺ�ǡ Ԃሻ so that satisfiable. is ሻߑሺܧܴെߴܨ if only and if exists ߤ ǡ ǥ ͳǡʹǡ ൌ ݅ for The extraction of a solution of CPF ȭ from a satisfying as pseudo-code using shown is ሻߑሺܧܴെߴܨ valuation of Algorithm 2.

The algorithm tracks moves of agents towards their exits from the current time layer of the reduced time expansion in that Note, recorded. is ߙ graph during which the solution each time layer the time step at which agents exit the layer is synchronized among all the agents (that is, agents exit at the same time step). It may therefore occur that agents wait for the last agent to finish its movements in the layer before they exit the layer together into the next one. The algorithm allows us to state the following theorem (proof is ommited).

SATISFACTION). ሻ઱ሺࡱࡾെࣖࡲ Theorem 1 (SOLUTION OF ઱ AND ൌ ܣ with ሻ൅ߙ ǡͲߙ ǡܣ ǡܩሺ A solution of a CPF ȭ ൌ that for Գ א ߴ exist there if only and if exists ሽ ߤܽ ǡǥǡʹܽ ǡͳܽሼ � satisfiable. is ሻȭሺܧܴെߴܨ formula

The original goal to reduce the size of the encoding by Ԃ- that fact the by fulfilled is ܩ reducing the expansion of RELAXED encoding needs no more time-layers than encodings for makespan optimal CPF solving. Moreover, there are cases where Ԃ-RELAXED encoding needs significantly fewer time expansions - see example in Figure 2 where 3 time expansions are needed in Ԃ-RELAXED encoding while makespan optimal encodings need 8 time expansions.

DEXALER-ߴ Algorithm 2. Solution extraction algorithm for encoding. A sequence of arrangements of agents forming a fo݂ solution of given CPF ȭ is extracted from satisfying valuation ȭ. of encoding DEXALER-ߴ representing ሻȭሺܧܴെߴܨ formula

input: ȭ - an instance of CPF encoding DEXALER-ߴ in layers time of number the - ߴ ሻȭሺܧܴെߴܨ of valuation satisfying a - ݂

output: makespan and sequence of arrangements of agents ൅ߙ ,...,ͳߙ ,Ͳߙ forming the solution

DEXALER-ߴExtract-Solution- function

pair :ሻ݂ ǡߴ ǡሿ൅ߙ ǡͲߙ ǡܣ ǡሻܧ ǡܸሺ ൌ ܩሾ ሺȭ ൌ layer time a at movements which at step time // Ͳ ՚ šƒߟ 1: // are finished 2: do ߴ ǡ ͳǡʹǡǥ ൌ ݈ for each 3: šƒߟ ՚ ‹ߟ // time step at which movements // at a time layer start 4: do ܣ א ܽ for each 5: ‹ߟ ՚ ߟ 6: ሻܽሺ ‹ߟߙ ՚ ݑ 7: ሻܧܵܮܣܨ ൌ ሻ ݈ݑࣟሺ݂ and ߴ ് ݈ሺ while do ሻሻܽሺ൅ߙ ് ݑ and ߴ ൌ ݈ሺ or 8: ݑ in located be will ܽ agent // ݑ ՚ ሻܽሺߟ൒ߙ ߟ // at all the time steps ൒ 9: do ܧ א ሽݒ ǡݑሼ that such ܸ א ݒ for each 10: ݒǡݑࣟ൫݂ if then ܧܷܴܶ ൌ ൯ ݈ 11: ݒ ՚ ݑ 12: ൅ͳ ߟ ՚ ߟ 13: ሻߟ ǡ šƒߟ՚ƒš༌ሺ šƒߟ 14: ݑ ՚ ሻܽሺ ߟ൒ߙ ൧ሻ šƒߟߙ ǡ ǥ ǡͳߙ ǡͲߙൣ ǡ šƒߟሺ 15: return

Let ENCODING). DEXALER-ࣖ Proposition 2 (ADVANTAGE OF Then ȭ. CPF a in achievable makespan optimal an be ߟ a exists there Moreover, .ߟ ൑ ߴ for solvable is ሻȭሺܧܴെߴܨ � holds. ߟ ൏ ߴ CPF instance ȭ where strict inequality

The number of time layers in Ԃ-RELAXED encoding that grants finding a solution corresponds rather to the intensity of interactions among agents. Hence to further reduce the size of the encoding via reducing the number of time layers we suggest decomposing solving of a given CPF ȭ into solving multiple CPFs in which intesity of interactions among agents is low and thus they can be solved by satifying Ԃ-RELAXED encoding formualae consisting of few time layers.

The suggested decomposition corresponds to placing agents to their goals one by one while individual CPFs represents relocating a single agent where positions of previously placed agents are preserved. The process is called UniAGENT solving and it is formally described as Algorithm 3.

Without proof let us state that the UniAGENT method is sound; that is, it always finds a solution provided a solution exists. This is due to the fact, that we do constrain only agents that have been placed so far while remaining agents can be placed arbitrarily. This in theory tells that all the subgoals determined by single agent placement are fesible.

Algorithm 3. UniAGENT SAT-based CPF solving. Agents (robots) are placed to their goals one by one. Relocation of a single agent to DEXALER-ߴ its goal is solved as an individual CPF using encoding where already placed agents preserve their positions. Relatively small difference between the initial arrangement and goal in single agent relocation CPFs allows to solve them with few time layers in the reduced time expansion graph.

pair :ሻሿ൅ߙ ǡͲߙ ǡܣ ǡሻܧ ǡܸሺ ൌ ܩሾ function Solve-UniAGENT ሺȭ ൌ 1: ሽ ߤܽ ǡ ǥ ǡʹܽ ǡͳܽሼ ൌ ܣ let Ͳ ՚ šƒߟ 2: 3: do ߤ ǥǡ ͳǡʹǡ ൌ ݅ for each 4: šƒߟߙ ՚ Ͳߚ 5: do െͳ ݅ ǡ ǥ ͳǡʹǡ ൌ ݆ for each 6: ሻ ݆ܽሺ šƒߟߙ ՚ ሻ ݆ܽሺ൅ߚ 7: ሻ݅ܽሺ൅ߙ ՚ ሻ݅ܽሺ൅ߚ 8: ሻሿ൅ߚ ǡͲߚ ǡܣ ǡܩሾ ൌ ሺȰ Find-Optimal-Parameter ՚ ሻ݂ ǡߴሺ 9: ሻ݂ ǡߴ ሺȰǡ DEXALER-ߴExtract-Solution- ՚ ሻറݏ ǡߟሺ 10: do െͳ ߟ ǡ Ͳǡͳǡǥ ൌ ݇ for each 11: ሿ݇ሾറݏ ՚ ݇൅ šƒߟߙ ߟ ൅ šƒߟ ՚ šƒߟ 12: ൧ሻ šƒߟߙ ǡ ǥ ǡͳߙ ǡͲߙൣ ǡ šƒߟሺ 13: return

In our minor experiments, we found that the Ԃ-RELAXED encoding is very easy to solve if there are few time layers but it gets rapidly harder with the increasing number of time layers. The number of time layers necesssary to reach the solvability when a single agent is relocated is typically very low (usually 1 to 3 time layers). Moreover, the makespan of solutions generated by the UniAGENT solving process is similar to that of generated by solving the Ԃ-RELAXED

encoding where all the agents are relocated at once in cases where we managed to solve the Ԃ-RELAXED encoding. These observations together justifies the use of the new encoding as suggested in the UniAGENT solving process.

5 Experimental Evaluation

Series of experiments have been conducted in order to evaluate the suggested propositional Ԃ-RELAXED encoding and UniAGENT solving process based on it.

The comparison has been done with existent encodings for makespan optimal CPF solving - INVERSE, ALL-DIFFERENT, DIRECT, MATCHING, and SIMPLIFIED [Surynek, 2012a, 2012b, 2014]. To include other than SATbased methods, the comparison with A*-based OD+ID [Standley and Korf, 2011] for makespan optimal solving is also presented. Makespan suboptimal methods are represented by WHCA* [Silver, 2005] in our comparison.

We used benchmarks suggested in [Silver, 2005] which consist of randomly generated CPF instances over 4connected grids with randomly placed obstacles. There are also randomly placed obstacles by which ʹͲΨ of all the vertices are occupied. An important module in the whole solving process is a SAT solver. Glucose version 3.0 [Audemard and Simon, 2013] has been used in the experimental evaluation.

5.1 Encoding Size Comparison

The important characteristic of propositional formulae with respect to the speed of their solving is their size while small is preferable (the size is represented by the number of variables and clauses in our case).

Selected results are shown in Table 1. Size measurement is done on 4-connected grid and for various numbers of agents in the environment. For each number of agents 10 random instances were generated and average value for each characteristic is presented.

It can be observed from presented results that the ԂRELAXED encoding is the smallest in terms of the number of clauses and the second smallest in terms of the number of variables just after the MATCHING encoding. The average clause length also indicates that most of clauses are binary.

Note, that formulae for all the encodings were generated with the same number of time-layers. In most cases to time-layers fewer needs encoding DEXALER-ߴ however, achieve solvability.

1 2 4 6 8 10 12 14 16 18 20 22 24 26 28 30 32

5.2 Runtime Evaluation

Runtime tests were done over 4-connected grids with growing number of agents. The timeout has been set to 256 seconds and for each number of agents 10 random instances were solved while runtime was recorded - average runtime is presented.

Runtime results are presented in Figure 3 and Figure 4. Average optimal makespan and average sub-optimal makespan obtained with the UniAGENT and WHCA* methods are also shown. It can be observed that OD+ID and WHCA* although performing as best for small number of agents, quickly reaches the timeout as the number of agents grows. UniAGENT method scales up as the best for growing number of agents though the makespan is up to several times longer than the optimum. Up to 30 agents (occupancy ͺ͵Ψ) and up to 48 agents (occupancy of ͹ͷΨ) can be solved in 6ྶ6 and 8ྶ8 grid respectively with no obstacles within the timeout of 1.0 minute.

Motivated by experiments presented in [Standley and the by ʹሻ-puzzles െ ʹܰሺ Korf, 2011], we also tried to solve UniAGENT solver; that is, 4-connected grids with two blanks (two blanks grant that instances are solvable). In these situations, A*-based solvers relying on independence detection such as OD+ID and MGS1 do not scale well. The ሺ͵ʹ െ ʹሻ-puzzles were solved in less than 1.0 second by UniAGENT solver. The ሺͶʹ െ ʹሻ-puzzles needed approximately 10 seconds. Larger puzzles have not been solved under 1.0 minute.

We also made comparison with several domain independent planners including SAT-based makespan optimal SATPLAN [Kautz and Selman, 1999] and SASE [Huang et al., 2010] and makespan suboptimal LPG-td [Gerevini et al., 2008] and SGPLAN [Hsu et al., 2006]. Planners were run on instances over 6ྶ6 grid with 20% obstacles containing few agents - part of results is shown in Table 2. SATPLAN and SASE performed orders of magnitude worse than SAT-based solving with refered domain dependent encodings (thus not presented). Makespan suboptimal planners LPG-td and SGPLAN performed much better but still do not scale up. Moreover, they tend to generate worse makespans than the UniAGENT method.

6 Conclusions

The concept of reduced time expansion graph and this on based CPF of encoding propositional DEXALER-ߴ graph have been introduced. The search for a solution of CPF is reduced to the search of vertex disjoint paths in reduced time expansion graph which is done via SAT solving. In order to maximally reduce the size of the propositional encoding, the search for a goal arrangement is decomposed into multiple searches for sub-goals which correspond to placement of a single agent.

Experimental evaluation indicates that the novel CPF solving method - called UniAGENT solver - scales up better for higher number of agents than comparable makespan suboptimal seach-based method WHCA*. The relaxation from the requirement on the makespan optimality allowed significant runtime improvement compared to other propositional encodings and related SAT-based solving schemes. This advanced applicability of SAT-based CPF solving in higly constrained situations towards even denser occupacy with agents.

Although solutions generated by the UniAGENT method are makespan suboptimal, they are obtained through optimization of a diffrent parameter - namely the number of time layers in the Ԃ-RELAXED encoding - hence their makespan is not as dramatically far from the optimum as in the case of rule based algorithms like PUSH-AND-ROTATE [de Wilde et al., 2014]. Altogether, UniAGENT solver represents a viable alternative to existing rule and search based CPF solvers.