Set Reconciliation

This entry formally verifies the set reconciliation algorithm with nearly optimal communication complexity, due to Y. Minsky et al. [1]. The algorithm allows two communication partners, who have a similar pair of sets to reconcile them while using messages of nearly optimal size, proportional to a bound on the maximum symmetric difference between the sets. The formalization also introduces an optimization, which reduces the communication complexity even further compared to the original publication.