Title
Motion planning with Satisfiability Modulo Theories
Abstract
Motion planning is an important problem with many applications in robotics. In this paper, we focus on motion planning with rectangular obstacles parallel to the X, Y or Z axis. We formulate motion planning using Satisfiability Modulo Theories (SMT) and use SMT solvers to find a feasible path from the source to the goal. Our formulation decompose the robotic path into N path segments where the two ends of each path segment can be constrained using difference logic. Our SMT approach will find a solution if and only if a feasible path exists for the given constraints. We present extensive experimental results to demonstrate the scalability of our approach.
Year
DOI
Venue
2014
10.1109/ICRA.2014.6906597
Robotics and Automation
Keywords
DocType
ISSN
computability,mobile robots,path planning,SMT approach,SMT solvers,motion planning,rectangular obstacles,robotics,satisfiability modulo theory
Conference
1050-4729
Citations 
PageRank 
References 
3
0.40
10
Authors
7
Name
Order
Citations
PageRank
William N. N. Hung130434.98
Xiaoyu Song247151.61
Jindong Tan368777.41
Xiaojuan Li485.01
Jie Zhang5366.46
R. Wang66111.21
Peng Gao730.74