prof. RNDr. Pavel Surynek, Ph.D.

Stať ve sborníku

10.5220/0012385600003636

Katedra aplikované matematiky

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 introduction of action durations 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 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 st ructures. 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.

Článek

10.1007/s42979-022-01437-x

Katedra aplikované matematiky

We address the problem of evacuation from the perspective of agent-based modeling (ABM) in this paper. The evacuation problem is modeled as a navigation of multiple agents that spatially interact with each other in a known environment. The environment is divided into a danger and a safe zone while the task of agents is to move from the danger zone to the safe one in a collision-free manner. Unlike previous approaches that model the environment as a discrete graph with agents placed in its vertices, at most one agent per vertex, our approach adopts various continuous aspects such as a grid-based embedding of the environment into 2D space and continuous line of sight of agents. In addition to this, we adopt hierarchical structure of multi-agent system in which so called leading agents are more informed having full knowledge of other agents and are capable of performing multi-agent pathfinding (MAPF) via centralized algorithms like conflict-based search (CBS) while so called follower agents with limited knowledge about other agents are modeled using simple local rules. Our experimental evaluation indicates that suggested hierarchical modeling approach can serve as a tool for studying the progress and the efficiency of evacuation processes in different environments.

Stať ve sborníku

10.5220/0011693900003393

Katedra aplikované matematiky

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.

Stať ve sborníku

10.1109/IROS55552.2023.10341952

Katedra aplikované matematiky

We address the problem of multi-goal multi robot path planning (MG-MRPP) via counterexample guided abstraction refinement (CEGAR) framework. MG-MRPP generalizes the standard discrete multi-robot path planning (MRPP) problem. While the task in MRPP is to navigate robots in an undirected graph from their starting vertices to one individual goal vertex per robot, MG-MRPP assigns each robot multiple goal vertices and the task is to visit each of them at least once. Solving MG-MRPP not only requires finding collision free paths for individual robots but also determining the order of visiting robot's goal vertices so that common objectives like the sum-of-costs are optimized. We use the Boolean satisfiability (SAT) techniques as the underlying paradigm. A specifically novel in this work is the use of non-refined abstractions when formulating the MG-MRPP problem as SAT. While the standard CEGAR approach for MG-MRPP does not encode collision elimination constraints in the initial abstraction and leave them to subsequent refinements. The novel CEGAR approach leaves some abstractions deliberately 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 MG-MRPP solutions. Non-refining however yields order-of-magnitude smaller SAT encodings than those of the previous CEGAR approach and speeds up the overall solving process.

Stať ve sborníku

10.1007/978-3-031-37616-0_34

Katedra aplikované matematiky

We study the planning-acting loop for the multi-agent path finding problem (MAPF). 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. We focus on executing MAPF plans with a group of Crazyflies, small indoor quadcopters, for which we developed a platform that integrates decision theoretic planning and plan execution modules. Our platform can be used for testing suitability of variants of MAPF for execution with real agents. 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. 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.

Stať ve sborníku

10.5220/0012188200003543

Katedra aplikované matematiky

We study the planning-acting loop for multi-agent path finding with continuous time (MAPF R ). The standard 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. The standard MAPF takes place in a discrete graph with agents located in its vertices and instantaneous moves of agents across edges. MAPFR adds continuous elements to MAPF via allowing agents to wait in a vertex for arbitrary length of time to avoid the collision. We focus in this paper on executing MAPFR plans with a group of Crazyflies, small indoor quadcopters. We show how to modify the existing continuous-time conflict-based search algorithm (CCBS) for MAPF R to produce plans that are suitable for execution with the quadcopters. Our platform can be used for testing suitability of variants of MAPF for execution with real agents. Our finding is that the MAPF variant with continuous time and the related CCBS algorithm allows f or extensions that can produce safe plans for quadcopters, namely cylindrical protection zone around each quadcopter can be introduced at the planning level.

Stať ve sborníku

10.1109/ICTAI59109.2023.00055

Katedra aplikované matematiky

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.

Stať ve sborníku

10.5220/0012206800003543

Katedra aplikované matematiky

We focus on rule-based algorithms for multi-agent path finding (MAPF) in this paper. MAPF is a task of finding non-conflicting paths connecting agents’ specified initial and goal positions in a shared environment specified via an undirected graph. Rule-based algorithms use a fixed set of predefined primitives to move agents to their goal positions in a complete manner. We propose to apply spectral clustering on the underlying graph to decompose the graph into highly connected component and move agents to their goal cluster first before the rule-based algorithm is applied. The benefit of this approach is twofold: (1) the algorithms are often more efficient on highly connected clusters and (2) we can potentially run the algorithms in parallel on individual clusters.

Stať ve sborníku

10.1609/socs.v15i1.21790

Katedra aplikované matematiky

We address the problem of evacuation from the heuristic search perspective combined with agent-based modeling (ABM). The evacuation problem is modeled as a navigation of multiple agents in a known environment. The environment is divided into a danger and a safe zone while the task of agents is to move from the danger zone to the safe zone in a collision-free manner. Unlike previous approaches that model the environment as a discrete graph with agents placed in its vertices, at most one agent per vertex, our approach adopts various continuous aspects such as a grid-based embedding of the environment into 2D space and continuous line of sight of agents. In addition to this, we adopt hierarchical structure of our multi-agent system in which so called leading agents are more informed and are capable of performing multi-agent pathfinding (MAPF) via centralized algorithms like conflict-based search (CBS) while so called following agents with limited knowledge about other agents are modeled using simple local rules. Our experimental evaluation indicates that suggested hierarchical modeling approach can serve as a tool for studying the progress and the efficiency of evacuation processes in different environments.

Stať ve sborníku

10.1007/978-3-031-22953-4_8

Katedra aplikované matematiky

We address the problem of variable and truth-value choice in modern search-based Boolean satisfiability (SAT) solvers depending on the problem domain. The SAT problem is the task to determine truth-value assignment for variables of a given Boolean formula under which the formula evaluates to true. The SAT problem is often used as a canonical representation of combinatorial problems in many domains of computer science ranging from artificial intelligence to software engineering. Modern complete search-based SAT solvers represent a universal problem solving tool which often provide higher efficiency than ad-hoc direct solving approaches. Many efficient variable and truth-value selection heuristics were devised. Heuristics can usually be fine tuned by single or multiple numerical parameters prior to executing the search process over the concrete SAT instance. In this paper we present a machine learning approach that predicts the parameters of heuristic from the underlying structure of a graph derived from the input SAT instance. Using this approach we effectively fine tune the SAT solver for specific problem domain.

Stať ve sborníku

10.5220/0010845200003116

Katedra aplikované matematiky

Orchestrating warehouse sorting robots each transporting a single package from the conveyor belt to its destination is a NP-hard problem, often modeled Multi-agent path-finding (MAPF) where the environment is represented as a graph and robots as agents in vertices of the graph. However, in order to maintain the speed of operations in such a setup, sorting robots must be given a route to follow almost at the moment they obtain the package, so there is no time to perform difficult offline planning. Hence in this work, we are inspired by the approach of enriching conflict-based search (CBS) optimal MAPF algorithm by so-called highways that increase the speed of planning towards on-line operations. We investigate whether adding highways to the underlying graph will be enough to enforce global behaviour of a large number of robots that are controlled locally. If we succeed, the slow global planning step could be omitted without significant loss of performance.

Stať ve sborníku

10.1609/socs.v15i1.21782

Katedra aplikované matematiky

Classical planning is a task of finding a sequence of actions that achieve a given goal. One of many approaches to classical planning is compilation into propositional satisfiability (SAT). In this work, we propose a new method that uses lazy compilation into SAT. Different from the standard compilation method, lazy compilation constructs the target propositional formula step by step while the SAT solver is consulted at each step and refinements of the formula are suggested according to SAT solver's answers. The performed experiments pointed out that lazy compilation has the potential to improve the performance of the planners.

Článek

10.1613/jair.1.13318

Katedra aplikované matematiky

In the multi-agent path finding problem (MAPF) we are given a set of agents each with re- spective start and goal positions. The task is to find paths for all agents while avoiding collisions, aiming to minimize a given objective function. Many MAPF solvers were introduced in the past decade for optimizing two specific objective functions: sum-of-costs and makespan. 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 is known on the performance and relevance of solvers from the compilation-based approach on the sum-of-costs objective. In this paper, we start to close the gap between these cost functions in the compilation-based approach.

Článek

10.1016/j.artint.2022.103766

Katedra aplikované matematiky

Mutex propagation is a form of efficient constraint propagation popularly used in AI planning to tightly approximate the reachable states from a given state. We utilize this idea in the context of Multi-Agent Path Finding (MAPF). When adapted to MAPF, mutex propagation provides stronger constraints for conflict resolution in CBS, a popular optimal search-based MAPF algorithm, as well as in MDD-SAT, an optimal satisfiability-based MAPF algorithm. Mutex propagation provides CBS with the ability to break symmetries in MAPF and provides MDD-SAT with the ability to make stronger inferences than unit propagation. While existing work identifies a limited form of symmetries and requires the manual design of symmetry-breaking constraints, mutex propagation is more general and allows for the automated design of symmetry-breaking constraints. Our experimental results show that CBS with mutex propagation is capable of outperforming CBSH-RCT, a state-of-the-art variant of CBS, with respect to the success rate. We also show that MDD-SAT with mutex propagation often performs better than MDD-SAT with respect to the success rate.

Článek

10.1016/j.artint.2022.103662

Katedra aplikované matematiky

Multi-Agent Pathfinding (MAPF) is the problem of finding paths for multiple agents such that each agent reaches its goal and the agents do not collide. In recent years, variants of MAPF have risen in a wide range of real-world applications such as warehouse management and autonomous vehicles. Optimizing common MAPF objectives, such as minimizing sum-of-costs or makespan, is computationally intractable, but state-of-the-art algorithms are able to solve optimally problems with dozens of agents. However, most MAPF algorithms assume that (1) time is discretized into time steps and (2) the duration of every action is one time step. These simplifying assumptions limit the applicability of MAPF algorithms in real-world applications and raise non-trivial questions such as how to discretize time in an effective manner. We propose two novel MAPF algorithms for finding optimal solutions that do not rely on any time discretization.

Stať ve sborníku

Katedra aplikované matematiky

Boolean satisfiability (SAT) solvers are essential tools for many domains in computer science and engineering. Modern complete search-based SAT solvers represent a universal problem solving tool which often provide higher efficiency than ad-hoc direct solving approaches. Over the course of at least two decades of SAT related research, many variable and value selection heuristics were devised. Heuristics can usually be tuned by single or multiple numerical parameters prior to executing the search process over the concrete SAT instance. In this paper we present a machine learning approach that predicts the parameters of heuristic from the underlying structure of the input SAT instance.

Stať ve sborníku

10.24963/ijcai.2022/783

Katedra aplikované matematiky

Multi-agent path finding (MAPF) attracts considerable attention in artificial intelligence community. The task in the standard MAPF is to find discrete paths through which agents can navigate from their starting positions to individual goal positions. The combination of two additional requirements makes the problem computationally challenging: agents must not collide with each other and the paths must be optimal with respect to some objective. Two major approaches to optimal MAPF solving include dedicated search-based methods, and compilation-based methods that reduce a MAPF instance to an instance in a different formalism, for which an efficient solver exists. In this survey, we summarize major compilation-based solvers for MAPF using CSP, SAT, and MILP formalisms. We explain the core ideas of the solvers in a simplified and unified way while preserving the merit making them more accessible for a wider audience.

Stať ve sborníku

10.1609/socs.v15i1.21798

Katedra aplikované matematiky

Multi-agent path finding (MAPF) represents a task of finding non-colliding paths for agents via which they can navigate from their initial positions to specified goal positions. Contemporary optimal solving algorithms include dedicated search-based methods, that solve the problem directly, and compilation-based algorithms that reduce MAPF to a different formalism for which an efficient solver exists. In this paper, we enhance the existing Boolean satisfiability-based (SAT) algorithm for MAPF via using sparse decision diagrams representing the set of candidate paths for each agent, from which the target Boolean encoding is derived, considering more promising paths before the less promising ones are taken into account. Suggested sparse diagrams lead to a smaller target Boolean formulae that can be constructed and solved faster while optimality guarantees of the approach are kept. Specifically, considering the candidate paths sparsely instead of considering them all makes the SAT-based approach more competitive for MAPF on large maps.

Stať ve sborníku

10.1109/ICTAI52525.2021.00078

Katedra aplikované matematiky

Adversarial Multi-Agent Path Finding (AMAPF) extends the standard discrete Multi-Agent Path Finding with an adversarial element. Agents of two competing teams are deployed in a shared environment represented by an undirected graph. The first team aims to navigate all its agents from their initial locations to given goal locations, while the second team aims to prevent agents of the first team from fulfilling their goal. We prove that the problem of finding a winning strategy is EXPTIME-complete.

Stať ve sborníku

Katedra aplikované matematiky

The task in multi-agent path finding (MAPF) is to find paths through which agents can navigate from their starting posi- tions to given individual goal positions. The combination of two additional requirements makes the problem challenging: (i) agents must not collide with each other and (ii) the paths must be optimal with respect to some objective. We summa- rize and compare main ideas of contemporary compilation- based solvers for MAPF using MIP and SAT formalisms.

Stať ve sborníku

10.1007/978-3-030-71158-0_19

Katedra aplikované matematiky

We address multi-agent path finding (MAPF) with continuous movements and geometric agents, i.e. agents of various geometric shapes moving smoothly between predefined positions. We analyze a new solving approach based on satisfiability modulo theories (SMT) that is designed to obtain optimal solutions with respect to common cumulative objectives. 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 or edges of the graph. In the continuous version (MAPF(R)), agents move in an n-dimensional Euclidean space along straight lines that interconnect predefined positions. Agents themselves are geometric objects of various shapes occupying certain volume of the space - circles, polygons, etc. We develop concepts for circular omni-directional agents having constant velocities in the 2D plane but a generalization for different shapes is possible. As agents can have different shapes/sizes and are moving smoothly along lines, a movement along certain lines done with small agents can be non-colliding while the same movement may result in a collision if performed with larger agents. Such a distinction rooted in the geometric reasoning is not present in the standard MAPF. The SMT-based approach for MAPF(R) called SMT-CBSR reformulates previous Conflict-based Search (CBS) algorithm in terms of SMT. Lazy generation of constraints is the key idea behind the previous algorithm SMT-CBS. Each time a new conflict is discovered, the underlying encoding is extended with new to eliminate the conflict. SMT-CBSR significantly extends this idea by generating also the decision variables lazily. Generating variables on demand is needed because in the continuous case the number of possible decision variables is potentially uncountable hence cannot be generated in advance as in the case of SMT-CBS. We compared SMT-CBSR and adaptations of CBS for the continuous variant of M

Stať ve sborníku

Katedra teoretické informatiky
Katedra aplikované matematiky

The task in multi-agent path finding (MAPF) is to find non- conflicting paths connecting agents’ start and goal positions. The MAPF problem is often compiled to Boolean satisfia- bility (SAT) and solved by existing SAT solvers. Contem- porary compilation approaches of MAPF to SAT regard the SAT solver as an external tool whose task is to return an as- signment of all decision variables of a Boolean model of the input MAPF instance. We present in this paper a novel compi- lation scheme called DPLL(MAPF) in which the consistency checking of partial assignments of decision variables with re- spect to the MAPF rules is integrated directly into the SAT solver. This scheme allows for far more automated compila- tion where the SAT solver and the consistency checking pro- cedure work together simultaneously to create the Boolean model and to search for its satisfying assignment.

Stať ve sborníku

Katedra aplikované matematiky

We present ESO-MAPF, a research and educational platform for experimenting with multi-agent path finding (MAPF). ESO-MAPF focuses on demonstrating the planning-acting chain in the MAPF domain. MAPF is the task of finding collision free paths for agents from their starting positions to given individual goals. The standard MAPF uses the abstraction where agents move in an undirected graph via traversing its edges in discrete steps. The discrete abstraction simplifies the planning phase however resulting discrete plans often need to be executed in the real continuous environment. ESO-MAPF shows how to bridge discrete planning and the acting phase in which the resulting plans are executed on physical robots. We simulate centralized plans on a group of OZOBOT Evo robots using their reflex functionalities and outputs on the surface of the screen that serves as the environment. Various problems arising along the planning-acting chain are illustrated to emphasize the educational point of view.

Stať ve sborníku

10.5220/0010678200003064

Katedra aplikované matematiky

The problem of evacuation is addressed from the perspective of agent-based modeling (ABM) in this paper. We study evacuation as a problem of navigation of multiple agents in a known environment. The environment is divided into a danger and a safe zone while the task of agents is to move from the danger zone to the safe one. Unlike previous approaches that model the environment as a discrete graph with agents placed in its vertices our approach adopts various continuous aspects such as grid-based embedding of the environment into 2D space continuous line of sight of an agent. In addition to this, we adopt hierarchical structure of multi-agent system in which so called leading agents are more informed and are capable of performing multiagent pathfinding (MAPF) via centralized algorithms like conflict-based search (CBS) while so called follower agents are modeled using simple local rules. Our experimental evaluation indicates that suggested modeling approach can serve as a tool for studying the progress and the efficiency of the evacuation process.

Stať ve sborníku

Katedra aplikované matematiky

We introduce multi-goal multi agent path finding (MG-MAPF) 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, MG-MAPF assigns each agent multiple goal vertices and the task is to visit each of them at least once. Solving MG-MAPF 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 MG-MAPF: a heuristic search-based algorithm called Hamiltonian-CBS (HCBS) and a compilation-based algorithm built using the satisfiability modulo theories (SMT), called SMT-Hamiltonian-CBS (SMT-HCBS).

Stať ve sborníku

Katedra aplikované matematiky

We introduce multi-goal multi agent path finding (MG- MAPF) 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, MG-MAPF assigns each agent multiple goal vertices and the task is to visit each of them at least once.

Stať ve sborníku

10.1109/ICTAI52525.2021.00021

Katedra aplikované matematiky

Multi-robot path planning (MRPP) is the task of finding non-conflicting paths for robots via which they can navigate themselves to specified individual goal positions. MRPP uses an undirected graph to represent a shared environment in which the robots move instantaneously between vertices in discrete time steps. Such discrete formulation enables relatively simple algorithms, often based on multi-valued decision diagrams (MDDs) that represent possible paths for each robot, but results in an inaccurate modeling of the real robotic task. Recently introduced continuous variant of MRPP assumes fixed trajectories for robots and fully continuous time but is more difficult to be addressed algorithmically. The set of possible paths for individual robots in the continuous variant can be represented in real-time decision diagram (RDD) which however is often too large. An improvement of RDDs based on sparsification that includes paths into RDD according to their heuristic prioritization is suggested in this short paper. We show that sparse RDDs can improve existing compilation-based algorithms significantly while keeping their optimality guarantees.

Stať ve sborníku

10.1109/IROS51168.2021.9636296

Katedra aplikované matematiky

Path planning for multiple robots (MRPP) represents a task of finding non-colliding paths for robots via which they can navigate from their initial positions to specified goal positions. The problem is often modeled using undirected graphs where robots move between vertices across edges while no two robots can simultaneously occupy the same vertex nor can traverse an edge in opposite directions. 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 linear programming (MILP), or Boolean satisfiability (SAT). In this paper, we enhance existing SAT-based algorithm for MRPP via sparsification of the set of candidate paths for each robot from which the target Boolean encoding is derived. Suggested sparsification of the set of paths led to a smaller target Boolean formulae that can be constructed and solved faster while optimality guarantees of the approach have been kept.

Stať ve sborníku

Katedra aplikované matematiky

Multi-agent path finding with continuous movements and time (denoted MAPFR) is addressed. The task is to navigate agents that move smoothly between predefined positions to their individual goals so that they do not collide. Recently a novel solving approach for obtaining makespan optimal so- lutions called SMT-CCBS based on satisfiability modulo the- ories (SMT) has been introduced. We extend the approach further towards the sum-of-costs objective which is a more challenging case in the yes/no SMT environment due to more complex calculation of the objective

Stať ve sborníku

10.1109/ICTAI50040.2020.00036

Katedra aplikované matematiky

he 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.

Stať ve sborníku

10.1109/IROS45743.2020.9341047

Katedra aplikované matematiky

Multi-robot path planning (MRPP) is a task of planning collision free paths for a group of robots in a graph. Each robot starts in its individual starting vertex and its task is to reach a given goal vertex. Existing techniques for solving MRPP optimally under various objectives include search-based and compilation-based approaches. Often however finding an optimal solution is too difficult hence sub-optimal algorithms that trade-off the quality of solutions and the runtime have been devised. We suggest eSMT-CBS, a new bounded suboptimal algorithm built on top of recent compilation-based method for optimal MRPP based on satisfiability modulo theories (SMT). We compare eSMT-CBS with ECBS, a major representative of bounded sub-optimal search-based algorithms. The experimental evaluation shows significant advantage of eSMT-CBS across variety of scenarios.

Stať ve sborníku

10.1109/ICTAI50040.2020.00186

Katedra aplikované matematiky

oken swapping (TSWAP) represents a challenging problem underlying in many practical applications ranging from item relocation to quantum program compilation. 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 a pair of adjacent vertices. The goal is to perform a sequence of swaps so that token and vertex colors agree across the graph. The total number of swaps is usually required to be small. We study bounded sub-optimal algorithms for solving the TSWAP problem.

Stať ve sborníku

10.5220/0010105800280038

Katedra aplikované matematiky

Multi-agent pathfinding is a problem of finding paths for multiple agents from their initial configuration to their goal configuration that results in a plan execution without collisions. In this paper, we deploy MAPF solutions on a swarm of small mobile robots. During the plan execution, we mitigate the problem of desynchronization that comes with the plan execution on physical hardware using the reflex-based behavior of the robots.

Stať ve sborníku

10.1109/SMC42975.2020.9283368

Katedra aplikované matematiky

Multi-agent pathfinding (MAPF) represents a core problem in robotics. In its abstract form, the task is to navigate agents in an undirected graph to individual goal vertices so that conflicts between agents do not occur. Many algorithms for finding feasible or optimal solutions have been devised. We focus on the execution of MAPF solutions with a swarm of simple physical robots. Such execution is important for understanding how abstract plans can be transferred into reality and vital for educational demonstrations. We show how to use a swarm of reflex-based Ozobot Evo robots for MAPF execution.

Stať ve sborníku

10.1007/978-3-030-59535-7_7

Katedra aplikované matematiky

Multi-agent path finding with continuous movements and time (denoted MAPF-R) is addressed. The task is to navigate agents that move smoothly between predefined positions to their individual goals so that they do not col-lide. Recently a novel solving approach for obtaining makespan optimal solutions called SMT-CBS-R based on satisfiability modulo theories (SMT) has been introduced.

Stať ve sborníku

10.1007/978-3-030-58285-2_16

Katedra aplikované matematiky

Multi-agent path finding with continuous movements and time (denoted MAPF-R) is addressed. The task is to navigate agents that move smoothly between predefined positions to their individual goals so that they do not collide. The new algorithm combines collision resolutionknown from conflict-based search (CBS) with previous generation of incompleteSAT encodings on top of a novel scheme for selecting decision variables in a po-tentially uncountable search space.

Stať ve sborníku

Katedra aplikované matematiky

Mutex propagation is a form of efficient constraint propagation popularly used in AI planning to tightly approximate the reachable states from a given state. We utilize this idea in the context of Multi-Agent Path Finding (MAPF). When adapted to MAPF, mutex propagation provides stronger constraints for conflict resolution in Conflict-Based Search (CBS), a popular optimal MAPF algorithm, and provides it with the ability to identify and reason with symmetries in MAPF.

Stať ve sborníku

10.1007/978-3-030-69322-0_16

Katedra aplikované matematiky

Multi-agent path finding (MAPF) is the problem of planning a set of non-colliding paths for a set of agents so that each agent reaches its individual goal location following its path. A mutex from classical planning is a constraint forbidding a pair of facts to be both true or a pair of actions to be executed simultaneously. In the context of MAPF, mutexes are used to rule out the simultaneous occurrence of a pair of agents in a pair of locations, which can prune the search space. Previously mutex propagation had been integrated into conflictbased search (CBS), a major search-based approach for solving MAPF optimally. In this paper, we introduce mutex propagation into the compilation-based (SATbased) solver MDD-SAT, an alternative to search-based solvers. Our experiments show that, despite mutex propagation being computationally expensive, it prunes the search space significantly so that the overall performance of MDD-SAT is improved.

Článek

Katedra aplikované matematiky

Jak přimět desetiletí propracovávané všemožné triky pracovat na hledání optimální cesty pro mobilní roboty k dosažení cíle a chytře odřezávat neperspektivní kandidáty na vyhnutí se srážkám.

Stať ve sborníku

Katedra aplikované matematiky

Multi-agent path finding (MAPF) in continuous space and time with geometric agents, i.e. agents of various geometric shapes moving smoothly between predefined positions, is addressed in this paper. We analyze a new solving approach based on satisfiability modulo theories (SMT) that is designed to obtain makespan optimal solutions.

Stať ve sborníku

10.1109/SMC42975.2020.9282891

Katedra aplikované matematiky

A variant of multi-agent path finding in continuous space and time with geometric agents MAPFR 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-CBSR based on satisfiability modulo theories (SMT).

Stať ve sborníku

Katedra aplikované matematiky

We address conflict reasoning in generalizations of multi-agent path finding (MAPF). We assume items placed in vertices of an undirected graph with at most one item per vertex. Items can be relocated across edges while various constraints depending on the concrete type of MAPF must be satisfied. We recall a general problem formulation that encompasses known types of item relocation problems such as multi-agent path finding (MAPF) and token swapping (TSWAP). We show how to express new types of relocation problems in the general problem formulation. We thoroughly evaluate a novel solving method for item relocation that combines satisfiability modulo theory (SMT) with conflict-based search (CBS).

Stať ve sborníku

10.5220/0008071501370143

Katedra aplikované matematiky

This paper addresses evacuation problems from the perspective of cooperative path finding (CPF). The evacuation problem we call multi-agent evacuation(MAE) consists of an undirected graph and a set of agents.The task is to move agents from the endangered part of the graph into the safe part as quickly as possible.Although there exist centralized evacuation algorithms based on network flows that are optimal with respect to various objectives, such algorithms would hardly be applicable in practice since real agents will not be able to follow the centrally created plan. Therefore we designed a local evacuation planning algorithm called LC-MAE based on local CPF techniques. Agent-based simulations in multiple real-life scenarios show that LC-MAE produces solutions that are only worse than the optimum by a small factor. Moreover our approach led to important findings about how many agents need to behave rationally to increase the speed of evacuation.

Stať ve sborníku

10.1109/IROS40897.2019.8967962

Katedra aplikované matematiky

We address variants of multi-robot path planning in graphs (MRPP). We assume robots placed in vertices of an undirected graph with at most one robot per vertex. Robots can move across edges while various problem specific constraints must be satisfied. We introduce a general problem formulation that encompasses known types of robot relocation problems such as multi-robot path planning (MRPP), token swapping (TSWAP), token rotation (TROT), and token permutation (TPERM).

Stať ve sborníku

10.1609/aaai.v33i01.33017627

Katedra aplikované matematiky

Multi-Agent Path Finding (MAPF) has been widely studiedin the AI community. For example, Conflict-Based Search(CBS) is a state-of-the-art MAPF algorithm based on a two-level tree-search. However, previous MAPF algorithms as-sume that an agent occupies only a single location at anygiven time, e.g., a single cell in a grid. This limits their ap-plicability in many real-world domains that have geometricagents in lieu of point agents. Geometric agents are referredto as “large” agents because they can occupy multiple pointsat the same time. In this paper, we formalize and study LA-MAPF, i.e., MAPF for large agents.

Stať ve sborníku

Katedra aplikované matematiky

Multi-Agent Path Finding (MAPF) has been widely studied in the AI community. For example, Conflict-Based Search(CBS) is a state-of-the-art MAPF algorithm based on a two-level tree-search. However, previous MAPF algorithms assume that an agent occupies only a single location at any given time, e.g., a single cell in a grid. This limits their applicability in many real-world domains that have geometric agents in lieu of point agents. In this paper, we formalize and study MAPF for large agents that considers the shapesof agents. We present a generalized version of CBS, called Multi-Constraint CBS (MC-CBS), that adds multiple constraints (instead of one constraint) for an agent when it generates a high-level search node. Experimental results show thatall MC-CBS variants significantly outperform CBS. The best variant also outperforms EPEA* (a state-of-the-art A*-based MAPF solver) in all cases and MDD-SAT (a state-of-the-art reduction-based MAPF solver) in some cases.

Stať ve sborníku

Katedra aplikované matematiky

n 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.

Stať ve sborníku

Katedra aplikované matematiky

We address a variant of multi-agent path finding(MAPF) with continuous time and geometric agents. The standard MAPF is a task of navigating agents in an undirected graph from given starting vertices to given goals so that agents do not collide. In the continuous version (MAPFR), agents move in then-dimensional Euclidean space along straight lines that inter-connect predefined positions. We present a new solving ap-proach based on satisfiability modulo theories(SMT) to obtain makespan optimal solutions. Our SMT-based approach for MAPFR called SMT-CBSR reformulates the Conflict-based Search (CBS) algorithm in terms of SMT concepts.

Stať ve sborníku

Katedra aplikované matematiky

This paper gives an overview of conflict reasoning in generalizations of multi-agent path finding (MAPF). MAPF and derived variants assume items placed in vertices of an undirected graph with at most one item per vertex. Items can be relocated across edges while various constraints depending on the concrete type of relocation problem must be satisfied. We recall a general problem formulation that encompasses known types of item relocation problems such as multi-agent path finding (MAPF), token swapping (TSWAP), token rotation (TROT), and token permutation (TPERM). We then focused on three existing optimal algorithms for MAPF: search-based CBS, and propositional satisfiability (SAT) - based MDD-SAT and SMT-CBS. These algorithms were modified to tackle various types of conflicts. The major contribution of this paper is a thorough experimental evaluation of CBS, MDD-SAT, and SMT-CBS on various types of relocation problems.

Stať ve sborníku

Katedra aplikované matematiky

This paper addresses optimal and near-optimal solving of the (N2–1)-puzzle using the A* search algorithm.We develop a novel heuristic based on artificial neural networks (ANNs) called ANN-distance that attempts to estimate the minimum number of moves necessary to reach the goal configuration of the puzzle. With a well trained ANN-distance heuristic, whose inputs are just the positions of the pebbles, we are able to achieve better accuracy of predictions than with conventional heuristics such as those derived from the Manhattan distance or pattern database heuristics. Though we cannot guarantee admissibility of ANN-distance, an experimental evaluation on random 15-puzzles shows that in most cases ANN-distance calculates the true minimum distance from the goal, and furthermore, A* search with the ANN-distance heuristic usually finds an optimal solution or a solution that is very close to the optimum. Moreover, the underlying neural network in ANN-distance consumes much less memory than a comparable pattern database.

Stať ve sborníku

Katedra aplikované matematiky

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 MAPFR, a theory of continuous MAPF with geometric agents, are also discussed.

Stať ve sborníku

Katedra aplikované matematiky

We address engineering of smart behavior of agents in evacuation problems from the perspective of cooperative path finding (CPF) in this paper.We introduce an abstract version of evacuation problems we call multi-agent evacuation (MAE) that consists of an undirected graph representing the map of the environment and a set of agents moving in this graph. The task is to move agents from the endangered part of the graph into the safe part as quickly as possible. Although the abstract evacuation task can be solved using centralized algorithms based on network flows that are near-optimal with respect to various objectives, such algorithms would hardly be applicable in practice since real agents will not be able to follow the centrally created plan. Therefore we designed a decentralized evacuation planning algorithm called LC-MAE based on local rules derived from local cooperative path finding (CPF) algorithms. We compared LC-MAE with near-optimal centralized algorithm using agent-based simulations in multiple real-life scenarios. Our finding it that LC-MAE produces solutions that are only worse than the optimum by a small factor. Moreover our approach led to important observations about how many agents need to behave rationally to increase the speed of evacuation. A small fraction of rational agents can speed up the evacuation dramatically.

Stať ve sborníku

10.24963/ijcai.2019/164

Katedra aplikované matematiky

We unify search-based and compilation-based approaches to multi-agent path finding (MAPF) through satisfiability modulo theories (SMT). The task in MAPF is to navigate agents in an undirected graph to given goal vertices so that they do not collide. We rephrase Conflict-Based Search (CBS),one of the state-of-the-art algorithms for optimal MAPF solving, in the terms of SMT. This ideac ombines SAT-based solving known from MDD-SAT, a SAT-based optimal MAPF solver, at the low-level with conflict elimination of CBS at the high-level. Where the standard CBS branches the search after a conflict, we refine the propositional model with a disjunctive constraint. Our novel algorithm called SMT-CBS hence does not branch at the high-level but incrementally extends the propositional model. We experimentally compare SMT-CBS with CBS, ICBS, and MDD-SAT.

Stať ve sborníku

Katedra aplikované matematiky

We unify search-based and compilation-based approaches to multi-agent path finding (MAPF) through satisfiability modulo theories(SMT). The task in MAPF is to navigate agents in an undirected graph to given goal vertices so that they do not collide. We rephrase Conflict-Based Search (CBS) in the terms of SMT. This idea combines MDD-SAT, a SAT-based optimal MAPF solver, at the low level with conflict elimination of CBS at the high level.

Stať ve sborníku

Katedra aplikované matematiky

We study practical approaches to solving the token swapping (TSWAP) problem optimally in this 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.

Stať ve sborníku

Katedra aplikované matematiky

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.

Článek

Katedra aplikované matematiky

V mnoha velkoskladech zásilkových společností od USA, přes Evropu po Čínu spěchají armády pojízdných robotů od jednoho regálu k druhému. Roboti nakládají a převážejí zboží na místa určení, kde je pracovníci převezmou, zabalí a následně odešlou k nedočkavým zákazníkům. Naskládat zboží do krabice ještě stále umějí lépe a rychleji lidé. Je ale asi jen otázkou času, kdy i tento úkol roboti zvládnou.

Článek

Katedra aplikované matematiky

Much of the literature on suboptimal, polynomial-time algorithms for multi-agent path finding focuses on undirected graphs, where motion is permitted in both directions along a graph edge. Despite this, traveling on directed graphs is relevant in navigation domains, such as path finding in games, and asymmetric communication networks.

Stať ve sborníku

Katedra aplikované matematiky

We present and evaluate diBOX, an algorithm for multi-agent path finding on strongly biconnected directed graphs. diBOX runs in polynomial time, computes suboptimal solutions and is complete for instances on strongly biconnected digraphs with at least two unoccupied positions. A detailed empirical analysis shows a good scalability for diBOX.

Stať ve sborníku

Katedra aplikované matematiky

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.