Counterexample Guided Inductive Optimization Applied to Mobile Robots Path Planning (Extended Version)

TL;DR

This paper introduces a novel off-line path planning algorithm for mobile robots that uses Counterexample-Guided Inductive Optimization with SAT and SMT solvers to achieve globally optimal paths.

Contribution

It is the first application of CEGIO to mobile robot path planning, demonstrating its effectiveness with off-the-shelf solvers for 2D path optimization.

Findings

Successfully applied CEGIO to 2D robot path planning

Achieved globally optimal paths using SAT/SMT solvers

First use of CEGIO in mobile robotics

Abstract

We describe and evaluate a novel optimization-based off-line path planning algorithm for mobile robots based on the Counterexample-Guided Inductive Optimization (CEGIO) technique. CEGIO iteratively employs counterexamples generated from Boolean Satisfiability (SAT) and Satisfiability Modulo Theories (SMT) solvers, in order to guide the optimization process and to ensure global optimization. This paper marks the first application of CEGIO for planning mobile robot path. In particular, CEGIO has been successfully applied to obtain optimal two-dimensional paths for autonomous mobile robots using off-the-shelf SAT and SMT solvers.