SAT ENCODING

Multi-Agents Path Finding - Implemented in Python

Developed a project to encode Multi-Agent Pathfinding (MAPF) problems into SAT (Satisfiability) instances using Multi-valued Decision Diagrams (MDDs). The approach focused on minimizing the sum-of-costs by representing agents' paths and constraints as logical formulas. MDDs were used to capture feasible paths for each agent efficiently, and a state-of-the-art SAT solver was integrated to compute solutions. The project emphasized performance evaluation and scalability, addressing challenges in encoding large MAPF instances and optimizing computation times through advanced heuristics and solver configurations. This work contributes to solving complex MAPF problems with applications in robotics, logistics, and AI.