2.5. NP-Hardness and NP-Completeness🔗

NPHard encB B says that every problem in NP, over any type of instances and with any encoding of them, reduces to B; NPComplete adds that B is itself in NP. Hardness transfers along reductions (NPHard.trans), which is how almost every hardness proof goes. An NP-complete problem is in P exactly when P and NP coincide (NPComplete.mem_P_iff), so two NP-complete problems are both in P or both outside it (NPComplete.mem_P_iff_mem_P):

example : Clique ∈ P (encPair encGraph encNat) ↔ SAT ∈ P encCNF :=
  Clique_npComplete.mem_P_iff_mem_P CookLevin.SAT_npComplete