#BIS and #PP2DNF: counting the independent sets of a bipartite graph

A bipartite graph is given with its bipartition (FirstOrder.Language.bipGraph): a unary relation marks the left side, the right side is the rest, and only the edges from a left vertex to a right vertex are read. DescriptiveComplexity.SharpBIS is the number of its independent sets, the sets with no edge from a left member to a right member.

Like the count of all the independent sets of a graph, it is one-call #P-complete and not parsimoniously (DescriptiveComplexity.sharpBIS_sharpP_oneCallComplete). Hardness is from that problem, by stretching (DescriptiveComplexity.stretchInterp): every edge is replaced by 2n paths of length two through new middle vertices, which form the left side. An independent set of the result is any set S of vertices and any set of middles of the edges with no endpoint in S, so the oracle answers ∑ S, (2 ^ (2n)) ^ e(S), and the remainder modulo 2 ^ (2n) counts the sets with e(S) = 0, the complements of the independent sets (DescriptiveComplexity.card_stretchIndep_mod).

DescriptiveComplexity.SharpPP2DNF is the same data read as a formula: one variable per vertex and one term x ∧ y per edge, a partitioned positive 2-DNF. Its models are the sets of vertices that are not independent, so #BIS + #PP2DNF = 2 ^ n (DescriptiveComplexity.sharpBIS_add_sharpPP2DNF) and it is one-call #P-complete as well (DescriptiveComplexity.sharpPP2DNF_sharpP_oneCallComplete).

In the literature these are the two partitioned positive problems. The independent sets of a bipartite graph are the complements of its vertex covers, i.e., of the models of ⋀ (x ∨ y) over its edges, so #BIS is #PP2CNF, whose #P-hardness is due to Provan and Ball 1983; #PP2DNF is its dual. This is the form in which Dalvi and Suciu 2012 (Theorem 5.1 there, and Proposition 5.2 for the query R(x), S(x, y), T(y)) use it. The hardness proved here is by a different route, with one oracle call, and is not taken from those papers.

The interpretation is three-dimensional and relativized: the vertices are the diagonal triples of one tag, and each of two other tags carries the triples (u, v, i) with u – v an edge.

@[reducible, inline]

abbrev FirstOrder.Language.bgEdge : Language.bipGraph.Relations 2

edge a b: there is an edge between a and b; read for a on the left and b on the right.

Equations

• FirstOrder.Language.bgEdge = FirstOrder.Language.bipGraphRel.edge

instance FirstOrder.Language.instIsRelationalBipGraph : Language.bipGraph.IsRelational

def FirstOrder.Language.bipGraph : Language

The relational language of bipartite graphs given with their bipartition.

Equations

• FirstOrder.Language.bipGraph = { Functions := fun (x : ℕ) => Empty, Relations := FirstOrder.Language.bipGraphRel }

def FirstOrder.Language.instDecidableEqBipGraphRel.decEq {a✝ : ℕ} (x✝ x✝¹ : bipGraphRel a✝) : Decidable (x✝ = x✝¹)

Equations

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

@[reducible, inline]

abbrev FirstOrder.Language.bgLeft : Language.bipGraph.Relations 1

left a: the vertex a is on the left side.

Equations

• FirstOrder.Language.bgLeft = FirstOrder.Language.bipGraphRel.left

@[instance_reducible]

instance FirstOrder.Language.instDecidableEqBipGraphRel {a✝ : ℕ} : DecidableEq (bipGraphRel a✝)

Equations

• FirstOrder.Language.instDecidableEqBipGraphRel = FirstOrder.Language.instDecidableEqBipGraphRel.decEq

inductive FirstOrder.Language.bipGraphRel : ℕ → Type

The relation symbols of the language.

• left : bipGraphRel 1

  left a: the vertex a is on the left side.

• edge : bipGraphRel 2

  edge a b: there is an edge between a and b; read for a on the left and b on the right.

def DescriptiveComplexity.BGLeft {A : Type} [FirstOrder.Language.bipGraph.Structure A] (a0 : A) : Prop

left a: the vertex a is on the left side.

Equations

• DescriptiveComplexity.BGLeft a0 = FirstOrder.Language.Structure.RelMap FirstOrder.Language.bgLeft ![a0]

def DescriptiveComplexity.BGEdge {A : Type} [FirstOrder.Language.bipGraph.Structure A] (a0 a1 : A) : Prop

edge a b: there is an edge between a and b; read for a on the left and b on the right.

Equations

• DescriptiveComplexity.BGEdge a0 a1 = FirstOrder.Language.Structure.RelMap FirstOrder.Language.bgEdge ![a0, a1]

The problem

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

The set S is independent in a bipartite graph: no edge goes from a left member of S to a right member of S.

Equations

• DescriptiveComplexity.BipIndep A S = ∀ (x y : A), S x → S y → DescriptiveComplexity.BGLeft x → ¬DescriptiveComplexity.BGLeft y → ¬DescriptiveComplexity.BGEdge x y

@[reducible, inline]

abbrev DescriptiveComplexity.bisSOLang : FirstOrder.Language

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

Equations

• DescriptiveComplexity.bisSOLang = FirstOrder.Language.bipGraph.sum DescriptiveComplexity.satAssignBlock.lang

@[reducible, inline]

abbrev DescriptiveComplexity.kbLeftSym : bisSOLang.Relations 1

The left-side symbol, in the kernel vocabulary.

Equations

• DescriptiveComplexity.kbLeftSym = Sum.inl FirstOrder.Language.bgLeft

@[reducible, inline]

abbrev DescriptiveComplexity.kbEdgeSym : bisSOLang.Relations 2

The edge symbol, in the kernel vocabulary.

Equations

• DescriptiveComplexity.kbEdgeSym = Sum.inl FirstOrder.Language.bgEdge

@[reducible, inline]

abbrev DescriptiveComplexity.kbSetSym : bisSOLang.Relations 1

The guessed set, in the kernel vocabulary.

Equations

• DescriptiveComplexity.kbSetSym = Sum.inr DescriptiveComplexity.satNuSym

noncomputable def DescriptiveComplexity.bisKernel : bisSOLang.Sentence

The first-order kernel: no edge from a left member to a right member.

Equations

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

theorem DescriptiveComplexity.card_bipIndep_eq_witnessCount (A : Type) [FirstOrder.Language.bipGraph.Structure A] : Nat.card { S : A → Prop // BipIndep A S } = witnessCount satAssignBlock bisKernel A

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

noncomputable def DescriptiveComplexity.SharpBIS : CountingProblem FirstOrder.Language.bipGraph

#BIS: the number of independent sets of a bipartite graph.

Equations

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

The stretched graph

noncomputable def DescriptiveComplexity.stretchMidDom : (FirstOrder.Language.graph.sum FirstOrder.Language.order).Formula (Fin 3)

Domain of the middle vertices: the triples whose first two coordinates are the ends of an edge.

Equations

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

noncomputable def DescriptiveComplexity.stretchInterp : RelFOInterpretation (FirstOrder.Language.graph.sum FirstOrder.Language.order) FirstOrder.Language.bipGraph (Option Bool) 3

The stretched graph, drawn in triples: the tag none carries the vertices, on the diagonal, and each tag some b the middle vertices (u, v, i) of the edge u – v, adjacent to u and to v. The middle vertices are the left side.

Equations

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

theorem DescriptiveComplexity.sharpBIS_stretch {A : Type} [FirstOrder.Language.graph.Structure A] [LinearOrder A] : SharpBIS.Count (stretchInterp.MapRel A) = Nat.card { T : A ⊕ (EdgePair fun (a b : A) => FirstOrder.Language.Structure.RelMap FirstOrder.Language.adj ![a, b]) × Bool × A → Prop // StretchIndep (fun (a b : A) => FirstOrder.Language.Structure.RelMap FirstOrder.Language.adj ![a, b]) T }

The independent sets of the interpreted bipartite graph are those of the stretched graph.

The reduction

noncomputable def DescriptiveComplexity.sharpAllIndependentSets_oneCall_sharpBIS : OneCallReduction SharpAllIndependentSets SharpBIS

Counting the independent sets of a graph reduces to #BIS with one call: the number of independent sets of the stretched graph, modulo 2 ^ (2n), is the number of independent sets of the graph.

Equations

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

theorem DescriptiveComplexity.sharpBIS_sharpP_oneCallHard : SharpP.OneCallHard SharpBIS

#BIS is one-call #P-hard.

theorem DescriptiveComplexity.sharpBIS_sharpP_oneCallComplete : SharpP.OneCallComplete SharpBIS

#BIS is one-call #P-complete: counting the independent sets of a bipartite graph is in #P, and every problem of #P reduces to it with one call. Registered in the Lax archive as Lax859101.BipartiteComplete.sharpBIS_sharpP_oneCallComplete.

#PP2DNF

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

The set S of true variables satisfies the partitioned positive 2-DNF formula of a bipartite graph – one variable per vertex, one term x ∧ y per edge from a left vertex x to a right vertex y: some term has both its variables true.

Equations

• DescriptiveComplexity.Pp2dnfModel A S = ∃ (x : A) (y : A), S x ∧ S y ∧ DescriptiveComplexity.BGLeft x ∧ ¬DescriptiveComplexity.BGLeft y ∧ DescriptiveComplexity.BGEdge x y

theorem DescriptiveComplexity.card_pp2dnfModel_eq_witnessCount (A : Type) [FirstOrder.Language.bipGraph.Structure A] : Nat.card { S : A → Prop // Pp2dnfModel A S } = witnessCount satAssignBlock (FirstOrder.Language.BoundedFormula.not bisKernel) A

The number of models of the formula is the number of witnesses of the negated kernel of #BIS.

noncomputable def DescriptiveComplexity.SharpPP2DNF : CountingProblem FirstOrder.Language.bipGraph

#PP2DNF: the number of satisfying assignments of a partitioned positive 2-DNF formula, presented as its bipartite graph.

Equations

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

theorem DescriptiveComplexity.sharpBIS_add_sharpPP2DNF (A : Type) [FirstOrder.Language.bipGraph.Structure A] [Finite A] : SharpBIS.Count A + SharpPP2DNF.Count A = 2 ^ Nat.card A

Independent sets and models share out the sets of vertices: #BIS + #PP2DNF = 2 ^ n.

noncomputable def DescriptiveComplexity.sharpBIS_oneCall_sharpPP2DNF : OneCallReduction SharpBIS SharpPP2DNF

#BIS reduces to #PP2DNF with one call, on the same instance: #BIS = 2 ^ n - #PP2DNF.

Equations

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

theorem DescriptiveComplexity.sharpPP2DNF_sharpP_oneCallHard : SharpP.OneCallHard SharpPP2DNF

#PP2DNF is one-call #P-hard.

theorem DescriptiveComplexity.sharpPP2DNF_sharpP_oneCallComplete : SharpP.OneCallComplete SharpPP2DNF

#PP2DNF is one-call #P-complete. Registered in the Lax archive as Lax859101.BipartiteComplete.sharpPP2DNF_sharpP_oneCallComplete.