#DNF: counting the models of a DNF formula #

The number of models of a formula in disjunctive normal form, on the vocabulary of SAT read disjunctively as for DescriptiveComplexity.TAUT: a model is a set of variables of the formula making every literal of some term true (DescriptiveComplexity.DnfModel).

Deciding whether a DNF formula has a model is easy – it has one exactly when some term contains no variable both positively and negatively – so #DNF is not parsimoniously #P-hard unless P = NP. It is the first problem of the catalog that is not parsimoniously complete:

DescriptiveComplexity.sharpDnf_mem_sharpP: the models are the witnesses of an existential second-order sentence;
DescriptiveComplexity.sharpSat_oneCall_sharpDnf: by De Morgan's law, the assignments that are not models of a CNF formula are the models of the DNF formula obtained by negating every literal (DescriptiveComplexity.dnfModel_swap_iff), and there are 2 ^ n assignments of the n variables of the formula in all. So #SAT(φ) = 2 ^ n - #DNF(¬φ): one call, at the sign swap DescriptiveComplexity.swapSignInterp, and a subtraction from a power of two whose exponent is a definable count;
DescriptiveComplexity.sharpDnf_sharpP_oneCallComplete: #DNF is one-call #P-complete.

This is the reduction of Durand, Hermann, Kolaitis 2005 (Proposition 3.4), where it is the example of a strong subtractive reduction: the difference of the counts at a tautology and at the negated formula, the models of the second being among those of the first. So #DNF is also complete under subtractive reductions, a notion under which #P is closed: that stronger statement is DescriptiveComplexity.sharpDnf_sharpP_complete, in DescriptiveComplexity.Problems.Sat.CountingDnfSubtractive.

Models of a DNF formula #

source

def DescriptiveComplexity.DnfModel (A : Type) [FirstOrder.Language.sat.Structure A] (ν : A → Prop) :

Prop

The set ν of true variables is a model of the DNF formula: it makes every literal of some term true, and consists of variables of the formula.

Equations

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

Instances For

Dependency graph

The kernel #

source

noncomputable def DescriptiveComplexity.dnfTermKernel :

satSOLang.Sentence

Kernel conjunct: some term has all its literals true.

Equations

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

Instances For

Dependency graph

source

noncomputable def DescriptiveComplexity.sharpDnfKernel :

satSOLang.Sentence

The first-order kernel of #DNF: some term is true, and the truth assignment only holds of variables of the formula.

Equations

DescriptiveComplexity.sharpDnfKernel = DescriptiveComplexity.dnfTermKernel ⊓ DescriptiveComplexity.satVarKernel

Instances For

Dependency graph

The counting problem #

source

theorem DescriptiveComplexity.card_dnfModel_eq_witnessCount (A : Type) [FirstOrder.Language.sat.Structure A] :

Nat.card { ν : A → Prop // DnfModel A ν } = witnessCount satAssignBlock sharpDnfKernel A

The number of models of a DNF formula is the number of witnesses of the kernel of #DNF.

Dependency graph

source

noncomputable def DescriptiveComplexity.SharpDNF :

CountingProblem FirstOrder.Language.sat

#DNF: the number of models of a DNF formula.

Equations

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

Instances For

Dependency graph

source

theorem DescriptiveComplexity.sharpDnf_mem_sharpP :

SharpP.Mem SharpDNF

#DNF is in #P: the models of a DNF formula are the witnesses of an existential second-order sentence.

Dependency graph

De Morgan: the non-models of a CNF formula #

source

(DnfModel B fun (b : B) => ν (e.symm b)) ↔ (∀ (x : A), ν x → SatOccurs A x) ∧ ¬SatModel A ν

De Morgan's law, for models: the models of the DNF formula B, the sign swap of the CNF formula A, are the sets of variables of A that are not models of A.

Dependency graph

source

SharpSAT.Count A + SharpDNF.Count B = 2 ^ Nat.card { x : A // SatOccurs A x }

Models and non-models share out the assignments: a CNF formula with n variables and its sign swap, read as a DNF formula, have 2 ^ n models between them.

Dependency graph

The reduction #

source

noncomputable def DescriptiveComplexity.satOccursAt {α : Type} (x : α) :

FirstOrder.Language.sat.Formula α

“x is a variable of the formula”: it occurs in some clause.

Equations

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

Instances For

Dependency graph

source

noncomputable def DescriptiveComplexity.satOccursFormula :

(FirstOrder.Language.sat.sum FirstOrder.Language.order).Formula (Fin 1)

“x is a variable of the formula”, over the ordered expansion.

Equations

DescriptiveComplexity.satOccursFormula = FirstOrder.Language.LHom.sumInl.onFormula (DescriptiveComplexity.satOccursAt 0)

Instances For

Dependency graph

source

theorem DescriptiveComplexity.realize_satOccursFormula (A : Type) [FirstOrder.Language.sat.Structure A] [LinearOrder A] (a : A) :

(satOccursFormula.Realize fun (x : Fin 1) => a) ↔ SatOccurs A a

Dependency graph

source

noncomputable def DescriptiveComplexity.sharpSat_oneCall_sharpDnf :

OneCallReduction SharpSAT SharpDNF

#SAT reduces to #DNF with one call: #SAT(φ) = 2 ^ n - #DNF(¬φ), for n the number of variables of φ.

Equations

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

Instances For

Dependency graph

source

theorem DescriptiveComplexity.sharpDnf_sharpP_oneCallHard :

SharpP.OneCallHard SharpDNF

#DNF is one-call #P-hard.

Dependency graph

source

theorem DescriptiveComplexity.sharpDnf_sharpP_oneCallComplete :

SharpP.OneCallComplete SharpDNF

#DNF is one-call #P-complete (Durand, Hermann, Kolaitis 2005): in #P, and every problem of #P reduces to it with one call. Registered in the Lax archive as Lax859101.DnfComplete.sharpDnf_sharpP_oneCallComplete.

Dependency graph