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

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21240%2F23%3A00371963" target="_blank" >RIV/68407700:21240/23:00371963 - isvavai.cz</a>

Výsledek na webu

<a href="https://doi.org/10.1109/ICTAI59109.2023.00055" target="_blank" >https://doi.org/10.1109/ICTAI59109.2023.00055</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1109/ICTAI59109.2023.00055" target="_blank" >10.1109/ICTAI59109.2023.00055</a>

Jazyk výsledku

angličtina

Název v původním jazyce

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

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

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

Popis výsledku anglicky

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.

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/GA22-31346S" target="_blank" >GA22-31346S: logicMOVE: Logické uvažování v plánování pohybu pro mnoho robotických agentů</a><br>

Návaznosti

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

Rok uplatnění

2023

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

35th IEEE International Conference on Tools with Artificial Intelligence

ISBN

979-8-3503-4273-4

ISSN

1082-3409

e-ISSN

—

Počet stran výsledku

8

Strana od-do

333-340

Název nakladatele

IEEE Computer Society

Místo vydání

Cannes

Místo konání akce

Atlanta

Datum konání akce

6. 11. 2023

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

WRD - Celosvětová akce

Kód UT WoS článku

001139095400047