Formalizing Theory of Approximating the Traveling-Salesman Problem

This repository contains the formalizations for my Interdisipliary Project at TU Munich.

For my project I have formalized parts of section 21.1, Approximation Algorithms for the TSP, from [1]. I have formalized and formally verified two approximation algorithms, the DoubleTree and the Christofides-Serdyukov algorithm, for the Metric TSP. I have also formalized an L-reduction from the Minimum Vertex Cover Problem with maximum degree of 4 to the Metric TSP, which proves the MaxSNP-hardness of the Metric TSP.

References

• [1] B. Korte and J. Vygen. Combinatorial Optimization: Theory and Algorithms. Springer Berlin, Heidelberg, 6th edition, 2018.