The Cardinality of Identifying Code Sets for Soccer Ball Graph with Application to Remote Sensing

TL;DR

This work models Earth-region monitoring as a Minimum Identifying Code Set (MICS) problem on a Soccer Ball Graph (SBG), proving via human-style arguments that the MICS lies between $9$ and $10$ and that at least $26$ distinct size-$10$ ICSes exist. It then employs a comprehensive machine-verified approach: encoding the ICS problem as pseudo-Boolean constraints, generating a cutting-planes proof of unsatisfiability to show that no solution with $| ext{ICS}|\,\le 9$ exists, and using PB solving to confirm that a size-$10$ ICS does exist and that exactly $26$ such solutions exist. The combination of analytical lower/upper bounds and machine-verified certificates provides rigorous guarantees for satellite deployment strategies in the soccer-ball planet model and demonstrates the viability of machine-generated proofs for combinatorial sensor-placement questions. The methods, including PB encodings, certificate verification, and solution counting, offer a blueprint for certifiable proofs in related graph-structured monitoring and network-design problems.

Abstract

In the context of satellite monitoring of the earth, we can assume that the surface of the earth is divided into a set of regions. We assume that the impact of a big social/environmental event spills into neighboring regions. Using Identifying Code Sets (ICSes), we can deploy sensors in such a way that the region in which an event takes place can be uniquely identified, even with fewer sensors than regions. As Earth is almost a sphere, we use a soccer ball as a model. We construct a Soccer Ball Graph (SBG), and provide human-oriented, analytical proofs that 1) the SBG has at least 26 ICSes of cardinality ten, implying that there are at least 26 different ways to deploy ten satellites to monitor the Earth and 2) that the cardinality of the minimum Identifying Code Set (MICS) for the SBG is at least nine. We then provide a machine-oriented formal proof that the cardinality of the MICS for the SBG is in fact ten, meaning that one must deploy at least ten satellites to monitor the Earth in the SBG model. We also provide machine-oriented proof that there are exactly 26 ICSes of cardinality ten for the SBG.

Figures (3)

• Figure 1: A soccer ball and the corresponding Soccer Ball Graph (SBG).
• Figure 2: Examples of Color Assignments using Motif IIA. A circle drawn around a node indicates that that node is injected with color. We visualise the motifs by drawing red convex hulls around a $P$-type nodes that are injected with color, and blue convex hulls around all $H$-type nodes that are injected with color.
• Figure 4: A proof that the set of PB constraints in \ref{['eq:unsat-pb']} is unsatisfiable.

Theorems & Definitions (19)

• Definition 1
• Definition 2
• Definition 3
• Definition 4
• Theorem 1
• Proof 1
• Theorem 2
• Proof 2
• Lemma 1
• Proof 3