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

Kód výsledku v 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>

Výsledek na webu

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

Jazyk výsledku

angličtina

Název v původním jazyce

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

Popis výsledku v původním jazyce

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

Název v anglickém jazyce

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

Popis výsledku anglicky

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

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

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

Projekt

<a href="/cs/project/GA19-17966S" target="_blank" >GA19-17966S: intALG-MAPFg: Inteligentní algoritmy pro zobecněné varianty multi-agetního hledání cest</a><br>

Návaznosti

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

Rok uplatnění

2021

Kód důvěrnosti údajů

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

Název statě ve sborníku

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

—

Počet stran výsledku

22

Strana od-do

399-420

Název nakladatele

Springer

Místo vydání

Berlin

Místo konání akce

Valletta

Datum konání akce

22. 2. 2020

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

000722435000019