Counting all the independent sets of a graph

DescriptiveComplexity.SharpAllIndependentSets is the number of independent sets of a graph, of every size, on the plain vocabulary of graphs. A graph always has one, the empty set, so the problem is not parsimoniously #P-hard unless P = NP; it is one-call #P-complete (DescriptiveComplexity.sharpAllIndependentSets_sharpP_oneCallComplete).

Hardness is from DescriptiveComplexity.SharpIndependentSet, which counts the independent sets of exactly the threshold size and is parsimoniously complete. The reduction (DescriptiveComplexity.pendInterp) attaches n pendant leaves to each of the n vertices; an independent set of the result is an independent set S of the graph and any set of leaves of the vertices outside S, so the answer of the oracle is ∑ S, (2 ^ n) ^ (n - |S|), and the number of independent sets of size k is its digit of rank n - k in base 2 ^ n (DescriptiveComplexity.card_indepSet_pend_digit, in DescriptiveComplexity.Problems.CliqueFamily.Pendant). The post-processing term is that digit, oracle / 2 ^ (n * (n - k)) % 2 ^ n: the number n - k is the number of unmarked elements, a definable cardinality. This is the first reduction of the library to use a quotient and a remainder.

The interpretation is two-dimensional and relativized: the vertices are the diagonal pairs of one tag, the leaves all the pairs of the other.

The problem

@[reducible, inline]

abbrev DescriptiveComplexity.indepSOLang : FirstOrder.Language

The vocabulary of the kernel: graphs with one unary relation variable.

Equations

• DescriptiveComplexity.indepSOLang = FirstOrder.Language.graph.sum DescriptiveComplexity.satAssignBlock.lang

@[reducible, inline]

abbrev DescriptiveComplexity.kisAdjSym : indepSOLang.Relations 2

The adjacency symbol, in the kernel vocabulary.

Equations

• DescriptiveComplexity.kisAdjSym = Sum.inl FirstOrder.Language.adj

@[reducible, inline]

abbrev DescriptiveComplexity.kisSetSym : indepSOLang.Relations 1

The guessed set, in the kernel vocabulary.

Equations

• DescriptiveComplexity.kisSetSym = Sum.inr DescriptiveComplexity.satNuSym

noncomputable def DescriptiveComplexity.indepKernel : indepSOLang.Sentence

The first-order kernel: no two distinct elements of the set are adjacent.

Equations

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

theorem DescriptiveComplexity.card_indepSet_eq_witnessCount (A : Type) [FirstOrder.Language.graph.Structure A] : Nat.card { S : A → Prop // IndepSet (fun (x y : A) => FirstOrder.Language.Structure.RelMap FirstOrder.Language.adj ![x, y]) S } = witnessCount satAssignBlock indepKernel A

The number of independent sets of a graph is the number of witnesses of the kernel.

noncomputable def DescriptiveComplexity.SharpAllIndependentSets : CountingProblem FirstOrder.Language.graph

#Independent Sets, of all sizes: the number of independent sets of a graph.

Equations

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

theorem DescriptiveComplexity.sharpAllIndependentSets_apply (A : Type) [FirstOrder.Language.graph.Structure A] : SharpAllIndependentSets.Count A = Nat.card { S : A → Prop // IndepSet (fun (x y : A) => FirstOrder.Language.Structure.RelMap FirstOrder.Language.adj ![x, y]) S }

The graph with pendant leaves

noncomputable def DescriptiveComplexity.pendInterp : RelFOInterpretation (FirstOrder.Language.markedGraph.sum FirstOrder.Language.order) FirstOrder.Language.graph Bool 2

The graph with pendant leaves, drawn in pairs: the tag false carries the vertices, on the diagonal, and the tag true the leaves, the leaf (a, i) being adjacent to the vertex a alone.

Equations

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

noncomputable def DescriptiveComplexity.mgUnmarkedAt {α : Type} (x : α) : FirstOrder.Language.markedGraph.Formula α

“x is not marked.”

Equations

• DescriptiveComplexity.mgUnmarkedAt x = FirstOrder.Language.BoundedFormula.not (FirstOrder.Language.mgMarked.formula₁ (FirstOrder.Language.var x))

noncomputable def DescriptiveComplexity.unmarkedCount : PolyTerm FirstOrder.Language.markedGraph

The number of unmarked elements, as a polynomial term.

Equations

• DescriptiveComplexity.unmarkedCount = DescriptiveComplexity.PolyTerm.count (FirstOrder.Language.LHom.sumInl.onFormula (DescriptiveComplexity.mgUnmarkedAt 0))

theorem DescriptiveComplexity.eval_unmarkedCount {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] : PolyTerm.eval A unmarkedCount = Nat.card { v : A // ¬MGMarked v }

theorem DescriptiveComplexity.sharpAllIndependentSets_pend {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] : SharpAllIndependentSets.Count (pendInterp.MapRel A) = Nat.card { T : A ⊕ A × A → Prop // IndepSet (pendAdj fun (a b : A) => MGAdj a b) T }

The independent sets of the interpreted graph are those of the graph with pendant leaves.

The reduction

noncomputable def DescriptiveComplexity.sharpIndependentSet_oneCall_sharpAllIndependentSets : OneCallReduction SharpIndependentSet SharpAllIndependentSets

#Independent Set reduces to counting all the independent sets, with one call: in the graph with n pendant leaves at each of its n vertices, the independent sets of size k of the graph are counted by the digit of rank n - k of the number of independent sets, in base 2 ^ n.

Equations

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

theorem DescriptiveComplexity.sharpAllIndependentSets_sharpP_oneCallHard : SharpP.OneCallHard SharpAllIndependentSets

Counting all the independent sets is one-call #P-hard.

theorem DescriptiveComplexity.sharpAllIndependentSets_sharpP_oneCallComplete : SharpP.OneCallComplete SharpAllIndependentSets

Counting all the independent sets of a graph is one-call #P-complete. Registered in the Lax archive as Lax859101.AllSetsComplete.sharpAllIndependentSets_sharpP_oneCallComplete.