#SAT: counting the models of a CNF formula

The counting version of DescriptiveComplexity.SAT, on the same vocabulary: the number of models of a CNF formula (Valiant 1979).

A model is a set of true variables satisfying every clause, and it is a set of variables of the formula: an element that occurs in no clause is not a variable (DescriptiveComplexity.SatOccurs), and a model does not contain it (DescriptiveComplexity.SatModel). Without that convention every clause element and every unused element of an instance would double the count, where the decision problem can afford to leave them unconstrained.

DescriptiveComplexity.SharpSAT is the bundled counting problem; its support is SAT (DescriptiveComplexity.sharpSat_support_iff), and it belongs to #P (DescriptiveComplexity.sharpSat_mem_sharpP), the models being the witnesses of the Σ₁ definition of SAT with one conjunct added to the kernel. Its hardness is in DescriptiveComplexity.Problems.Sat.CountingHardness.

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

The set ν of true variables is a model of the CNF formula: every clause contains a true literal, and ν consists of variables of the formula.

Equations

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

theorem DescriptiveComplexity.satModel_restrict {A : Type} [FirstOrder.Language.sat.Structure A] {ν : A → Prop} (h : ∀ (c : A), FirstOrder.Language.Structure.RelMap FirstOrder.Language.satIsClause ![c] → ∃ (x : A), FirstOrder.Language.Structure.RelMap FirstOrder.Language.satPosIn ![c, x] ∧ ν x ∨ FirstOrder.Language.Structure.RelMap FirstOrder.Language.satNegIn ![c, x] ∧ ¬ν x) : SatModel A fun (x : A) => ν x ∧ SatOccurs A x

A satisfying assignment restricts to a model: only the values at the variables of the formula matter.

The kernel

noncomputable def DescriptiveComplexity.satVarKernel : satSOLang.Sentence

Kernel conjunct: the truth assignment only holds of variables of the formula, i.e., of elements occurring in a clause.

Equations

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

noncomputable def DescriptiveComplexity.sharpSatKernel : satSOLang.Sentence

The first-order kernel of #SAT: the kernel of SAT, and the truth assignment only holds of variables of the formula.

Equations

• DescriptiveComplexity.sharpSatKernel = DescriptiveComplexity.satKernel ⊓ DescriptiveComplexity.satVarKernel

def DescriptiveComplexity.satAssignEquiv (A : Type) : (A → Prop) ≃ satAssignBlock.Assignment A

Unary relations, as assignments of the truth-assignment block.

Equations

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

The counting problem

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

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

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

#SAT: the number of models of a CNF formula.

Equations

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

theorem DescriptiveComplexity.sharpSat_apply (A : Type) [FirstOrder.Language.sat.Structure A] : SharpSAT.Count A = Nat.card { ν : A → Prop // SatModel A ν }

theorem DescriptiveComplexity.sharpSat_support_iff (A : Type) [FirstOrder.Language.sat.Structure A] [Finite A] : SharpSAT.support.Holds A ↔ SAT.Holds A

The support of #SAT is SAT: on a finite structure, the number of models is positive exactly when the formula is satisfiable.

theorem DescriptiveComplexity.sharpSat_mem_sharpP : SharpP.Mem SharpSAT

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