CLIQUE is NP-hard to VERTEX-COVER (exact size k) is NP-complete

TheoremCLIQUE is NP-hard#✓fully proved

Every decision problem \(L\) in NP has a polynomial-time many-one reduction to CLIQUE: a polynomial-time computable map \(f\) on bit strings such that, for every bit string \(x\), \(L\) accepts \(x\) exactly when CLIQUE accepts \(f(x)\).

theorem cliqueDec_npHard : ∀ L : DecisionProblem, L ∈ NP → PolyManyOneRed L cliqueDec
Uses 39 · Used by 2
Statement usesCLIQUE · Polynomial-time many-one reduction · Complexity classes · Decision problems · The complexity class NP
Proof usesEvery NP problem reduces to binary-index CNF-SAT · SAT accepts the code of a formula exactly when it is satisfiable · Unparsable input is not in SAT · Adjacency bits of Karp's clique graph · Karp's reduction from SAT to CLIQUE is correct · Decoding a graph instance · Encoding of a graph instance · SAT ≤ CLIQUE is polynomial-time · Language of graph instances with a property · Fixed no-instance · NP-hardness transfers along reductions · Adjacency of literal occurrences in Karp's clique graph · Literal occurrences of a CNF formula · Vertex pairs in encoding order · Karp's SAT-to-CLIQUE map on bit strings · Karp's CLIQUE instance of a CNF formula · The graph encoded by pair bits · Decoding a complete length-prefixed CNF formula · The CNF decoder inverts the length-prefixed CNF code · Length-prefixed binary code of a CNF formula · Reading a unary length prefix · SAT as a decision problem · CNF formula · CNF clause · Satisfiability of a CNF formula · Bitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Polynomial-time computable functions
Used byCLIQUE is NP-complete · INDEPENDENT-SET is NP-hard

TheoremINDEPENDENT-SET is NP-hard#✓fully proved

Every decision problem \(L\) in NP has a polynomial-time many-one reduction to INDEPENDENT-SET: a polynomial-time computable map \(f\) on bit strings such that, for every bit string \(x\), \(L\) accepts \(x\) exactly when INDEPENDENT-SET accepts \(f(x)\).

theorem indSetDec_npHard : ∀ L : DecisionProblem, L ∈ NP → PolyManyOneRed L indSetDec
Uses 20 · Used by 2
Statement usesINDEPENDENT-SET · Polynomial-time many-one reduction · Complexity classes · Decision problems · The complexity class NP
Proof usesCLIQUE · Correctness of the complementing map from CLIQUE to INDEPENDENT-SET · CLIQUE is NP-hard · Complementing map from CLIQUE to INDEPENDENT-SET instances · CLIQUE ≤ INDEPENDENT-SET is polynomial-time · NP-hardness transfers along reductions · Bitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Polynomial-time computable functions
Used byINDEPENDENT-SET is NP-complete · VERTEX-COVER (exact size k) is NP-hard

TheoremVERTEX-COVER (exact size k) is NP-hard#✓fully proved

Every decision problem in NP reduces by a polynomial-time many-one reduction to the decision problem VERTEX-COVER, which accepts exactly the valid encodings of a number \(k\) and a graph \(G\) such that \(G\) has a vertex cover of exactly \(k\) vertices.

theorem vertexCoverDec_npHard :
    ∀ L : DecisionProblem, L ∈ NP → PolyManyOneRed L vertexCoverDec
Uses 28 · Used by 2
Statement usesThe VERTEX-COVER problem · Polynomial-time many-one reduction · Complexity classes · Decision problems · The complexity class NP
Proof usesDecoding a graph instance · Encoding of a graph instance · Independent sets and vertex covers of complementary sizes · INDEPENDENT-SET · INDEPENDENT-SET is NP-hard · INDEPENDENT-SET ≤ VERTEX-COVER is polynomial-time · Map from INDEPENDENT-SET to VERTEX-COVER instances · Language of graph instances with a property · Unparsable input is rejected · Fixed no-instance · NP-hardness transfers along reductions · Vertex pairs in encoding order · The graph encoded by pair bits · Reading a unary length prefix · Bitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Polynomial-time computable functions
Used byVERTEX-COVER (exact size k) is NP-complete · SUBSET-SUM is NP-hard

AbbreviationThe CLIQUE, INDEPENDENT-SET and VERTEX-COVER verifier as a host component#✓fully proved

For a mode \(m\) (clique, independent set or vertex cover), this is the host component whose stacks are \(X, W, C, N, V, T\), each over the symbol alphabet of the SAT verifier, and whose labels and program are those of the verifier machine of mode \(m\).

abbrev kgVerifyComp (m : KGVerify.Mode) : Host.Comp where
  K := KGVerify.K
  Γ := fun _ => SatVerifier.Sym
  finΓ := fun _ => SatVerifier.Sym.instFintype
  L := KGVerify.Lab
  prog := KGVerify.prog m
  ks := [.X, .W, .C, .N, .V, .T]
  ks_nodup := by decide
  mem_ks k := by cases k <;> decide
Uses 6 · Used by 1
Statement usesComponent machine · Stacks of the CLIQUE verifier · Labels of the CLIQUE verifier · Modes of the clique verifier · Program of the clique verifier · Stack alphabet of the SAT verifier
Used byNP membership from the CLIQUE, INDEPENDENT-SET and VERTEX-COVER verifier

TheoremNP membership from the CLIQUE, INDEPENDENT-SET and VERTEX-COVER verifier#✓fully proved

Let \(L\) be a decision problem, let \(m\) be a mode (clique, independent set or vertex cover), and let \(V_m\) be the verifier of mode \(m\). If for every bit string \(x\), \(L\) accepts \(x\) exactly when there is a bit string \(w\) with \(|w| \le |x|\) such that \(V_m\) accepts \((x, w)\), then \(L\) is in NP.

theorem mem_NP_of_kgCheck {L : DecisionProblem} (m : KGVerify.Mode)
    (h : ∀ x, L x = true ↔ ∃ w, w.length ≤ x.length ∧ KGVerify.kgCheck m x w = true) : L ∈ NP
Uses 25 · Used by 3
Statement usesModes of the clique verifier · The verifier for CLIQUE, INDEPENDENT-SET and VERTEX-COVER · Complexity classes · Decision problems · The complexity class NP
Proof usesComponent machine · Verifier host, canonical form · Stacks of the CLIQUE verifier · Labels of the CLIQUE verifier · Program of the clique verifier · The verifier machine for clique, independent set and vertex cover · Start label of the clique verifier · The CLIQUE, INDEPENDENT-SET and VERTEX-COVER verifier as a host component · Stack alphabet of the SAT verifier · Bitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Polynomial-time computable functions · Exact-length runs of a TM2 machine · Runs within a step budget
Used byCLIQUE is in NP · INDEPENDENT-SET is in NP · VERTEX-COVER (exact size k) is in NP

TheoremCLIQUE is in NP#✓fully proved

CLIQUE is in NP.

theorem cliqueDec_mem_NP : cliqueDec ∈ NP
Uses 7 · Used by 1
Statement usesCLIQUE · Complexity classes · Decision problems · The complexity class NP
Proof usesModes of the clique verifier · CLIQUE is verified with witnesses no longer than the input · NP membership from the CLIQUE, INDEPENDENT-SET and VERTEX-COVER verifier
Used byCLIQUE is NP-complete

TheoremINDEPENDENT-SET is in NP#✓fully proved

INDEPENDENT-SET is in NP.

theorem indSetDec_mem_NP : indSetDec ∈ NP
Uses 7 · Used by 1
Statement usesINDEPENDENT-SET · Complexity classes · Decision problems · The complexity class NP
Proof usesModes of the clique verifier · INDEPENDENT-SET is verified with witnesses no longer than the input · NP membership from the CLIQUE, INDEPENDENT-SET and VERTEX-COVER verifier
Used byINDEPENDENT-SET is NP-complete

TheoremVERTEX-COVER (exact size k) is in NP#✓fully proved

The decision problem VERTEX-COVER, which accepts exactly the valid encodings of a number \(k\) and a graph \(G\) such that \(G\) has a vertex cover of exactly \(k\) vertices, is in NP.

theorem vertexCoverDec_mem_NP : vertexCoverDec ∈ NP
Uses 7 · Used by 1
Statement usesThe VERTEX-COVER problem · Complexity classes · Decision problems · The complexity class NP
Proof usesModes of the clique verifier · VERTEX-COVER is verified by the clique verifier in cover mode · NP membership from the CLIQUE, INDEPENDENT-SET and VERTEX-COVER verifier
Used byVERTEX-COVER (exact size k) is NP-complete

TheoremCLIQUE is NP-complete#✓fully proved

CLIQUE lies in NP, and every decision problem in NP has a polynomial-time many-one reduction to CLIQUE.

theorem cliqueDec_npComplete :
    cliqueDec ∈ NP ∧ ∀ L : DecisionProblem, L ∈ NP → PolyManyOneRed L cliqueDec
Uses 7
Statement usesCLIQUE · Polynomial-time many-one reduction · Complexity classes · Decision problems · The complexity class NP
Proof usesCLIQUE is in NP · CLIQUE is NP-hard

TheoremINDEPENDENT-SET is NP-complete#✓fully proved

INDEPENDENT-SET lies in NP, and every decision problem in NP has a polynomial-time many-one reduction to INDEPENDENT-SET.

theorem indSetDec_npComplete :
    indSetDec ∈ NP ∧ ∀ L : DecisionProblem, L ∈ NP → PolyManyOneRed L indSetDec
Uses 7
Statement usesINDEPENDENT-SET · Polynomial-time many-one reduction · Complexity classes · Decision problems · The complexity class NP
Proof usesINDEPENDENT-SET is in NP · INDEPENDENT-SET is NP-hard

TheoremVERTEX-COVER (exact size k) is NP-complete#✓fully proved

The decision problem VERTEX-COVER, which accepts exactly the valid encodings of a number \(k\) and a graph \(G\) such that \(G\) has a vertex cover of exactly \(k\) vertices, is in NP, and every decision problem in NP reduces to it by a polynomial-time many-one reduction.

theorem vertexCoverDec_npComplete :
    vertexCoverDec ∈ NP ∧ ∀ L : DecisionProblem, L ∈ NP → PolyManyOneRed L vertexCoverDec
Uses 7
Statement usesThe VERTEX-COVER problem · Polynomial-time many-one reduction · Complexity classes · Decision problems · The complexity class NP
Proof usesVERTEX-COVER (exact size k) is in NP · VERTEX-COVER (exact size k) is NP-hard
11 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.