finished report

Author: kollerlukas

README.md

@@ -1,9 +1,10 @@
 # Formalising Theory of Approximating the Travelling-Salesman Problem
 
-## TODO
-- [x] formalize and proof correct Double-Tree algorithm (`./DoubleTree.thy`)
-- [x] formalize and proof correct Christofides-Serdyukov algorithm (`./ChristofidesSerdyukov.thy`)
-- [ ] (?) connect Prim formalization (finish adaptor `./MSTPrimAdaptor.thy`)
-- [ ] (?) formalize and proof correct algroithm for Eulerian Tour (`./Eulerian.thy`)
-- [ ] (?) formalize Multi-graphs by encoding Multi-graphs in normal-simple graphs (`./MultiGraph.thy`)
-- [ ] proof MAXSNP-hardness of metric TSP
+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.