Non-Refined Abstractions in Counterexample Guided Abstraction Refinement for Multi-Agent Path Finding
The result's identifiers
Result code in 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>
Result on the web
<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>
Alternative languages
Result language
angličtina
Original language name
Non-Refined Abstractions in Counterexample Guided Abstraction Refinement for Multi-Agent Path Finding
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 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.
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
2023
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
35th IEEE International Conference on Tools with Artificial Intelligence
ISBN
979-8-3503-4273-4
ISSN
1082-3409
e-ISSN
—
Number of pages
8
Pages from-to
333-340
Publisher name
IEEE Computer Society
Place of publication
Cannes
Event location
Atlanta
Event date
Nov 6, 2023
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
001139095400047