Continuous Multi-agent Path Finding via Satisfiability Modulo Theories (SMT)

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21240%2F21%3A00356869" target="_blank" >RIV/68407700:21240/21:00356869 - isvavai.cz</a>

Result on the web

<a href="https://doi.org/10.1007/978-3-030-71158-0_19" target="_blank" >https://doi.org/10.1007/978-3-030-71158-0_19</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-030-71158-0_19" target="_blank" >10.1007/978-3-030-71158-0_19</a>

Result language

angličtina

Original language name

Continuous Multi-agent Path Finding via Satisfiability Modulo Theories (SMT)

Original language description

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

Czech name

—

Czech description

—

Type

D - Article in proceedings

CEP classification

—

OECD FORD branch

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Project

<a href="/en/project/GA19-17966S" target="_blank" >GA19-17966S: intALG-MAPFg: Intelligent Algorithms for Generalized Variants of Multi-Agent Path Finding</a><br>

Continuities

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Publication year

2021

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Article name in the collection

Agents and Artificial Intelligence, 12th International Conference, ICAART 2020, Valletta, Malta, February 22-24, 2020, Revised Selected Papers

ISBN

978-3-030-71157-3

ISSN

0302-9743

e-ISSN

—

Number of pages

22

Pages from-to

399-420

Publisher name

Springer

Place of publication

Berlin

Event location

Valletta

Event date

Feb 22, 2020

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

000722435000019