Using incomplete satisfiability modulo theories to determine robotic tasks

Abstract

Many robotic task specifications can be naturally expressed by boolean combinations of arbitrary constraints. This allows a separation of problem description and solution strategy. In this paper, we present a novel approach to solve non-linear constraint systems based on Satisfiability Modulo Theories. While most SMT-based techniques emphasize completeness, we intentionally use an incomplete local search strategy. Despite this incompleteness, the presented solution is able to deal with many real world problems like task allocation or robot positioning. We show that our approach is able to exploit the logical structure to solve highly complex tasks almost in real-time.