Skip to content
  1. CLRS-Lean
  2. Chapter 34. NP-Completeness
  3. 34.5. NP-Complete Problems
  4. 34.5. VERTEX-COVER
  5. 34.5. Bidirectional CLIQUE / VERTEX-COVER Semantics
Browse chapters
Imports
import CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.VertexCover.ReverseCompleteness

Bidirectional complement semantics for CLIQUE and VERTEX-COVER

For a well-formed graph-plus-target instance, the deterministic complement construction translates the decision predicates exactly in either direction.

namespace CLRSnamespace Chapter34namespace CliqueInstance

A well-formed instance has a cover of size at most k exactly when its complement has a clique of size |V| - k.

theorem hasVertexCover_iff_complement_hasClique {I : CliqueInstance} (hI : I.WellFormed) : I.HasVertexCover ↔ I.complementForVertexCover.HasClique := by constructor · exact complement_hasClique_of_hasVertexCover · exact hasVertexCover_of_complement_hasClique hI
end CliqueInstanceend Chapter34end CLRS