Counting classes, the class #P, and its relation to NP

A DescriptiveComplexity.CountingClass is to counting problems what a DescriptiveComplexity.ComplexityClass is to decision problems: a membership predicate and a hardness predicate, closed under reductions – here the parsimonious ones of DescriptiveComplexity.Counting, membership backward and hardness forward. As on the decision side, hardness also travels along the relativized reductions of DescriptiveComplexity.Counting.Relativized, whose target universe is definable, and hardness for a class is cofinality for those: a problem whose solutions span the universe can be hard in no other way.

Parsimonious hardness is not the hardness of the literature

The hardness predicate is named ParsimoniousHard, and completeness ParsimoniousComplete, never plain “hard” and “complete”, because they are strictly stronger than what “#P-hard” and “#P-complete” mean in the literature, where the reductions are polynomial-time Turing (or one oracle call followed by arithmetic). Counting the satisfying assignments of a DNF formula, or the independent sets of a graph, is #P-complete in that sense, and it is not parsimoniously #P-hard unless NP ⊆ PTIME (DescriptiveComplexity.NP_subset_PTIME_of_sharpP_parsimoniousHard): a parsimonious reduction preserves “the count is positive”, so it carries the hardness of the decision problem along, and these problems have an easy one. The unqualified names are left free for the weaker notion.

Parsimonious completeness is the notion under which completeness says something about the decision problem underneath and about approximability (Arenas, Muñoz, Riveros 2020).

The class DescriptiveComplexity.SharpP is defined by witness counting (DescriptiveComplexity.SharpPDefinable), as NP is defined by existential second-order definability.

Relation to NP

The decision problem underneath a counting problem is its support, “is the count positive?”. Three statements tie #P to NP through it:

• DescriptiveComplexity.mem_NP_iff_exists_sharpP_support: the problems of NP are exactly the supports of the problems of #P;
• DescriptiveComplexity.NP_hard_support_of_sharpP_parsimoniousHard: the support of a parsimoniously #P-hard problem is NP-hard;
• DescriptiveComplexity.NP_subset_PTIME_of_sharpP_parsimoniousHard: if a parsimoniously #P-hard problem has its support in PTIME, then NP ⊆ PTIME.

def DescriptiveComplexity.OrderedParsimoniousReduction.congrTarget {L L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {C : CountingProblem L} {D D' : CountingProblem L'} (h : ∀ (A : Type) [inst : L'.Structure A] [Finite A], D.Count A = D'.Count A) (g : OrderedParsimoniousReduction C D) : OrderedParsimoniousReduction C D'

Replacing the target of an ordered parsimonious reduction by a counting problem with the same values on finite structures.

Equations

• DescriptiveComplexity.OrderedParsimoniousReduction.congrTarget h g = { Tag := g.Tag, tagFinite := ⋯, tagNonempty := ⋯, dim := g.dim, toInterpretation := g.toInterpretation, correct := ⋯ }

structure DescriptiveComplexity.CountingClass : Type 1

An abstract counting class: a collection of counting problems (its Membership predicate) together with a ParsimoniousHardness predicate, closed under parsimonious reductions. Membership travels backward along them, hardness forward.

• Mem {L : FirstOrder.Language} [L.IsRelational] : CountingProblem L → Prop

  The counting problems belonging to the class. Use the notation C ∈ 𝒞.

• ParsimoniousHard {L : FirstOrder.Language} [L.IsRelational] : CountingProblem L → Prop

  The counting problems every problem of the class parsimoniously reduces to.

• mem_of_parsimonious {L L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {C : CountingProblem L} {D : CountingProblem L'} : ∀ (a : ParsimoniousReduction C D), self.Mem D → self.Mem C

  Membership travels backward along parsimonious reductions.

• parsimoniousHard_of_parsimonious {L L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {C : CountingProblem L} {D : CountingProblem L'} : ∀ (a : ParsimoniousReduction C D), self.ParsimoniousHard C → self.ParsimoniousHard D

  Parsimonious hardness travels forward along parsimonious reductions.

• mem_of_orderedParsimonious {L L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {C : CountingProblem L} {D : CountingProblem L'} : ∀ (a : OrderedParsimoniousReduction C D), self.Mem D → self.Mem C

  Membership travels backward along ordered parsimonious reductions.

• parsimoniousHard_of_orderedParsimonious {L L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {C : CountingProblem L} {D : CountingProblem L'} : ∀ (a : OrderedParsimoniousReduction C D), self.ParsimoniousHard C → self.ParsimoniousHard D

  Parsimonious hardness travels forward along ordered parsimonious reductions.

• parsimoniousHard_of_relOrderedParsimonious {L L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {C : CountingProblem L} {D : CountingProblem L'} : ∀ (a : RelOrderedParsimoniousReduction C D), self.ParsimoniousHard C → self.ParsimoniousHard D

  Parsimonious hardness travels forward along relativized ordered parsimonious reductions – the reductions with a definable target universe, needed for the problems whose solutions span it.

• mem_congr_finite {L : FirstOrder.Language} [L.IsRelational] {C D : CountingProblem L} : (∀ (A : Type) [inst : L.Structure A] [Finite A], C.Count A = D.Count A) → (self.Mem C ↔ self.Mem D)

  Membership only depends on the values of a counting problem on finite structures.

• parsimoniousHard_congr_finite {L : FirstOrder.Language} [L.IsRelational] {C D : CountingProblem L} : (∀ (A : Type) [inst : L.Structure A] [Finite A], C.Count A = D.Count A) → (self.ParsimoniousHard C ↔ self.ParsimoniousHard D)

  Parsimonious hardness, too, only depends on the finite instances.

def DescriptiveComplexity.«term_∈__1» : Lean.TrailingParserDescr

C ∈ 𝒞: the counting problem C belongs to the counting class 𝒞.

Equations

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

def DescriptiveComplexity.CountingClass.ofMem (Mem : {L₀ : FirstOrder.Language} → [inst : L₀.IsRelational] → CountingProblem L₀ → Prop) (mem_of_orderedParsimonious : ∀ {L₁ L₂ : FirstOrder.Language} [inst : L₁.IsRelational] [inst_1 : L₂.IsRelational] {C : CountingProblem L₁} {D : CountingProblem L₂} (a : OrderedParsimoniousReduction C D), Mem D → Mem C) (mem_congr_finite : ∀ {L₁ : FirstOrder.Language} [inst : L₁.IsRelational] {C D : CountingProblem L₁}, (∀ (A : Type) [inst_1 : L₁.Structure A] [Finite A], C.Count A = D.Count A) → (Mem C ↔ Mem D)) : CountingClass

The counting class with a given membership predicate, parsimonious hardness being cofinality for it: every member reduces to the problem, by a relativized ordered parsimonious reduction. Only the membership obligations have to be supplied.

Equations

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

def DescriptiveComplexity.CountingClass.ParsimoniousComplete (K : CountingClass) {L : FirstOrder.Language} [L.IsRelational] (C : CountingProblem L) : Prop

A counting problem is parsimoniously complete for a class if it belongs to it and every problem of the class parsimoniously reduces to it.

Equations

• K.ParsimoniousComplete C = (K.Mem C ∧ K.ParsimoniousHard C)

theorem DescriptiveComplexity.CountingClass.ParsimoniousComplete.mem (K : CountingClass) {L : FirstOrder.Language} [L.IsRelational] {C : CountingProblem L} (h : K.ParsimoniousComplete C) : K.Mem C

theorem DescriptiveComplexity.CountingClass.ParsimoniousComplete.parsimoniousHard (K : CountingClass) {L : FirstOrder.Language} [L.IsRelational] {C : CountingProblem L} (h : K.ParsimoniousComplete C) : K.ParsimoniousHard C

The class #P

noncomputable def DescriptiveComplexity.SharpP : CountingClass

The class #P: the counting problems that count the witnesses of an existential second-order sentence over ordered structures (Saluja, Subrahmanyam, Thakur 1995). It is closed under parsimonious reductions, and hardness for it is hardness under relativized ordered parsimonious reductions.

Equations

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

theorem DescriptiveComplexity.parsimoniousHard_sharpP_iff {L : FirstOrder.Language} [L.IsRelational] (C : CountingProblem L) : SharpP.ParsimoniousHard C ↔ ∀ {L'' : FirstOrder.Language} [inst : L''.IsRelational] (D : CountingProblem L''), SharpPDefinable D → Nonempty (RelOrderedParsimoniousReduction D C)

Parsimonious #P-hardness, unfolded: every #P-definable counting problem reduces to C by a relativized ordered parsimonious reduction.

Relation to NP

theorem DescriptiveComplexity.SharpPDefinable.support_sigmaSODefinable {L : FirstOrder.Language} [L.IsRelational] {C : CountingProblem L} (h : SharpPDefinable C) : SigmaSODefinable 1 C.support

The support of a #P-definable counting problem is Σ₁-definable: a count of witnesses is positive exactly when there is a witness, and the order the kernel reads is re-quantified by the order elimination of DescriptiveComplexity.sigmaSODefinable_of_orderPull.

theorem DescriptiveComplexity.support_mem_NP {L : FirstOrder.Language} [L.IsRelational] {C : CountingProblem L} (h : SharpP.Mem C) : NP.Mem C.support

The support of a problem of #P is in NP.

theorem DescriptiveComplexity.mem_NP_iff_exists_sharpP_support {L : FirstOrder.Language} [L.IsRelational] (P : DecisionProblem L) : NP.Mem P ↔ ∃ (C : CountingProblem L), SharpP.Mem C ∧ ∀ (A : Type) [inst : L.Structure A] [Finite A] [Nonempty A], C.support.Holds A ↔ P.Holds A

NP is the class of supports of #P: a decision problem is in NP exactly when it is, on nonempty finite structures, the question whether some counting problem of #P is positive – the counting problem being the number of witnesses of the Σ₁ definition. Registered in the Lax archive as Lax366625.SharpPAndNP.mem_NP_iff_exists_sharpP_support.

theorem DescriptiveComplexity.nonempty_relOrderedReduction_support_of_sharpP_parsimoniousHard {L : FirstOrder.Language} [L.IsRelational] {C : CountingProblem L} (hC : SharpP.ParsimoniousHard C) {L' : FirstOrder.Language} [L'.IsRelational] (Q : DecisionProblem L') (hQ : NP.Mem Q) : Nonempty (RelOrderedFOReduction Q C.support)

Every problem of NP reduces to the support of a parsimoniously #P-hard counting problem.

theorem DescriptiveComplexity.NP_hard_support_of_sharpP_parsimoniousHard {L : FirstOrder.Language} [L.IsRelational] {C : CountingProblem L} (hC : SharpP.ParsimoniousHard C) : NP.Hard C.support

The support of a parsimoniously #P-hard counting problem is NP-hard. Registered in the Lax archive as Lax366625.SharpPAndNP.NP_hard_support_of_sharpP_parsimoniousHard.

theorem DescriptiveComplexity.NP_subset_PTIME_of_sharpP_parsimoniousHard {L : FirstOrder.Language} [L.IsRelational] {C : CountingProblem L} (hC : SharpP.ParsimoniousHard C) (hsupp : PTIME.Mem C.support) : NP ⊆ PTIME

A parsimoniously #P-hard counting problem with an easy decision version collapses NP into PTIME. This is why the counting problems whose support is in PTIME – satisfying assignments of a DNF or of a monotone 2-CNF formula, independent sets, worlds of a probabilistic database satisfying a monotone query – are not parsimoniously #P-complete unless NP ⊆ PTIME. Registered in the Lax archive as Lax366625.SharpPAndNP.NP_subset_PTIME_of_sharpP_parsimoniousHard.