arXiv subjects

Pavel Surynek

Publications and source records attributed to Pavel Surynek.

27 records · Page 2Linked to original sources

arXiv2019

Multi-agent Path Finding with Continuous Time Viewed Through Satisfiability Modulo Theories (SMT)

This paper addresses a variant of multi-agent path finding (MAPF) in continuous space and time. We present a new solving approach based on satisfiability modulo theories (SMT) to obtain makespan optimal solutions. The standard MAPF is a task of navigating agents in an undirected graph from given starting vertices to given goal vertices so that agents do not collide with each other in vertices of the graph. In the continuous version (MAPF$^\mathcal{R}$) agents move in an $n$-dimensional Euclidean space along straight lines that interconnect predefined positions. For simplicity, we work with circular omni-directional agents having constant velocities in the 2D plane. As agents can have different sizes and move smoothly along lines, a non-colliding movement along certain lines with small agents can result in a collision if the same movement is performed with larger agents. Our SMT-based approach for MAPF$^\mathcal{R}$ called SMT-CBS$^\mathcal{R}$ reformulates the Conflict-based Search (CBS) algorithm in terms of SMT concepts. We suggest lazy generation of decision variables and constraints. Each time a new conflict is discovered, the underlying encoding is extended with new variables and constraints to eliminate the conflict. We compared SMT-CBS$^\mathcal{R}$ and adaptations of CBS for the continuous variant of MAPF experimentally.

cs.AI↗

arXiv2018

A Summary of Adaptation of Techniques from Search-based Optimal Multi-Agent Path Finding Solvers to Compilation-based Approach

In the multi-agent path finding problem (MAPF) we are given a set of agents each with respective start and goal positions. The task is to find paths for all agents while avoiding collisions aiming to minimize an objective function. Two such common objective functions is the sum-of-costs and the makespan. Many optimal solvers were introduced in the past decade - two prominent categories of solvers can be distinguished: search-based solvers and compilation-based solvers. Search-based solvers were developed and tested for the sum-of-costs objective while the most prominent compilation-based solvers that are built around Boolean satisfiability (SAT) were designed for the makespan objective. Very little was known on the performance and relevance of the compilation-based approach on the sum-of-costs objective. In this paper we show how to close the gap between these cost functions in the compilation-based approach. Moreover we study applicability of various techniques developed for search-based solvers in the compilation-based approach. A part of this paper introduces a SAT-solver that is directly aimed to solve the sum-of-costs objective function. Using both a lower bound on the sum-of-costs and an upper bound on the makespan, we are able to have a reasonable number of variables in our SAT encoding. We then further improve the encoding by borrowing ideas from ICTS, a search-based solver. Experimental evaluation on several domains show that there are many scenarios where our new SAT-based methods outperforms the best variants of previous sum-of-costs search solvers - the ICTS, CBS algorithms, and ICBS algorithms.

cs.AI↗

arXiv2018

Lazy Modeling of Variants of Token Swapping Problem and Multi-agent Path Finding through Combination of Satisfiability Modulo Theories and Conflict-based Search

We address item relocation problems in graphs in this paper. We assume items placed in vertices of an undirected graph with at most one item per vertex. Items can be moved across edges while various constraints depending on the type of relocation problem must be satisfied. We introduce a general problem formulation that encompasses known types of item relocation problems such as multi-agent path finding (MAPF) and token swapping (TSWAP). In this formulation we express two new types of relocation problems derived from token swapping that we call token rotation (TROT) and token permutation (TPERM). Our solving approach for item relocation combines satisfiability modulo theory (SMT) with conflict-based search (CBS). We interpret CBS in the SMT framework where we start with the basic model and refine the model with a collision resolution constraint whenever a collision between items occurs in the current solution. The key difference between the standard CBS and our SMT-based modification of CBS (SMT-CBS) is that the standard CBS branches the search to resolve the collision while in SMT-CBS we iteratively add a single disjunctive collision resolution constraint. Experimental evaluation on several benchmarks shows that the SMT-CBS algorithm significantly outperforms the standard CBS. We also compared SMT-CBS with a modification of the SAT-based MDD-SAT solver that uses an eager modeling of item relocation in which all potential collisions are eliminated by constrains in advance. Experiments show that lazy approach in SMT-CBS produce fewer constraint than MDD-SAT and also achieves faster solving run-times.

cs.AI↗

arXiv2018

Finding Optimal Solutions to Token Swapping by Conflict-based Search and Reduction to SAT

We study practical approaches to solving the token swapping (TSWAP) problem optimally in this short paper. In TSWAP, we are given an undirected graph with colored vertices. A colored token is placed in each vertex. A pair of tokens can be swapped between adjacent vertices. The goal is to perform a sequence of swaps so that token and vertex colors agree across the graph. The minimum number of swaps is required in the optimization variant of the problem. We observed similarities between the TSWAP problem and multi-agent path finding (MAPF) where instead of tokens we have multiple agents that need to be moved from their current vertices to given unique target vertices. The difference between both problems consists in local conditions that state transitions (swaps/moves) must satisfy. We developed two algorithms for solving TSWAP optimally by adapting two different approaches to MAPF - CBS and MDD- SAT. This constitutes the first attempt to design optimal solving algorithms for TSWAP. Experimental evaluation on various types of graphs shows that the reduction to SAT scales better than CBS in optimal TSWAP solving.

cs.AI↗

arXiv2017

Maintaining Ad-Hoc Communication Network in Area Protection Scenarios with Adversarial Agents

We address a problem of area protection in graph-based scenarios with multiple mobile agents where connectivity is maintained among agents to ensure they can communicate. The problem consists of two adversarial teams of agents that move in an undirected graph shared by both teams. Agents are placed in vertices of the graph; at most one agent can occupy a vertex; and they can move into adjacent vertices in a conflict free way. Teams have asymmetric goals: the aim of one team - attackers - is to invade into given area while the aim of the opponent team - defenders - is to protect the area from being entered by attackers by occupying selected vertices. The team of defenders need to maintain connectivity of vertices occupied by its own agents in a visibility graph. The visibility graph models possibility of communication between pairs of vertices. We study strategies for allocating vertices to be occupied by the team of defenders to block attacking agents where connectivity is maintained at the same time. To do this we reserve a subset of defending agents that do not try to block the attackers but instead are placed to support connectivity of the team. The performance of strategies is tested in multiple benchmarks. The success of a strategy is heavily dependent on the type of the instance, and so one of the contributions of this work is that we identify suitable strategies for diverse instance types.

cs.MA↗

arXiv2017

Area Protection in Adversarial Path-Finding Scenarios with Multiple Mobile Agents on Graphs: a theoretical and experimental study of target-allocation strategies for defense coordination

We address a problem of area protection in graph-based scenarios with multiple agents. The problem consists of two adversarial teams of agents that move in an undirected graph shared by both teams. Agents are placed in vertices of the graph; at most one agent can occupy a vertex; and they can move into adjacent vertices in a conflict free way. Teams have asymmetric goals: the aim of one team - attackers - is to invade into given area while the aim of the opponent team - defenders - is to protect the area from being entered by attackers by occupying selected vertices. We study strategies for allocating vertices to be occupied by the team of defenders to block attacking agents. We show that the decision version of the problem of area protection is PSPACE-hard under the assumption that agents can allocate their target vertices multiple times. Further we develop various on-line vertex-allocation strategies for the defender team in a simplified variant of the problem with single stage vertex allocation and evaluated their performance in multiple benchmarks. The success of a strategy is heavily dependent on the type of the instance, and so one of the contributions of this work is that we identify suitable vertex-allocation strategies for diverse instance types. In particular, we introduce a simulation-based method that identifies and tries to capture bottlenecks in the graph, that are frequently used by the attackers. Our experimental evaluation suggests that this method often allows a successful defense even in instances where the attackers significantly outnumber the defenders.

cs.AI↗

arXiv2017

Modifying Optimal SAT-based Approach to Multi-agent Path-finding Problem to Suboptimal Variants

In multi-agent path finding (MAPF) the task is to find non-conflicting paths for multiple agents. In this paper we focus on finding suboptimal solutions for MAPF for the sum-of-costs variant. Recently, a SAT-based approached was developed to solve this problem and proved beneficial in many cases when compared to other search-based solvers. In this paper, we present SAT-based unbounded- and bounded-suboptimal algorithms and compare them to relevant algorithms. Experimental results show that in many case the SAT-based solver significantly outperforms the search-based solvers.

cs.AI↗

arXiv2016

Makespan Optimal Solving of Cooperative Path-Finding via Reductions to Propositional Satisfiability

The problem of makespan optimal solving of cooperative path finding (CPF) is addressed in this paper. The task in CPF is to relocate a group of agents in a non-colliding way so that each agent eventually reaches its goal location from the given initial location. The abstraction adopted in this work assumes that agents are discrete items moving in an undirected graph by traversing edges. Makespan optimal solving of CPF means to generate solutions that are as short as possi-ble in terms of the total number of time steps required for the execution of the solution. We show that reducing CPF to propositional satisfiability (SAT) represents a viable option for obtaining makespan optimal solutions. Several encodings of CPF into propositional formulae are suggested and experimentally evaluated. The evaluation indicates that SAT based CPF solving outperforms other makespan optimal methods significantly in highly constrained situations (environments that are densely occupied by agents).

cs.AI↗

arXiv2016

Improvements in Sub-optimal Solving of the $(N^2-1)$-Puzzle via Joint Relocation of Pebbles and its Applications to Rule-based Cooperative Path-Finding

The problem of solving $(n^2-1)$-puzzle and cooperative path-finding (CPF) sub-optimally by rule based algorithms is addressed in this manuscript. The task in the puzzle is to rearrange $n^2-1$ pebbles on the square grid of the size of n x n using one vacant position to a desired goal configuration. An improvement to the existent polynomial-time algorithm is proposed and experimentally analyzed. The improved algorithm is trying to move pebbles in a more efficient way than the original algorithm by grouping them into so-called snakes and moving them jointly within the snake. An experimental evaluation showed that the algorithm using snakes produces solutions that are 8% to 9% shorter than solutions generated by the original algorithm. The snake-based relocation has been also integrated into rule-based algorithms for solving the CPF problem sub-optimally, which is a closely related task. The task in CPF is to relocate a group of abstract robots that move over an undirected graph to given goal vertices. Robots can move to unoccupied neighboring vertices and at most one robot can be placed in each vertex. The $(n^2-1)$-puzzle is a special case of CPF where the underlying graph is represented by a 4-connected grid and there is only one vacant vertex. Two major rule-based algorithms for CPF were included in our study - BIBOX and PUSH-and-SWAP (PUSH-and-ROTATE). Improvements gained by using snakes in the BIBOX algorithm were stable around 30% in $(n^2-1)$-puzzle solving and up to 50% in CPFs over bi-connected graphs with various ear decompositions and multiple vacant vertices. In the case of the PUSH-and-SWAP algorithm the improvement achieved by snakes was around 5% to 8%. However, the improvement was unstable and hardly predictable in the case of PUSH-and-SWAP.

cs.AI↗