Skip to content
  1. CLRS-Lean
  2. Chapter 34. NP-Completeness
  3. 34.5. NP-Complete Problems
  4. 34.5. HAM-CYCLE
  5. 34.5. Certificate
  6. 34.5. Basic
Browse chapters
Imports
import CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.HamiltonianCycle.Language import CLRSLean.Chapter_34.Section_34_4_NP_Completeness_Proofs.GeneralClique.Certificate.Basic

Raw HAM-CYCLE certificate checker

namespace CLRS.Chapter34abbrev encodeHamiltonianCycleCertificate := encodeCliqueCertificateabbrev decodeHamiltonianCycleCertificate := decodeCliqueCertificate

Total Boolean checker for an ordered Hamiltonian-cycle certificate.

def hamiltonianCycleVerifier (certificate input : List HamiltonianCycleSym) : Bool := match decodeHamiltonianCycleInstance input, decodeHamiltonianCycleCertificate certificate with | some I, some vertices => decide (I.WellFormed ∧ I.targetSize = I.vertexCount ∧ I.ListRepresentsHamiltonianCycle vertices) | _, _ => false
end CLRS.Chapter34