Email Gateway (Oct 28 2026 at 15:51): Email Gateway (Oct 28 2026 at 15:51):From: Jasmin Blanchette <jasmin.blanchette@ifi.lmu.de>
Subject: [isabelle] New AFP entry: Travelling Salesman via Dynamic Programming
Dear all,
It is my pleasure to announce the following C.S.-related formalization:
Travelling Salesman via Dynamic Programming
by Maksym Bortin
https://isa-afp.org/entries/TSP_Dyn_Prog.html
Travelling Salesman Problem (TSP) is well-known to be NP-hard. The computational solution, derived in this theory, follows the Bellman-Held-Karp approach utilising the power set of locations to be visited by the salesman.
Enjoy!
Jasmin
Last updated: Oct 29 2026 at 04:52 UTC