Documentation

DescriptiveComplexity.Problems.CliqueFamily

The clique family is NP-complete #

Umbrella file for the problems Clique, Independent Set and Vertex Cover on marked graphs (DescriptiveComplexity.Clique, DescriptiveComplexity.IndependentSet, DescriptiveComplexity.VertexCover, defined in DescriptiveComplexity.Problems.CliqueFamily.Defs), collecting the quantifier-free reductions of DescriptiveComplexity.Problems.CliqueFamily.Reductions and their composites – all three problems are FO-interreducible – and deriving the NP-completeness of all three from

with no machine model anywhere. Membership travels backward and hardness forward along the quantifier-free inter-reductions, yielding DescriptiveComplexity.indSet_NP_complete and DescriptiveComplexity.vertexCover_NP_complete. As with any complexity-theoretic statement, these results are about finite marked graphs only (ComplexityClass.mem_congr_finite/hard_congr_finite).

source
noncomputable def DescriptiveComplexity.vertexCover_fo_reduction_clique :
FOReduction VertexCover Clique

Vertex Cover FO-reduces to Clique, by composing the mark and edge complementations.

Equations
Instances For
    source
    noncomputable def DescriptiveComplexity.clique_fo_reduction_vertexCover :
    FOReduction Clique VertexCover

    Clique FO-reduces to Vertex Cover, by composing the edge and mark complementations.

    Equations
    Instances For

      NP-completeness #

      source
      theorem DescriptiveComplexity.clique_mem_NP :
      NP.Mem Clique

      Clique is in NP: it is Σ₁-definable.

      source
      theorem DescriptiveComplexity.clique_NP_hard :
      NP.Hard Clique

      Clique is NP-hard: SAT, which is NP-hard, reduces to it by an ordered FO reduction.

      source
      theorem DescriptiveComplexity.clique_NP_complete :
      NP.Complete Clique

      Clique is NP-complete, derived from the first-order reductions of this library and the Cook–Levin theorem.

      source
      theorem DescriptiveComplexity.indSet_mem_NP :
      NP.Mem IndependentSet

      Independent Set is in NP: it FO-reduces to Clique, which is in NP.

      source
      theorem DescriptiveComplexity.indSet_NP_hard :
      NP.Hard IndependentSet

      Independent Set is NP-hard: Clique, which is NP-hard, reduces to it.

      source
      theorem DescriptiveComplexity.indSet_NP_complete :
      NP.Complete IndependentSet

      Independent Set is NP-complete.

      source
      theorem DescriptiveComplexity.vertexCover_mem_NP :
      NP.Mem VertexCover

      Vertex Cover is in NP: it FO-reduces to Independent Set, which is in NP.

      source
      theorem DescriptiveComplexity.vertexCover_NP_hard :
      NP.Hard VertexCover

      Vertex Cover is NP-hard: Independent Set, which is NP-hard, reduces to it.

      source
      theorem DescriptiveComplexity.vertexCover_NP_complete :
      NP.Complete VertexCover

      Vertex Cover is NP-complete.