SAT-Based Large Neighborhood Search for Multi-Agent Pathfinding

We propose a novel hybrid algorithm, LNS-SAT, that uses a Boolean Satisfiability (SAT) repair engine within a Large Neighborhood Search (LNS) to solve Multi-Agent Path Finding (MAPF) makespan-optimally. An initial solution is obtained from the agents’ shortest paths to their goal, where they wait for all agents to finish. Compact spatial-temporal zones are created around conflicts and solved using a lazy Multi-Decision Diagrams (MDDs) SAT encoding. If a zone proves unsatisfiable (UNSAT) time of agents who wait at their goal is reallocated to the zone. If no more waiting time (slack) is available, the zone is expanded and tried again until a local solution is found. In the limit, the zone encompasses the full MAPF instance. Increasing the makespan only when the global instance is UNSAT ensures that the first successful makespan is optimal. Experiments on MovingAI benchmark maps with 10–200 agents show substantially higher success rates and lower runtimes compared to a global MDD-SAT baseline. LNS-SAT scales the performance of MDD-SAT encodings to larger maps with more agents while preserving optimality.