A propositional satisfiability (SAT) benchmark motivated by planning paths for multiple robots on graphs is described in this short paper. It is suggested to model the ques-tion if robots can find paths in a graph to given goal vertices in the given number of time steps as propositional satisfiability.
The problem, its propositional model, and benchmark genera-tor for grid environments are described.