面向遥感应用的足球球图识别代码集合基数

在卫星监视地球的背景下，我们可以假设地球表面被划分为一组区域。我们假设巨大的社会/环境事件的影响会蔓延到相邻区域。通过识别代码集合（ICS），我们可以将传感器部署在这样的方式，使得发生事件的区域即使传感器数量少于区域数量，也能被唯一识别。由于地球几乎是一个球体，我们使用足球作为模型。我们构建了足球球图（SBG），并提供了面向人的、分析性的证明，表明 1）SBG 至少有 26 个基数为 10 的 ICS，暗示存在至少 26 种不同的方式部署 10 个卫星来监视地球；以及 2）SBG 的最小识别代码集（MICS）的基数至少为 9。随后我们提供了面向机器的形式化证明，表明 SBG 的 MICS 的基数实际上是 10，即必须部署至少 10 个卫星来监视 SBG 模型中的地球。我们还提供了机器导向的证明，表明 SBG 中恰好存在 26 个基数为 10 的 ICS。