#3SAT: counting the models of a 3-CNF formula

The counting version of DescriptiveComplexity.ThreeSAT: the number of models of a CNF formula whose clauses have at most three literals. As for the decision problem, the width bound is folded in: an instance violating it has no model to count. Models are those of DescriptiveComplexity.SharpSAT – sets of variables of the formula (DescriptiveComplexity.SatModel).

DescriptiveComplexity.SharpThreeSAT is in #P (DescriptiveComplexity.sharpThreeSat_mem_sharpP), the kernel of #SAT being conjoined with the first-order sentence stating the width bound. Its parsimonious hardness is in DescriptiveComplexity.Problems.ThreeSat.CountingFromSat.

noncomputable def DescriptiveComplexity.sharpThreeSatKernel : satSOLang.Sentence

The first-order kernel of #3SAT: no clause is wide, and the truth assignment is a model.

Equations

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

theorem DescriptiveComplexity.card_threeSatModel_eq_witnessCount (A : Type) [FirstOrder.Language.sat.Structure A] : Nat.card { ν : A → Prop // WidthAtMostThree A ∧ SatModel A ν } = witnessCount satAssignBlock sharpThreeSatKernel A

The number of models of a 3-CNF formula is the number of witnesses of the kernel of #3SAT.

noncomputable def DescriptiveComplexity.SharpThreeSAT : CountingProblem FirstOrder.Language.sat

#3SAT: the number of models of a CNF formula with at most three literals per clause; zero when some clause is wider.

Equations

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

theorem DescriptiveComplexity.sharpThreeSat_support_iff (A : Type) [FirstOrder.Language.sat.Structure A] [Finite A] : SharpThreeSAT.support.Holds A ↔ ThreeSAT.Holds A

The support of #3SAT is 3SAT. Registered in the Lax archive as Lax280166.ThreeSATComplete.sharpThreeSat_support_iff.

theorem DescriptiveComplexity.sharpThreeSat_mem_sharpP : SharpP.Mem SharpThreeSAT

#3SAT is in #P.