Abstract

Satisfiability Modulo Theories (SMT) solvers have recently emerged as a core technology in automated reasoning about systems. In this paper, we demonstrate the utility of these solvers in integrated task and motion planning (ITMP) for robots performing mobile manipulation. Specifically, we present a system–-called ROBOSYNTH–-for integrated task and motion planning that uses discrete search based on SMT-solvers as a complement to motion planning algorithms. As far as we know, this is the first application of SMT-solving in ITMP. The inputs to our version of ITMP are: (1) a scene description that specifies the physical space that the robot manipulates; (2) a plan outline that syntactically defines a space of plausible integrated plans; and (3) a set of logical requirements that we want the generated plan to satisfy. Given these inputs, our method uses a motion planning algorithm to construct a discrete placement graph whose paths represent feasible, low-level motion plans. An SMT-solver is now used to symbolically explore the space of all integrated plans that correspond to paths in the placement graph, and also satisfy the constraints demanded by the plan outline and the requirements. We have evaluated our approach on a generalization of an ITMP problem investigated in prior work. The experiments demonstrate that our method is capable of generating inte- grated plans that are interesting in a qualitative sense. We also find the method to scale well with an increase in the number of objects and locations manipulated, as well as the size of the space of plausible integrated plans.

Publisher: http://dx.doi.org/10.1109/ICRA.2014.6906924

PDF preprint: http://kavrakilab.org/publications/nedunuri-prabhu2014smt-based-synthesis-of.pdf