⊕SAT and Mod_k-SAT: complete problems for the classes defined by one count

For a property R of a number, DescriptiveComplexity.CountingProblem.decide R C is the decision problem “R holds of the count of C”, and DescriptiveComplexity.countClass₁ R the class of the problems defined by R of one witness count: ⊕P for Odd, Mod_k P for “not a multiple of k”.

• The decision version of #SAT is complete for every such class (DescriptiveComplexity.decide_sharpSat_countClass₁_complete): membership is that #SAT is in #P, and hardness is the parsimonious Tseitin interpretation of DescriptiveComplexity.Problems.Sat.CountingHardness, which carries a witness count to a model count exactly and so carries any property of it.
• It transfers along parsimonious reductions (DescriptiveComplexity.countClass₁_complete_of_sharpP_parsimoniousComplete): the decision version of every parsimoniously #P-complete problem is complete for every such class. So ⊕SAT, ⊕3SAT, ⊕Clique, …, and the parity of the number of accepting runs of a machine, are ⊕P-complete; likewise for Mod_k P.
• The machine characterization (DescriptiveComplexity.mem_parityP_iff_le_parity_sharpNtmAccept): a problem is in ⊕P exactly when it reduces to the parity of the number of accepting runs of a nondeterministic polynomial-time machine, through the counting machine bridge of DescriptiveComplexity.Problems.Machine.CountingHardness.

The classical statements are Papadimitriou, Zachos 1982 for ⊕SAT and Valiant 1979 for the transfer: a parsimonious reduction preserves every property of the count.

The decision version of a counting problem

def DescriptiveComplexity.CountingProblem.decide {L : FirstOrder.Language} [L.IsRelational] (R : ℕ → Prop) (C : CountingProblem L) : DecisionProblem L

The decision version of a counting problem by a property R of numbers: does the count satisfy R?

Equations

• DescriptiveComplexity.CountingProblem.decide R C = { Holds := fun (A : Type) (inst : L.Structure A) => R (C.Count A), iso_invariant := ⋯ }

theorem DescriptiveComplexity.CountingProblem.decide_iff {L : FirstOrder.Language} [L.IsRelational] (R : ℕ → Prop) (C : CountingProblem L) (A : Type) [L.Structure A] : (decide R C).Holds A ↔ R (C.Count A)

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.countClass₁ (R : ℕ → Prop) : ComplexityClass

The class of the problems defined by the property R of one witness count.

Equations

• DescriptiveComplexity.countClass₁ R = DescriptiveComplexity.countClass (fun (x x_1 : ℕ) => True) fun (c x : ℕ) => R c

def DescriptiveComplexity.RelOrderedParsimoniousReduction.decide {L : FirstOrder.Language} [L.IsRelational] {L' : FirstOrder.Language} [L'.IsRelational] (R : ℕ → Prop) {C : CountingProblem L} {D : CountingProblem L'} (f : RelOrderedParsimoniousReduction C D) : RelOrderedFOReduction (CountingProblem.decide R C) (CountingProblem.decide R D)

A relativized parsimonious reduction is a relativized first-order reduction between the decision versions by any property: equal counts share every property.

Equations

• DescriptiveComplexity.RelOrderedParsimoniousReduction.decide R f = { Tag := f.Tag, tagFinite := ⋯, dim := f.dim, toRelInterpretation := f.toRelInterpretation, dom_nonempty := ⋯, correct := ⋯ }

def DescriptiveComplexity.OrderedParsimoniousReduction.decide {L : FirstOrder.Language} [L.IsRelational] {L' : FirstOrder.Language} [L'.IsRelational] (R : ℕ → Prop) {C : CountingProblem L} {D : CountingProblem L'} (f : OrderedParsimoniousReduction C D) : OrderedFOReduction (CountingProblem.decide R C) (CountingProblem.decide R D)

An ordered parsimonious reduction is an ordered first-order reduction between the decision versions by any property.

Equations

• DescriptiveComplexity.OrderedParsimoniousReduction.decide R f = { Tag := f.Tag, tagFinite := ⋯, tagNonempty := ⋯, dim := f.dim, toInterpretation := f.toInterpretation, correct := ⋯ }

The decision versions of #SAT

noncomputable def DescriptiveComplexity.CountDefinable.orderedReduction_decide_sharpSat {L : FirstOrder.Language} [L.IsRelational] (R : ℕ → Prop) {P : DecisionProblem L} (B : SOBlock) (φ : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence) (h : ∀ (A : Type) [inst : L.Structure A] [inst_1 : LinearOrder A] [Finite A] [Nonempty A], P.Holds A ↔ R (witnessCount B φ A)) : OrderedFOReduction P (CountingProblem.decide R SharpSAT)

Every problem defined by a property of one witness count reduces to the decision version of #SAT by that property: the parsimonious Tseitin interpretation.

Equations

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

theorem DescriptiveComplexity.decide_sharpSat_countClass₁_complete (R : ℕ → Prop) : (countClass₁ R).Complete (CountingProblem.decide R SharpSAT)

The decision version of #SAT by R is complete for the class of R.

theorem DescriptiveComplexity.countClass₁_complete_of_sharpP_parsimoniousComplete {L : FirstOrder.Language} [L.IsRelational] (R : ℕ → Prop) {C : CountingProblem L} (hC : SharpP.ParsimoniousComplete C) : (countClass₁ R).Complete (CountingProblem.decide R C)

Completeness transfers along parsimonious completeness: the decision version by R of every parsimoniously #P-complete problem is complete for the class of R.

⊕SAT and Mod_k-SAT

noncomputable def DescriptiveComplexity.ParitySAT : DecisionProblem FirstOrder.Language.sat

⊕SAT: the number of models of a CNF formula is odd.

Equations

• DescriptiveComplexity.ParitySAT = DescriptiveComplexity.CountingProblem.decide Odd DescriptiveComplexity.SharpSAT

noncomputable def DescriptiveComplexity.ModSAT (k : ℕ) : DecisionProblem FirstOrder.Language.sat

Mod_k-SAT: the number of models of a CNF formula is not a multiple of k.

Equations

• DescriptiveComplexity.ModSAT k = DescriptiveComplexity.CountingProblem.decide (fun (c : ℕ) => ¬k ∣ c) DescriptiveComplexity.SharpSAT

theorem DescriptiveComplexity.paritySat_parityP_complete : ParityP.Complete ParitySAT

⊕SAT is ⊕P-complete. Registered in the Lax archive as Lax175070.ParitySatComplete.paritySat_parityP_complete.

theorem DescriptiveComplexity.modSat_modP_complete (k : ℕ) : (ModP k).Complete (ModSAT k)

Mod_k-SAT is Mod_k P-complete. Registered in the Lax archive as Lax175070.ParitySatComplete.modSat_modP_complete.

theorem DescriptiveComplexity.parityP_complete_of_sharpP_parsimoniousComplete {L : FirstOrder.Language} [L.IsRelational] {C : CountingProblem L} (hC : SharpP.ParsimoniousComplete C) : ParityP.Complete (CountingProblem.decide Odd C)

The parity of every parsimoniously #P-complete problem is ⊕P-complete. Registered in the Lax archive as Lax175070.ParitySatComplete.parityP_complete_of_sharpP_parsimoniousComplete.

theorem DescriptiveComplexity.mem_parityP_iff_le_parity_sharpNtmAccept {L : FirstOrder.Language} [L.IsRelational] (P : DecisionProblem L) : ParityP.Mem P ↔ Nonempty (OrderedFOReduction P (CountingProblem.decide Odd SharpNTMAccept))

The machine characterization of ⊕P: a problem is in ⊕P exactly when it reduces to the parity of the number of accepting runs of a nondeterministic polynomial-time machine. Registered in the Lax archive as Lax175070.ParitySatComplete.mem_parityP_iff_le_parity_sharpNtmAccept.

theorem DescriptiveComplexity.mem_modP_iff_le_mod_sharpNtmAccept {L : FirstOrder.Language} [L.IsRelational] (k : ℕ) (P : DecisionProblem L) : (ModP k).Mem P ↔ Nonempty (OrderedFOReduction P (CountingProblem.decide (fun (c : ℕ) => ¬k ∣ c) SharpNTMAccept))

The machine characterization of Mod_k P. Registered in the Lax archive as Lax175070.ParitySatComplete.mem_modP_iff_le_mod_sharpNtmAccept.

theorem DescriptiveComplexity.modP_complete_of_sharpP_parsimoniousComplete {L : FirstOrder.Language} [L.IsRelational] (k : ℕ) {C : CountingProblem L} (hC : SharpP.ParsimoniousComplete C) : (ModP k).Complete (CountingProblem.decide (fun (c : ℕ) => ¬k ∣ c) C)

The residue of every parsimoniously #P-complete problem is Mod_k P-complete. Registered in the Lax archive as Lax175070.ParitySatComplete.modP_complete_of_sharpP_parsimoniousComplete.