Skip to content
  1. CLRS-Lean
  2. Chapter 34. NP-Completeness
  3. 34.5. NP-Complete Problems
  4. 34.5. Decision traveling-salesperson problem
  5. 34.5. Certificate
  6. 34.5. Basic
Browse chapters
Imports
import CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.TravelingSalesperson.Language

Raw decision-TSP certificate checker

namespace CLRS.Chapter34

Total Boolean checker for an ordered decision-TSP tour certificate.

def tspVerifier (certificate input : List TSPSym) : Bool := match decodeTSPData input, decodeTSPCertificate certificate with | some data, some vertices => decide (data.WellFormed ∧ data.toInstance.ListRepresentsTour vertices) | _, _ => false
end CLRS.Chapter34