#1-in-SAT: counting exactly-one models

The counting version of DescriptiveComplexity.OneInSAT: the number of assignments giving every clause exactly one true literal. As for #SAT, an assignment is a set of variables of the formula – of elements occurring in a clause (DescriptiveComplexity.OneInModel).

DescriptiveComplexity.SharpOneInSAT is in #P (DescriptiveComplexity.sharpOneInSat_mem_sharpP); its parsimonious hardness is in DescriptiveComplexity.Problems.OneInSat.CountingFromSat.

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

The set ν of true variables is an exactly-one model of the CNF formula: every clause has exactly one true literal, and ν consists of variables of the formula.

Equations

• DescriptiveComplexity.OneInModel A ν = (DescriptiveComplexity.OneInProper ν ∧ ∀ (x : A), ν x → DescriptiveComplexity.SatOccurs A x)

noncomputable def DescriptiveComplexity.sharpOneInKernel : satSOLang.Sentence

The first-order kernel of #1-in-SAT.

Equations

• DescriptiveComplexity.sharpOneInKernel = DescriptiveComplexity.oneInKernel ⊓ DescriptiveComplexity.satVarKernel

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

The number of exactly-one models is the number of witnesses of the kernel.

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

#1-in-SAT: the number of assignments of the variables of a CNF formula giving every clause exactly one true literal.

Equations

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

theorem DescriptiveComplexity.oneInModel_restrict {A : Type} [FirstOrder.Language.sat.Structure A] {ν : A → Prop} (h : OneInProper ν) : OneInModel A fun (x : A) => ν x ∧ SatOccurs A x

An exactly-one proper assignment restricts to an exactly-one model: only its values at the variables of the formula matter.

theorem DescriptiveComplexity.sharpOneInSat_support_iff (A : Type) [FirstOrder.Language.sat.Structure A] [Finite A] : SharpOneInSAT.support.Holds A ↔ OneInSAT.Holds A

The support of #1-in-SAT is 1-in-SAT. Registered in the Lax archive as Lax280166.OneInSATComplete.sharpOneInSat_support_iff.

theorem DescriptiveComplexity.sharpOneInSat_mem_sharpP : SharpP.Mem SharpOneInSAT

#1-in-SAT is in #P.