A novel approach to cooperative path-planning is presented. A SAT solver is used not to solve the whole instance but for optimizing the makespan of a sub-optimal solu-tion.
This approach is trying to exploit the ability of state-of-the-art SAT solvers to give a solution to relatively small instance quickly. A sub-optimal solution to the instance is obtained by some existent method first.
It is then submitted to the optimi-zation process which decomposes it into small subsequences for which optimal solu-tions are found by a SAT solver. The new shorter solution is subsequently obtained as concatenation of optimal sub-solutions.