Non-Refined Abstractions in Counterexample Guided Abstraction Refinement for Multi-Agent Path Finding (Extended Abstract)
The result's identifiers
Result code in 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>
Result on the web
<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>
Alternative languages
Result language
angličtina
Original language name
Non-Refined Abstractions in Counterexample Guided Abstraction Refinement for Multi-Agent Path Finding (Extended Abstract)
Original language description
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.
Czech name
—
Czech description
—
Classification
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)
Result continuities
Project
<a href="/en/project/GA22-31346S" target="_blank" >GA22-31346S: logicMOVE: Logic Reasoning in Motion Planning for Multiple Robotic Agents</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Others
Publication year
2024
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
Proceedings of the Seventeenth International Symposium on Combinatorial Search (SoCS 2024)
ISBN
978-1-57735-891-6
ISSN
2832-9171
e-ISSN
2832-9163
Number of pages
2
Pages from-to
287-288
Publisher name
AAAI Press
Place of publication
Menlo Park
Event location
Kananaskis
Event date
Jun 6, 2024
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—