Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Time-Ordered Ad-hoc Resource Sharing for Independent Robotic Agents

Arjo Chakravarty, Michael X. Grey, M. A. Viraj J. Muthugala, Mohan Rajesh Elara

TL;DR

The paper tackles ad-hoc resource contention among multiple robots by formalizing resource sharing as a constrained assignment problem and encoding it in CNF for SAT solvers. It develops a weighted-SAT optimizer that minimizes $\min \sum_{i,j} x_{i,j} c_{i,j}$ through iterative SAT solving with added exclusion clauses, complemented by a greedy conflict-driven method. It extends the CNF to schedule across time by introducing ordering variables $X_{ijkm}$ and compares discrete time discretization to a continuous-time ordering approach, showing efficiency gains for the continuous variant. The approach is validated in simulation and on two Smorphi robots, with open-source ROS 2/Open-RMF tooling published to enable ad-hoc resource sharing in real-world multi-robot deployments.

Abstract

Resource sharing is a crucial part of a multi-robot system. We propose a Boolean satisfiability based approach to resource sharing. Our key contributions are an algorithm for converting any constrained assignment to a weighted-SAT based optimization. We propose a theorem that allows optimal resource assignment problems to be solved via repeated application of a SAT solver. Additionally we show a way to encode continuous time ordering constraints using Conjunctive Normal Form (CNF). We benchmark our new algorithms and show that they can be used in an ad-hoc setting. We test our algorithms on a fleet of simulated and real world robots and show that the algorithms are able to handle real world situations. Our algorithms and test harnesses are opensource and build on Open-RMFs fleet management system.

Time-Ordered Ad-hoc Resource Sharing for Independent Robotic Agents

TL;DR

The paper tackles ad-hoc resource contention among multiple robots by formalizing resource sharing as a constrained assignment problem and encoding it in CNF for SAT solvers. It develops a weighted-SAT optimizer that minimizes through iterative SAT solving with added exclusion clauses, complemented by a greedy conflict-driven method. It extends the CNF to schedule across time by introducing ordering variables and compares discrete time discretization to a continuous-time ordering approach, showing efficiency gains for the continuous variant. The approach is validated in simulation and on two Smorphi robots, with open-source ROS 2/Open-RMF tooling published to enable ad-hoc resource sharing in real-world multi-robot deployments.

Abstract

Resource sharing is a crucial part of a multi-robot system. We propose a Boolean satisfiability based approach to resource sharing. Our key contributions are an algorithm for converting any constrained assignment to a weighted-SAT based optimization. We propose a theorem that allows optimal resource assignment problems to be solved via repeated application of a SAT solver. Additionally we show a way to encode continuous time ordering constraints using Conjunctive Normal Form (CNF). We benchmark our new algorithms and show that they can be used in an ad-hoc setting. We test our algorithms on a fleet of simulated and real world robots and show that the algorithms are able to handle real world situations. Our algorithms and test harnesses are opensource and build on Open-RMFs fleet management system.
Paper Structure (16 sections, 1 theorem, 11 equations, 10 figures, 3 algorithms)

This paper contains 16 sections, 1 theorem, 11 equations, 10 figures, 3 algorithms.

Table of Contents

  1. INTRODUCTION
  2. Background
  3. Problem Statement
  4. Definitions
  5. Simplification to CNF
  6. Cost Optimization
  7. Weighted-SAT Based Approach
  8. Alternate Solution to Optimization via a Greedy Conflict Driven Approach
  9. Understanding the weaknesses of each algorithm
  10. Experimental Benchmarks
  11. Extending the system to encode time ranges
  12. CNF encoding of scheduling constraints to create a model
  13. Definitions
  14. Comparing Discretization vs Continuous representation
  15. Validation
  16. ...and 1 more sections

Key Result

Lemma IV.1

Given an assignment $A_1=(x_{0,j} , x_{1,l} .... x_{n, z})$ if a cheaper solution $A_2$ exists, then $\exists x_{i,j} \in A_2$ such that given $x_{i,k} \in A_1$, $c_{i,j} < c_{i,k}$.

Figures (10)

  • Figure 1: Box-plot of Naive SAT based search vs heuristic driven search. Both solvers were given 100 hard optimization problems of different sizes. Benchmark was run on a 24-core GCP instance with code written in Rust. Each request has 10 alternatives.
  • Figure 2: Example of a scenario which elicits a worst case response in the SAT optimization process but is quickly solved by the greedy process in $O(n)$
  • Figure 3: Example of a scenario which elicits a worst case response in the Greedy process but is quickly solved by the SAT optimization process. Assume that alt3 has lowest cost.
  • Figure 4: Box-plot of time taken for SAT with heuristics to generate first feasible but suboptimal solution. For a request size of $n$, there are $n$ alternatives. I.E for 40 requests there are 40 alternatives each.
  • Figure 5: Box plot showing performance comparison when many options exist and no conflicts exist. Problem size $n$ refers to number of requests. Each request also has $n$ alternatives
  • ...and 5 more figures

Theorems & Definitions (2)

  • Lemma IV.1
  • proof