|
|
Solving multi-agent pathfinding via incremental SAT
Agh, Juraj ; Švancara, Jiří (advisor) ; Barták, Roman (referee)
Incremental SAT (satisfiability) is a way of determining the satisfiability of a formula repeatedly based on the previous determination. Multi-Agent path finding is a task of finding paths for a fixed set of agents in a shared environment without any collisions. When we require an optimal solution of MAPF using a SAT solver, we iterate through repeated formulae, each adjusted to the length of the solution. This leads us to use Incremental SAT solver. In this work, we try to solve the problems that arise during application of Incremental SAT solver to the MAPF. This is done in several steps. Firstly, we introduce some approaches to solve MAPF with a basic SAT solver. We model these approaches in C++ language, which provides us with some simply modifiable models for creating formulae. In the next step, we modify the better model to a model using an Incremental SAT solver. Thus at every iteration the model instead of creating a new formula, only extends the old formula. Lastly, we compare these approaches solving MAPF with an Incremental SAT solver.
|
guest ::
RSS feed.