# DPLL(MAPF): an Integration of Multi-Agent Path Finding and SAT Solving Technologies

arXiv: https://arxiv.org/abs/2111.06494 · HTML: https://mlsanity.com/paper/2111.06494/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 5 of its 38 references that are in the map.
- First posted on arXiv 11 Nov 2021.

## Builds on (most cited first, 5 of 5)

- [MAPP: a Scalable Multi-Agent Path Planning Algorithm with Tractability and Completeness Guarantees](https://mlsanity.com/paper/1401.3905/) (2014)
- [Overview: Generalizations of Multi-Agent Path Finding to Real-World Scenarios](https://mlsanity.com/paper/1702.05515/) (2017)
- [Multi-Agent Path Finding with Deadlines](https://mlsanity.com/paper/1806.04216/) (2018)
- [Explanation Generation for Multi-Modal Multi-Agent Path Finding with Optimal Resource Utilization using Answer Set Programming](https://mlsanity.com/paper/2008.03573/) (2020)
- [Towards Search-based Motion Planning for Micro Aerial Vehicles](https://mlsanity.com/paper/1810.03071/) (2018)

## Built on by (most cited first, 1 of 1)

- [An Analysis of Constraint-Based Multi-Agent Pathfinding Algorithms](https://mlsanity.com/paper/2511.18604/) (2025)

## Abstract (arXiv)

In multi-agent path finding (MAPF), the task is to find non-conflicting paths for multiple agents from their initial positions to given individual goal positions. MAPF represents a classical artificial intelligence problem often addressed by heuristic-search. An important alternative to search-based techniques is compilation of MAPF to a different formalism such as Boolean satisfiability (SAT). Contemporary SAT-based approaches to MAPF regard the SAT solver as an external tool whose task is to return an assignment of all decision variables of a Boolean model of input MAPF. We present in this short paper a novel compilation scheme called DPLL(MAPF) in which the consistency checking of partial assignments of decision variables with respect to the MAPF rules is integrated directly into the SAT solver. This scheme allows for far more automated compilation where the SAT solver and the consistency checking procedure work together simultaneously to create the Boolean model and to search for its satisfying assignment.