A Minimum Exact Disjunctive Basis for Two-Robot Solvability Profiles

Abstract

We completely characterize the solvability profiles of tasks for two autonomous mobile robots in the plane under variable disorientation, chirality, and rigid movements. The four standard capability models and the schedulers considered here have a known quotient order Q of thirteen computational classes. A task's solvability profile is the set of classes in which it is solvable, and is necessarily an upset of Q. We prove that every upset is realizable and construct a minimum exact disjunctive basis of thirteen concrete tasks. The basis contains one task for each principal upset. For every antichain of Q, the disjunction of the corresponding tasks has profile exactly equal to the union of their profiles. This exactness is not implied by the individual profiles: an algorithm may satisfy different disjuncts in different executions. We establish it by constructing, for every algorithm in each maximal class outside the target union, a single admissible fair execution violating all selected predicates simultaneously. Consequently, the realizable profiles form the entire finite distributive lattice Up(Q): there are exactly 54 profiles, counted by the antichain polynomial 1 + 13z + 24z^2 + 16z^3, and each has a canonical disjunctive representation using at most three principal tasks. We also identify six tasks whose solvability signatures recover every inclusion and incomparability in Q, and prove that six is minimum even among arbitrary separating tasks. Their profiles are precisely the principal upsets generated by the join-irreducible elements of Q. In contrast, any task family generating every profile by exact disjunctions must contain all thirteen principal profiles. Thus our exact disjunctive basis has minimum size and is unique at the profile level.

The Minimum Q-Order of BFGS with Exact Line Search Is One
Benqi Liu, Chenyi Li, Zaiwen Wen
arXiv1 Sep 2026PreprintarXiv licenceFull textOptimisation & controlarXiv
Exact Minimum Extension Degrees for Reed Solomon Codes under Linear and Nonlinear Repair at the Cut Set Bound
Yuhan Li
arXiv25 Oct 2026PreprintarXiv licenceFull textGeneral mathematicsarXiv
Links of minimum degree and exact covering numbers
Alfonso Gippini Requeijo
arXiv21 Oct 2026PreprintCC BY 4.0Full textCombinatorics & discrete mathematicsarXiv
An Odd-Arch Family of Perturbed Hofstadter Q-Recursions: Gaussian Profiles and Exact Frequency Laws
Marco Mantovanelli
arXiv1 Nov 2026PreprintCC BY 4.0Full textAlgebra & number theory Combinatorics & discrete mathematicsarXiv
On solving integer bilevel optimization problems with a non-convex quadratic follower objective function using disjunctive cuts
Kübra Tanınmış, Elisabeth Gaar, Jon Lee +2
arXiv1 Oct 2026PreprintCC BY 4.0Full textOptimisation & controlarXiv

Cite

BibTeX RIS

BibTeX

@misc{ninomiya2026minimum,
  title = {{A Minimum Exact Disjunctive Basis for Two-Robot Solvability Profiles}},
  author = {Tsukasa Ninomiya and Shota Naito and Naoki Kitamura and Yuichi Sudo and Koichi Wada},
  howpublished = {arXiv},
  year = {2026},
  month = oct,
  doi = {10.48550/arxiv.2610.17677},
  eprint = {2610.17677},
  archivePrefix = {arXiv},
  url = {https://arxiv.org/abs/2610.17677},
  note = {CC BY 4.0},
}

RIS

TY  - UNPB
TI  - A Minimum Exact Disjunctive Basis for Two-Robot Solvability Profiles
AU  - Tsukasa Ninomiya
AU  - Shota Naito
AU  - Naoki Kitamura
AU  - Yuichi Sudo
AU  - Koichi Wada
PY  - 2026
DA  - 2026/10/13
PB  - arXiv
DO  - 10.48550/arxiv.2610.17677
UR  - https://arxiv.org/abs/2610.17677
AB  - We completely characterize the solvability profiles of tasks for two autonomous mobile robots in the plane under variable disorientation, chirality, and rigid movements. The four standard capability models and the schedulers considered here have a known quotient order Q of thirteen computational classes. A task's solvability profile is the set of classes in which it is solvable, and is necessarily an upset of Q. We prove that every upset is realizable and construct a minimum exact disjunctive basis of thirteen concrete tasks. The basis contains one task for each principal upset. For every antichain of Q, the disjunction of the corresponding tasks has profile exactly equal to the union of their profiles. This exactness is not implied by the individual profiles: an algorithm may satisfy different disjuncts in different executions. We establish it by constructing, for every algorithm in each maximal class outside the target union, a single admissible fair execution violating all selected predicates simultaneously. Consequently, the realizable profiles form the entire finite distributive lattice Up(Q): there are exactly 54 profiles, counted by the antichain polynomial 1 + 13z + 24z^2 + 16z^3, and each has a canonical disjunctive representation using at most three principal tasks. We also identify six tasks whose solvability signatures recover every inclusion and incomparability in Q, and prove that six is minimum even among arbitrary separating tasks. Their profiles are precisely the principal upsets generated by the join-irreducible elements of Q. In contrast, any task family generating every profile by exact disjunctions must contain all thirteen principal profiles. Thus our exact disjunctive basis has minimum size and is unique at the profile level.
ER  -

Abstract

Related

Cite