#Independent Set and #Vertex Cover

The counting versions of the two other problems of the clique family, each counting the solutions of exactly the threshold size:

• DescriptiveComplexity.SharpIndependentSet: the independent sets with as many vertices as the marked set;
• DescriptiveComplexity.SharpVertexCover: the vertex covers with as many vertices as the marked set.

Both are parsimoniously #P-complete (DescriptiveComplexity.sharpIndependentSet_sharpP_parsimoniousComplete, DescriptiveComplexity.sharpVertexCover_sharpP_parsimoniousComplete), and nothing has to be built for it: the two interpretations of DescriptiveComplexity.Problems.CliqueFamily.Reductions are parsimonious as they stand. Complementing the edges turns the cliques of a size into the independent sets of that size, the same sets; complementing the marked set turns the vertex covers of the threshold size into the independent sets of the complementary size, by complementation (DescriptiveComplexity.coverComplEquiv). Membership in #P travels backward along the same reductions, down to the monotone bijection of #Clique.

Counting the covers of size at most the threshold would be a different problem. The support of the exact count is Vertex Cover all the same, a cover smaller than the threshold extending to one of exactly that size (DescriptiveComplexity.sharpVertexCover_support_iff).

The generic properties

def DescriptiveComplexity.CliqueOfSizeOn {A : Type} (Adjp : A → A → Prop) (Kp S : A → Prop) : Prop

The set S is pairwise Adjp-related off the diagonal and has exactly as many elements as the Kp-marked set.

Equations

• DescriptiveComplexity.CliqueOfSizeOn Adjp Kp S = ((∀ (x y : A), S x → S y → x ≠ y → Adjp x y) ∧ {x : A | S x}.ncard = {x : A | Kp x}.ncard)

def DescriptiveComplexity.CoverOfSizeOn {A : Type} (Adjp : A → A → Prop) (Kp C : A → Prop) : Prop

The set C meets every off-diagonal Adjp-edge and has exactly as many elements as the Kp-marked set.

Equations

• DescriptiveComplexity.CoverOfSizeOn Adjp Kp C = ((∀ (x y : A), x ≠ y → Adjp x y → C x ∨ C y) ∧ {x : A | C x}.ncard = {x : A | Kp x}.ncard)

def DescriptiveComplexity.cliqueOfSizeEquiv {A B : Type} (u : B ≃ A) {AdjB : B → B → Prop} {KB : B → Prop} {AdjA : A → A → Prop} {KA : A → Prop} (hadj : ∀ (b b' : B), b ≠ b' → (AdjB b b' ↔ AdjA (u b) (u b'))) (hK : ∀ (b : B), KB b ↔ KA (u b)) : { S : B → Prop // Finite B ∧ CliqueOfSizeOn AdjB KB S } ≃ { S : A → Prop // Finite A ∧ CliqueOfSizeOn AdjA KA S }

The sets of the threshold size transport along an equivalence commuting with the adjacency predicates off the diagonal and with the marks.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.ncard_not_eq_iff {A : Type} [Finite A] (s t : A → Prop) : {x : A | ¬s x}.ncard = {x : A | ¬t x}.ncard ↔ {x : A | s x}.ncard = {x : A | t x}.ncard

On a finite universe, two sets have the same size iff their complements do.

def DescriptiveComplexity.coverComplEquiv {A : Type} (Adjp : A → A → Prop) (Kp : A → Prop) : { C : A → Prop // Finite A ∧ CoverOfSizeOn Adjp Kp C } ≃ { S : A → Prop // Finite A ∧ CliqueOfSizeOn (fun (x y : A) => ¬Adjp x y) (fun (x : A) => ¬Kp x) S }

The covers of the threshold size are the complements of the independent sets of the complementary size.

Equations

• One or more equations did not get rendered due to their size.

The two counting problems

def DescriptiveComplexity.IndepOfSize (A : Type) [FirstOrder.Language.markedGraph.Structure A] (S : A → Prop) : Prop

The set S is an independent set with exactly as many vertices as the marked set, in a finite marked graph.

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.CoverOfSize (A : Type) [FirstOrder.Language.markedGraph.Structure A] (C : A → Prop) : Prop

The set C is a vertex cover with exactly as many vertices as the marked set, in a finite marked graph.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.SharpIndependentSet : CountingProblem FirstOrder.Language.markedGraph

#Independent Set: the number of independent sets with exactly as many vertices as the marked set.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.SharpVertexCover : CountingProblem FirstOrder.Language.markedGraph

#Vertex Cover: the number of vertex covers with exactly as many vertices as the marked set.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.sharpIndependentSet_apply (A : Type) [FirstOrder.Language.markedGraph.Structure A] : SharpIndependentSet.Count A = Nat.card { S : A → Prop // IndepOfSize A S }

theorem DescriptiveComplexity.sharpIndependentSet_support_iff (A : Type) [FirstOrder.Language.markedGraph.Structure A] [Finite A] : SharpIndependentSet.support.Holds A ↔ IndependentSet.Holds A

The support of #Independent Set is Independent Set. Registered in the Lax archive as Lax280166.IndependentSetComplete.sharpIndependentSet_support_iff.

theorem DescriptiveComplexity.sharpVertexCover_support_iff (A : Type) [FirstOrder.Language.markedGraph.Structure A] [Finite A] : SharpVertexCover.support.Holds A ↔ VertexCover.Holds A

The support of #Vertex Cover is Vertex Cover: a cover at most as large as the marked set extends to one of exactly that size. Registered in the Lax archive as Lax280166.VertexCoverComplete.sharpVertexCover_support_iff.

The interpretations, for counting

theorem DescriptiveComplexity.sharpIndependentSet_complEdge_map (A : Type) [FirstOrder.Language.markedGraph.Structure A] : SharpIndependentSet.Count (complEdgeInterp.Map A) = SharpClique.Count A

The independent sets of the complement graph are the cliques.

theorem DescriptiveComplexity.sharpVertexCover_complMark_map (A : Type) [FirstOrder.Language.markedGraph.Structure A] : SharpVertexCover.Count (complMarkInterp.Map A) = SharpIndependentSet.Count A

The vertex covers of the threshold size, the marked set being complemented, are the complements of the independent sets of the threshold size.

The reductions and the completeness theorems

noncomputable def DescriptiveComplexity.sharpClique_parsimonious_sharpIndependentSet : ParsimoniousReduction SharpClique SharpIndependentSet

#Clique reduces parsimoniously to #Independent Set, by complementing the edges.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.sharpIndependentSet_parsimonious_sharpVertexCover : ParsimoniousReduction SharpIndependentSet SharpVertexCover

#Independent Set reduces parsimoniously to #Vertex Cover, by complementing the marked set.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.sharpIndependentSet_sharpP_parsimoniousHard : SharpP.ParsimoniousHard SharpIndependentSet

#Independent Set is parsimoniously #P-hard.

theorem DescriptiveComplexity.sharpIndependentSet_sharpP_parsimoniousComplete : SharpP.ParsimoniousComplete SharpIndependentSet

#Independent Set is parsimoniously #P-complete, counting the independent sets of exactly the threshold size. Registered in the Lax archive as Lax280166.IndependentSetComplete.sharpIndependentSet_sharpP_parsimoniousComplete.

theorem DescriptiveComplexity.sharpIndependentSet_sharpP_complete : SharpP.Complete SharpIndependentSet

SharpIndependentSet is #P-complete: parsimoniously, hence under subtractive reductions.

theorem DescriptiveComplexity.sharpVertexCover_sharpP_parsimoniousHard : SharpP.ParsimoniousHard SharpVertexCover

#Vertex Cover is parsimoniously #P-hard.

theorem DescriptiveComplexity.sharpVertexCover_sharpP_parsimoniousComplete : SharpP.ParsimoniousComplete SharpVertexCover

#Vertex Cover is parsimoniously #P-complete, counting the vertex covers of exactly the threshold size. Registered in the Lax archive as Lax280166.VertexCoverComplete.sharpVertexCover_sharpP_parsimoniousComplete.

theorem DescriptiveComplexity.sharpVertexCover_sharpP_complete : SharpP.Complete SharpVertexCover

SharpVertexCover is #P-complete: parsimoniously, hence under subtractive reductions.