What is it about?
We model the multi-agent pathfinding problem via reduction to SAT with combination of Graph Theories provided by Monosat solver. The pure SAT encoding contains many clauses modeling a correct path in a graph, while only a smaller part of the formula forbids the conflicts between agents. The connectivity part of the formula can be off-loaded to the Graph Theories.
Featured Image
Why is it important?
This is the first usage of Graph Theories in context of MAPF. While the Monosat solver is no longer maintained, it still managed to outperform novel SAT solver. This indicates both an interesting research path in MAPF research as well as the motivation to include Graph Theories into any SMT solver.
Read the Original
This page is a summary of: Modelling Multi-Agent Pathfinding Problems by Integrating Connectivity and No-Collision Constraints, International Foundation for Autonomous Agents and Multiagent Systems,
DOI: 10.65109/bhiz5140.
You can read the full text:
Contributors
The following have contributed to this page
