Ing. Martin Čapek

Stať ve sborníku

Katedra teoretické informatiky
Katedra aplikované matematiky

The task in multi-agent path finding (MAPF) is to find non- conflicting paths connecting agents’ start and goal positions. The MAPF problem is often compiled to Boolean satisfia- bility (SAT) and solved by existing SAT solvers. Contem- porary compilation approaches of MAPF to SAT regard the SAT solver as an external tool whose task is to return an as- signment of all decision variables of a Boolean model of the input MAPF instance. We present in this paper a novel compi- lation scheme called DPLL(MAPF) in which the consistency checking of partial assignments of decision variables with re- spect to the MAPF rules is integrated directly into the SAT solver. This scheme allows for far more automated compila- tion where the SAT solver and the consistency checking pro- cedure work together simultaneously to create the Boolean model and to search for its satisfying assignment.