Disconnection proofs for motion planning

Probabilistic road-map (PRM) planners have shown great promise in attacking previously infeasible motion planning problems with many degrees of freedom. Yet when such a planner fails to find a path, it is not clear that no path exists, or that the planner simply did not sample adequately or intelligently the free part of the configuration space. We propose to attack the motion planning problem from the other end, focusing on disconnection proofs, or proofs showing that there exists no solution to the posed motion planning problem. Just as PRM planners avoid generating a complete description of the configuration space, our disconnection provers search for certain special classes of proofs that are compact and easy to find when the motion planning problem is 'obviously impossible," avoiding complex geometric and combinatorial calculations. We demonstrate such a prover in action for a simple, yet still realistic, motion planning problem. When it fails, the prover suggests key milestones, or configurations of the robot that can then be passed on and used by a PRM planner. Thus by hitting the motion planning problem from both ends, we hope to resolve the existence of a path, except in truly delicate border-line situations.