Non-Refined Abstractions in Counterexample Guided Abstraction Refinement for Multi-Agent Path Finding (Extended Abstract)

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21240%2F24%3A00381968" target="_blank" >RIV/68407700:21240/24:00381968 - isvavai.cz</a>

Výsledek na webu

<a href="https://doi.org/10.1609/socs.v17i1.31584" target="_blank" >https://doi.org/10.1609/socs.v17i1.31584</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1609/socs.v17i1.31584" target="_blank" >10.1609/socs.v17i1.31584</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 (Extended Abstract)

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

Název v anglickém jazyce

Non-Refined Abstractions in Counterexample Guided Abstraction Refinement for Multi-Agent Path Finding (Extended Abstract)

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

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í

2024

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

Proceedings of the Seventeenth International Symposium on Combinatorial Search (SoCS 2024)

ISBN

978-1-57735-891-6

ISSN

2832-9171

e-ISSN

2832-9163

Počet stran výsledku

2

Strana od-do

287-288

Název nakladatele

AAAI Press

Místo vydání

Menlo Park

Místo konání akce

Kananaskis

Datum konání akce

6. 6. 2024

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

WRD - Celosvětová akce

Kód UT WoS článku

—