SMT-Based Dynamic Multi-Robot Task Allocation

要約

マルチロボット タスク割り当て (MRTA) は、荷物配送、倉庫ロボット工学、ヘルスケアなどの多くのアプリケーション ドメインで発生する問題です。
この研究では、タスクの期限と容量のあるエージェント (複数の同時タスクの容量) を持つタスクの動的ストリームに対する MRTA の問題を検討します。
これまでの研究は一般に、静的なケースに焦点を当てており、制限的なタスク仕様に特化したアルゴリズムを使用していたり​​、保証が不足していたり​​しました。
我々は、満足度モジュロ理論 (SMT) に基づいてこれらの懸念を解決する、能力を備えたロボットのための動的 MRTA へのアプローチを提案します。
私たちのアプローチが健全かつ完全であること、および SMT エンコーディングが汎用的であり、より広範なクラスのタスク仕様への拡張が可能であることを示します。
SMT ソルバーの増分解決機能を活用して、オンラインで到着する新しいタスクを割り当てるときに学習した情報を保持する方法と、実行時の比較を提供する非増分的に解決する方法を示します。
さらに、完全なエンコードに向けて繰り返し調整できる、より小さいが潜在的に不完全なエンコードから開始するアルゴリズムを提供します。
病院のような環境のグラフ抽象化から作成されたマルチロボット配信をエンコードするパラメータ化された一連のベンチマークでメソッドを評価します。
私たちのアプローチの有効性は、未解釈関数の量子記号のない理論や、複数のソルバーにわたる線形またはビットベクトル演算など、さまざまなエンコーディングを使用して実証されます。

要約(オリジナル)

Multi-Robot Task Allocation (MRTA) is a problem that arises in many application domains including package delivery, warehouse robotics, and healthcare. In this work, we consider the problem of MRTA for a dynamic stream of tasks with task deadlines and capacitated agents (capacity for more than one simultaneous task). Previous work commonly focuses on the static case, uses specialized algorithms for restrictive task specifications, or lacks guarantees. We propose an approach to Dynamic MRTA for capacitated robots that is based on Satisfiability Modulo Theories (SMT) solving and addresses these concerns. We show our approach is both sound and complete, and that the SMT encoding is general, enabling extension to a broader class of task specifications. We show how to leverage the incremental solving capabilities of SMT solvers, keeping learned information when allocating new tasks arriving online, and to solve non-incrementally, which we provide runtime comparisons of. Additionally, we provide an algorithm to start with a smaller but potentially incomplete encoding that can iteratively be adjusted to the complete encoding. We evaluate our method on a parameterized set of benchmarks encoding multi-robot delivery created from a graph abstraction of a hospital-like environment. The effectiveness of our approach is demonstrated using a range of encodings, including quantifier-free theories of uninterpreted functions and linear or bitvector arithmetic across multiple solvers.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google