Showing 1–22 of 22 results for author: Surynek, P

Action Duration Generalization for Exact Multi-Agent Collective Construction

Authors: Martin Rameš, Pavel Surynek

Abstract: This paper addresses exact approaches to multi-agent collective construction problem which tasks a group of cooperative agents to build a given structure in a blocksworld under the gravity constraint. We propose a generalization of the existing exact model based on mixed integer linear programming by accommodating varying agent action durations. We refer to the model as a fraction-time model. The… ▽ More This paper addresses exact approaches to multi-agent collective construction problem which tasks a group of cooperative agents to build a given structure in a blocksworld under the gravity constraint. We propose a generalization of the existing exact model based on mixed integer linear programming by accommodating varying agent action durations. We refer to the model as a fraction-time model. The generalization by introducing action duration enables one to create a more realistic model for various domains. It provides a significant reduction of plan execution duration at the cost of increased computational time, which rises steeply the closer the model gets to the exact real-world action duration. We also propose a makespan estimation function for the fraction-time model. This can be used to estimate the construction time reduction size for the purpose of cost-benefit analysis. The fraction-time model and the makespan estimation function have been evaluated in a series of experiments using a set of benchmark structures. The results show a significant reduction of plan execution duration for non-constant duration actions due to decreasing synchronization overhead at the end of each action. According to the results, the makespan estimation function provides a reasonably accurate estimate of the makespan. △ Less

Submitted 20 December, 2023; originally announced December 2023.

Comments: 11 pages, 6 figures, ICAART 2024 extension

Multi-Agent Path Finding with Continuous Time Using SAT Modulo Linear Real Arithmetic

Authors: Tomáš Kolárik, Stefan Ratschan, Pavel Surynek

Abstract: This paper introduces a new approach to solving a continuous-time version of the multi-agent path finding problem. The algorithm translates the problem into an extension of the classical Boolean satisfiability problem, satisfiability modulo theories (SMT), that can be solved by off-the-shelf solvers. This enables the exploitation of conflict generalization techniques that such solvers can handle.… ▽ More This paper introduces a new approach to solving a continuous-time version of the multi-agent path finding problem. The algorithm translates the problem into an extension of the classical Boolean satisfiability problem, satisfiability modulo theories (SMT), that can be solved by off-the-shelf solvers. This enables the exploitation of conflict generalization techniques that such solvers can handle. Computational experiments show that the new approach scales better with respect to the available computation time than state-of-the art approaches and is usually able to avoid their exponential behavior on a class of benchmark problems modeling a typical bottleneck situation. △ Less

Submitted 15 December, 2023; v1 submitted 13 December, 2023; originally announced December 2023.

Comments: Full version of the paper

Counterexample Guided Abstraction Refinement with Non-Refined Abstractions for Multi-Agent Path Finding

Authors: Pavel Surynek

Abstract: Counterexample guided abstraction refinement (CEGAR) represents a powerful symbolic technique for various tasks such as model checking and reachability analysis. Recently, CEGAR combined with Boolean satisfiability (SAT) has been applied for multi-agent path finding (MAPF), a problem where the task is to navigate agents from their start positions to given individual goal positions so that the agen… ▽ More Counterexample guided abstraction refinement (CEGAR) represents a powerful symbolic technique for various tasks such as model checking and reachability analysis. Recently, CEGAR combined with Boolean satisfiability (SAT) has been applied for multi-agent path finding (MAPF), a problem where the task is to navigate agents from their start positions to given individual goal positions so that the agents do not collide with each other. The recent CEGAR approach used the initial abstraction of the MAPF problem where collisions between agents were omitted and were eliminated in subsequent abstraction refinements. We propose in this work a novel CEGAR-style solver for MAPF based on SAT in which some abstractions are deliberately left non-refined. This adds the necessity to post-process the answers obtained from the underlying SAT solver as these answers slightly differ from the correct MAPF solutions. Non-refining however yields order-of-magnitude smaller SAT encodings than those of the previous approach and speeds up the overall solving process making the SAT-based solver for MAPF competitive again in relevant benchmarks. △ Less

Submitted 20 January, 2023; originally announced January 2023.

Heuristically Guided Compilation for Multi-Agent Path Finding

Authors: Pavel Surynek

Abstract: Multi-agent path finding (MAPF) is a task of finding non-conflicting paths connecting agents' specified initial and goal positions in a shared environment. We focus on compilation-based solvers in which the MAPF problem is expressed in a different well established formalism such as mixed-integer linear programming (MILP), Boolean satisfiability (SAT), or constraint programming (CP). As the target… ▽ More Multi-agent path finding (MAPF) is a task of finding non-conflicting paths connecting agents' specified initial and goal positions in a shared environment. We focus on compilation-based solvers in which the MAPF problem is expressed in a different well established formalism such as mixed-integer linear programming (MILP), Boolean satisfiability (SAT), or constraint programming (CP). As the target solvers for these formalisms act as black-boxes it is challenging to integrate MAPF specific heuristics in the MAPF compilation-based solvers. We show in this work how the build a MAPF encoding for the target SAT solver in which domain specific heuristic knowledge is reflected. The heuristic knowledge is transferred to the SAT solver by selecting candidate paths for each agent and by constructing the encoding only for these candidate paths instead of constructing the encoding for all possible paths for an agent. The conducted experiments show that heuristically guided compilation outperforms the vanilla variants of the SAT-based MAPF solver. △ Less

Submitted 13 December, 2022; originally announced December 2022.

Comments: arXiv admin note: substantial text overlap with arXiv:2103.04496

Plan Execution for Multi-Agent Path Finding with Indoor Quadcopters

Authors: Matouš Kulhan, Pavel Surynek

Abstract: We study the planning and acting phase for the problem of multi-agent path finding (MAPF) in this paper. MAPF is a problem of navigating agents from their start positions to specified individual goal positions so that agents do not collide with each other. Specifically we focus on executing MAPF plans with a group of Crazyflies, small indoor quadcopters . We show how to modify the existing continu… ▽ More We study the planning and acting phase for the problem of multi-agent path finding (MAPF) in this paper. MAPF is a problem of navigating agents from their start positions to specified individual goal positions so that agents do not collide with each other. Specifically we focus on executing MAPF plans with a group of Crazyflies, small indoor quadcopters . We show how to modify the existing continuous time conflict-based search algorithm (CCBS) to produce plans that are suitable for execution with the quadcopters. The acting phase uses the the Loco positioning system to check if the plan is executed correctly. Our finding is that the CCBS algorithm allows for extensions that can produce safe plans for quadcopters, namely cylindrical protection zone around each quadcopter can be introduced at the planning level. △ Less

Submitted 6 July, 2022; v1 submitted 4 July, 2022; originally announced July 2022.

DPLL(MAPF): an Integration of Multi-Agent Path Finding and SAT Solving Technologies

Authors: Martin Čapek, Pavel Surynek

Abstract: In multi-agent path finding (MAPF), the task is to find non-conflicting paths for multiple agents from their initial positions to given individual goal positions. MAPF represents a classical artificial intelligence problem often addressed by heuristic-search. An important alternative to search-based techniques is compilation of MAPF to a different formalism such as Boolean satisfiability (SAT). Co… ▽ More In multi-agent path finding (MAPF), the task is to find non-conflicting paths for multiple agents from their initial positions to given individual goal positions. MAPF represents a classical artificial intelligence problem often addressed by heuristic-search. An important alternative to search-based techniques is compilation of MAPF to a different formalism such as Boolean satisfiability (SAT). Contemporary SAT-based approaches to MAPF regard the SAT solver as an external tool whose task is to return an assignment of all decision variables of a Boolean model of input MAPF. We present in this short paper a novel compilation scheme called DPLL(MAPF) in which the consistency checking of partial assignments of decision variables with respect to the MAPF rules is integrated directly into the SAT solver. This scheme allows for far more automated compilation where the SAT solver and the consistency checking procedure work together simultaneously to create the Boolean model and to search for its satisfying assignment. △ Less

Submitted 11 November, 2021; originally announced November 2021.

Compilation-based Solvers for Multi-Agent Path Finding: a Survey, Discussion, and Future Opportunities

Authors: Pavel Surynek

Abstract: Multi-agent path finding (MAPF) attracts considerable attention in artificial intelligence community as well as in robotics, and other fields such as warehouse logistics. The task in the standard MAPF is to find paths through which agents can navigate from their starting positions to specified individual goal positions. The combination of two additional requirements makes the problem computational… ▽ More Multi-agent path finding (MAPF) attracts considerable attention in artificial intelligence community as well as in robotics, and other fields such as warehouse logistics. The task in the standard MAPF is to find paths through which agents can navigate from their starting positions to specified individual goal positions. The combination of two additional requirements makes the problem computationally challenging: (i) agents must not collide with each other and (ii) the paths must be optimal with respect to some objective. Two major approaches to optimal MAPF solving include (1) dedicated search-based methods, which solve MAPF directly, and (2) compilation-based methods that reduce a MAPF instance to an instance in a different well established formalism, for which an efficient solver exists. The compilation-based MAPF solving can benefit from advancements accumulated during the development of the target solver often decades long. We summarize and compare contemporary compilation-based solvers for MAPF using formalisms like ASP, MIP, and SAT. We show the lessons learned from past developments and current trends in the topic and discuss its wider impact. △ Less

Submitted 23 April, 2021; originally announced April 2021.

Sparsification for Fast Optimal Multi-Robot Path Planning in Lazy Compilation Schemes

Authors: Pavel Surynek

Abstract: 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 di… ▽ More 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. △ Less

Submitted 7 March, 2021; originally announced March 2021.

Multi-Goal Multi-Agent Path Finding via Decoupled and Integrated Goal Vertex Ordering

Authors: Pavel Surynek

Abstract: We introduce multi-goal multi agent path finding (MAPF$^{MG}$) which generalizes the standard discrete multi-agent path finding (MAPF) problem. While the task in MAPF is to navigate agents in an undirected graph from their starting vertices to one individual goal vertex per agent, MAPF$^{MG}$ assigns each agent multiple goal vertices and the task is to visit each of them at least once. Solving MAP… ▽ More We introduce multi-goal multi agent path finding (MAPF$^{MG}$) which generalizes the standard discrete multi-agent path finding (MAPF) problem. While the task in MAPF is to navigate agents in an undirected graph from their starting vertices to one individual goal vertex per agent, MAPF$^{MG}$ assigns each agent multiple goal vertices and the task is to visit each of them at least once. Solving MAPF$^{MG}$ not only requires finding collision free paths for individual agents but also determining the order of visiting agent's goal vertices so that common objectives like the sum-of-costs are optimized. We suggest two novel algorithms using different paradigms to address MAPF$^{MG}$: a heuristic search-based search algorithm called Hamiltonian-CBS (HCBS) and a compilation-based algorithm built using the SMT paradigm, called SMT-Hamiltonian-CBS (SMT-HCBS). Experimental comparison suggests limitations of compilation-based approach. △ Less

Submitted 10 September, 2020; originally announced September 2020.

At-Most-One Constraints in Efficient Representations of Mutex Networks

Authors: Pavel Surynek

Abstract: The At-Most-One (AMO) constraint is a special case of cardinality constraint that requires at most one variable from a set of Boolean variables to be set to TRUE. AMO is important for modeling problems as Boolean satisfiability (SAT) from domains where decision variables represent spatial or temporal placements of some objects that cannot share the same spatial or temporal slot. The AMO constraint… ▽ More The At-Most-One (AMO) constraint is a special case of cardinality constraint that requires at most one variable from a set of Boolean variables to be set to TRUE. AMO is important for modeling problems as Boolean satisfiability (SAT) from domains where decision variables represent spatial or temporal placements of some objects that cannot share the same spatial or temporal slot. The AMO constraint can be used for more efficient representation and problem solving in mutex networks consisting of pair-wise mutual exclusions forbidding pairs of Boolean variable to be simultaneously TRUE. An on-line method for automated detection of cliques for efficient representation of incremental mutex networks where new mutexes arrive using AMOs is presented. A comparison of SAT-based problem solving in mutex networks represented by AMO constraints using various encodings is shown. △ Less

Submitted 10 June, 2020; originally announced June 2020.

Pushing the Envelope: From Discrete to Continuous Movements in Multi-Agent Path Finding via Lazy Encodings

Authors: Pavel Surynek

Abstract: Multi-agent path finding in continuous space and time with geometric agents MAPF$^\mathcal{R}$ is addressed in this paper. The task is to navigate agents that move smoothly between predefined positions to their individual goals so that they do not collide. We introduce a novel solving approach for obtaining makespan optimal solutions called SMT-CBS$^\mathcal{R}$ based on {\em satisfiability modulo… ▽ More Multi-agent path finding in continuous space and time with geometric agents MAPF$^\mathcal{R}$ is addressed in this paper. The task is to navigate agents that move smoothly between predefined positions to their individual goals so that they do not collide. We introduce a novel solving approach for obtaining makespan optimal solutions called SMT-CBS$^\mathcal{R}$ based on {\em satisfiability modulo theories} (SMT). The new algorithm combines collision resolution known from conflict-based search (CBS) with previous generation of incomplete SAT encodings on top of a novel scheme for selecting decision variables in a potentially uncountable search space. We experimentally compare SMT-CBS$^\mathcal{R}$ and previous CCBS algorithm for MAPF$^\mathcal{R}$. △ Less

Submitted 25 April, 2020; originally announced April 2020.

Comments: arXiv admin note: text overlap with arXiv:1903.09820

Multi-Agent Path Finding with Capacity Constraints

Authors: Pavel Surynek, T. K. Satish Kumar, Sven Koenig

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 age… ▽ More 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. △ Less

Submitted 21 July, 2019; originally announced July 2019.

Comments: arXiv admin note: substantial text overlap with arXiv:1809.05959 and arXiv:1907.07631

On the Tour Towards DPLL(MAPF) and Beyond

Authors: Pavel Surynek

Abstract: We discuss milestones on the tour towards DPLL(MAPF), a multi-agent path finding (MAPF) solver fully integrated with the Davis-Putnam-Logemann-Loveland (DPLL) propositional satisfiability testing algorithm through satisfiability modulo theories (SMT). The task in MAPF is to navigate agents in an undirected graph in a non-colliding way so that each agent eventually reaches its unique goal vertex. A… ▽ More We discuss milestones on the tour towards DPLL(MAPF), a multi-agent path finding (MAPF) solver fully integrated with the Davis-Putnam-Logemann-Loveland (DPLL) propositional satisfiability testing algorithm through satisfiability modulo theories (SMT). The task in MAPF is to navigate agents in an undirected graph in a non-colliding way so that each agent eventually reaches its unique goal vertex. At most one agent can reside in a vertex at a time. Agents can move instantaneously by traversing edges provided the movement does not result in a collision. Recently attempts to solve MAPF optimally w.r.t. the sum-of-costs or the makespan based on the reduction of MAPF to propositional satisfiability (SAT) have appeared. The most successful methods rely on building the propositional encoding for the given MAPF instance lazily by a process inspired in the SMT paradigm. The integration of satisfiability testing by the SAT solver and the high-level construction of the encoding is however relatively loose in existing methods. Therefore the ultimate goal of research in this direction is to build the DPLL(MAPF) algorithm, a MAPF solver where the construction of the encoding is fully integrated with the underlying SAT solver. We discuss the current state-of-the-art in MAPF solving and what steps need to be done to get DPLL(MAPF). The advantages of DPLL(MAPF) in terms of its potential to be alternatively parametrized with MAPF$^R$, a theory of continuous MAPF with geometric agents, are also discussed. △ Less

Submitted 11 July, 2019; originally announced July 2019.

Comments: arXiv admin note: substantial text overlap with arXiv:1809.05959

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

Authors: Pavel Surynek

Abstract: 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 t… ▽ More 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. △ Less

Submitted 23 March, 2019; originally announced March 2019.

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

Authors: Pavel Surynek

Abstract: 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… ▽ More 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. △ Less

Submitted 27 December, 2018; originally announced December 2018.

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

Authors: Pavel Surynek

Abstract: 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 f… ▽ More 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 swap** (TSWAP). In this formulation we express two new types of relocation problems derived from token swap** 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. △ Less

Submitted 16 September, 2018; originally announced September 2018.

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

Authors: Pavel Surynek

Abstract: We study practical approaches to solving the token swap** (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… ▽ More We study practical approaches to solving the token swap** (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. △ Less

Submitted 25 June, 2018; originally announced June 2018.

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

Authors: Marika Ivanová, Pavel Surynek, Diep Thi Ngoc Nguyen

Abstract: 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 ver… ▽ More 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. △ Less

Submitted 4 September, 2017; originally announced September 2017.

Comments: arXiv admin note: substantial text overlap with arXiv:1708.07285

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

Authors: Marika Ivanová, Pavel Surynek

Abstract: 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 - att… ▽ More 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. △ Less

Submitted 24 August, 2017; originally announced August 2017.

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

Authors: Pavel Surynek, Ariel Felner, Roni Stern, Eli Boyarski

Abstract: 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… ▽ More 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. △ Less

Submitted 1 July, 2017; originally announced July 2017.

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

Authors: Pavel Surynek

Abstract: 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 o… ▽ More 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). △ Less

Submitted 18 October, 2016; originally announced October 2016.

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

Authors: Pavel Surynek, Petr Michalík

Abstract: 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. T… ▽ More 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 grou** 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. △ Less

Submitted 16 October, 2016; originally announced October 2016.