#DNF is #P-complete

The reduction of #SAT to #DNF, as the strong subtractive reduction it is in Durand, Hermann, Kolaitis 2005 (Proposition 3.4): the number of models of a CNF formula is the number of models of a tautology over its variables, minus the number of models of its negation, and the models of the negation are models of the tautology. DescriptiveComplexity.Problems.Sat.CountingDnf has the same reduction with one oracle call, the count at the tautology being known; here both instances are drawn, and the statement is the stronger one, since #P is closed under subtractive reductions (DescriptiveComplexity.sharpDnf_sharpP_complete).

The two instances have to share their universe, and a tautology over n variables needs n + 1 terms when every element is a variable, so the universe is doubled:

• DescriptiveComplexity.dnfSubInterp, the subtrahend, carries the sign swap of the formula on one tag and nothing on the other;
• DescriptiveComplexity.dnfMinInterp, the minuend, has the term x on one tag and the term ¬x on the other for each variable x, and an empty term for each element that is not a variable.

The semantic content is two lemmas about a formula embedded in a larger universe, DescriptiveComplexity.dnfModel_embed_swap_iff (De Morgan) and DescriptiveComplexity.card_embedded_sets.

Formulas embedded in a larger universe

theorem DescriptiveComplexity.dnfModel_embed_swap_iff {A B : Type} [FirstOrder.Language.sat.Structure A] [FirstOrder.Language.sat.Structure B] {ι : A → B} (hι : Function.Injective ι) (hcl : ∀ (y : B), FirstOrder.Language.Structure.RelMap FirstOrder.Language.satIsClause ![y] ↔ ∃ (c : A), y = ι c ∧ FirstOrder.Language.Structure.RelMap FirstOrder.Language.satIsClause ![c]) (hpos : ∀ (y z : B), FirstOrder.Language.Structure.RelMap FirstOrder.Language.satPosIn ![y, z] ↔ ∃ (c : A) (x : A), y = ι c ∧ z = ι x ∧ FirstOrder.Language.Structure.RelMap FirstOrder.Language.satNegIn ![c, x]) (hneg : ∀ (y z : B), FirstOrder.Language.Structure.RelMap FirstOrder.Language.satNegIn ![y, z] ↔ ∃ (c : A) (x : A), y = ι c ∧ z = ι x ∧ FirstOrder.Language.Structure.RelMap FirstOrder.Language.satPosIn ![c, x]) (μ : B → Prop) : DnfModel B μ ↔ (∀ (y : B), μ y → ∃ (a : A), y = ι a ∧ SatOccurs A a) ∧ ¬SatModel A fun (a : A) => μ (ι a)

De Morgan's law, for an embedded formula: if B carries, on the image of ι, the sign swap of the CNF formula A, and nothing elsewhere, then the models of B read as a DNF formula are the sets of images of variables of A that are not models of A.

theorem DescriptiveComplexity.card_embedded_sets {A B : Type} {ι : A → B} (hι : Function.Injective ι) (p : A → Prop) (R : (A → Prop) → Prop) : Nat.card { μ : B → Prop // (∀ (y : B), μ y → ∃ (a : A), y = ι a ∧ p a) ∧ R fun (a : A) => μ (ι a) } = Nat.card { ν : A → Prop // (∀ (a : A), ν a → p a) ∧ R ν }

Sets of images of elements satisfying p, with a condition on their preimage, are as many as the sets of elements satisfying p with that condition.

The two instances

noncomputable def DescriptiveComplexity.dnfSubInterp : FOInterpretation (FirstOrder.Language.sat.sum FirstOrder.Language.order) FirstOrder.Language.sat Bool 1

The subtrahend: the sign swap of the formula on the tag false, and nothing on the tag true.

Equations

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

noncomputable def DescriptiveComplexity.dnfMinInterp : FOInterpretation (FirstOrder.Language.sat.sum FirstOrder.Language.order) FirstOrder.Language.sat Bool 1

The minuend: a tautology over the same variables. Each variable x gives the term x on the tag false and the term ¬x on the tag true, and an element that is not a variable gives the empty term on the tag true.

Equations

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

def DescriptiveComplexity.dnfPt {A : Type} (a : A) : Bool × (Fin 1 → A)

The image of an element of the formula in the two instances: the point of tag false.

Equations

• DescriptiveComplexity.dnfPt a = (false, fun (x : Fin 1) => a)

theorem DescriptiveComplexity.dnfPt_injective {A : Type} : Function.Injective dnfPt

theorem DescriptiveComplexity.eq_dnfPt {A : Type} (z : Bool × (Fin 1 → A)) {a : A} (h1 : z.1 = false) (h2 : a = z.2 0) : z = dnfPt a

The reduction

theorem DescriptiveComplexity.sharpSat_subtractive_sharpDnf : SubtractiveReducible SharpSAT SharpDNF

#SAT reduces to #DNF by a subtractive reduction. Registered in the Lax archive as Lax859101.DnfComplete.sharpSat_subtractive_sharpDnf.

theorem DescriptiveComplexity.sharpDnf_sharpP_hard : SharpP.Hard SharpDNF

#DNF is #P-hard: every problem of #P reduces to #SAT parsimoniously, and #SAT to #DNF by a strong subtractive reduction.

theorem DescriptiveComplexity.sharpDnf_sharpP_complete : SharpP.Complete SharpDNF

#DNF is #P-complete (Proposition 3.4 of Durand, Hermann, Kolaitis 2005): it is in #P, every problem of #P reduces to it by a subtractive reduction, and #P is closed under those. Registered in the Lax archive as Lax859101.DnfComplete.sharpDnf_sharpP_complete.