#NAE-SAT and #Set Splitting

The counting versions of DescriptiveComplexity.NAESAT and DescriptiveComplexity.SetSplitting. Their solutions come in complementary pairs, which is why neither is reached parsimoniously; both are one-call #P-complete.

• #NAE-SAT (DescriptiveComplexity.SharpNAESAT) counts the not-all-equal models among the sets of variables of the formula, the convention of #SAT, so that flipping a model inside the variables is again a model. The reduction from #SAT is that of the decision problem unchanged, one fresh variable added positively to every clause: a model of the result is a model of the formula with the fresh variable false, or its flip (DescriptiveComplexity.NaeCount.card_naeModel_map), so the count is halved, rounding up for the formula with no clause, whose only model is empty.
• #Set Splitting (DescriptiveComplexity.SharpSetSplitting) counts the color classes of ground elements splitting every set. The reduction from #NAE-SAT is again that of the decision problem: a splitting of the literal set system is an assignment of every element, the variables of the formula and the others alike, and each element that is no variable doubles the count (DescriptiveComplexity.NaeCount.card_split_map).

#NAE-SAT

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

A not-all-equal model: a not-all-equal proper set of variables of the formula.

Equations

• DescriptiveComplexity.NAEModel A ν = (DescriptiveComplexity.NAEProper ν ∧ ∀ (x : A), ν x → DescriptiveComplexity.SatOccurs A x)

noncomputable def DescriptiveComplexity.sharpNaeKernel : satSOLang.Sentence

The first-order kernel of #NAE-SAT.

Equations

• DescriptiveComplexity.sharpNaeKernel = DescriptiveComplexity.naeKernel ⊓ DescriptiveComplexity.satVarKernel

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

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

#NAE-SAT: the number of not-all-equal models of a CNF formula.

Equations

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

The fresh variable

theorem DescriptiveComplexity.NaeCount.oPt_injective {A : Type} : Function.Injective oPt

theorem DescriptiveComplexity.NaeCount.oPt_ne_xPt {A : Type} (x y : A) : oPt x ≠ xPt y

noncomputable def DescriptiveComplexity.NaeCount.least (A : Type) [LinearOrder A] [Finite A] [Nonempty A] : A

The least element.

Equations

• DescriptiveComplexity.NaeCount.least A = Classical.choose ⋯

theorem DescriptiveComplexity.NaeCount.least_le {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (a : A) : least A ≤ a

theorem DescriptiveComplexity.NaeCount.card_naeModel_map {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : SharpNAESAT.Count (naeInterp.Map A) + 1 = 2 * SharpSAT.Count A + 1 ∨ SharpNAESAT.Count (naeInterp.Map A) = 1 ∧ SharpSAT.Count A = 1

The count of the formula with the fresh variable: twice the count of the formula when there is a clause.

noncomputable def DescriptiveComplexity.sharpSat_oneCall_sharpNaeSat : OneCallReduction SharpSAT SharpNAESAT

#SAT reduces to #NAE-SAT with one call: add one fresh variable to every clause, and halve the count, rounding up.

Equations

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

theorem DescriptiveComplexity.sharpNaeSat_sharpP_oneCallComplete : SharpP.OneCallComplete SharpNAESAT

#NAE-SAT is one-call #P-complete. Registered in the Lax archive as Lax859101.NaeSatComplete.sharpNaeSat_sharpP_oneCallComplete.

#Set Splitting

def DescriptiveComplexity.SplitColoring (A : Type) [FirstOrder.Language.setSystem.Structure A] (S : A → Prop) : Prop

A splitting color class: a set of ground elements meeting every set of the family and its complement.

Equations

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

def DescriptiveComplexity.splitColoringEquiv (A : Type) [FirstOrder.Language.setSystem.Structure A] : { ρ : familyGuessBlock.Assignment A // A ⊨ sharpSetSplittingKernel } ≃ { S : A → Prop // SplitColoring A S }

The splitting color classes are the witnesses of the counting kernel, bijectively.

Equations

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

noncomputable def DescriptiveComplexity.SharpSetSplitting : CountingProblem FirstOrder.Language.setSystem

#Set Splitting: the number of color classes of ground elements splitting every set of the family.

Equations

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

noncomputable def DescriptiveComplexity.NaeCount.splitEquiv {A : Type} [FirstOrder.Language.sat.Structure A] : { S : SetSplitRed.splInterp.Map A → Prop // SplitColoring (SetSplitRed.splInterp.Map A) S } ≃ { ν : A → Prop // NAEProper ν }

The splittings of the literal set system are the not-all-equal assignments of every element.

Equations

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

theorem DescriptiveComplexity.NaeCount.card_split_map {A : Type} [FirstOrder.Language.sat.Structure A] [Finite A] : SharpSetSplitting.Count (SetSplitRed.splInterp.Map A) = SharpNAESAT.Count A * 2 ^ Nat.card { x : A // ¬SatOccurs A x }

The count of the literal set system: the count of the formula, doubled for each element that is no variable of it.

noncomputable def DescriptiveComplexity.nonVarCount : PolyTerm FirstOrder.Language.sat

The number of elements that are no variable of the formula, as a polynomial term.

Equations

• DescriptiveComplexity.nonVarCount = DescriptiveComplexity.PolyTerm.count (FirstOrder.Language.BoundedFormula.not DescriptiveComplexity.satOccursFormula)

theorem DescriptiveComplexity.eval_nonVarCount (A : Type) [FirstOrder.Language.sat.Structure A] [LinearOrder A] : PolyTerm.eval A nonVarCount = Nat.card { x : A // ¬SatOccurs A x }

noncomputable def DescriptiveComplexity.sharpNaeSat_oneCall_sharpSetSplitting : OneCallReduction SharpNAESAT SharpSetSplitting

#NAE-SAT reduces to #Set Splitting with one call: the literal set system, its count divided by 2 to the number of elements that are no variable of the formula.

Equations

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

theorem DescriptiveComplexity.sharpSetSplitting_sharpP_oneCallComplete : SharpP.OneCallComplete SharpSetSplitting

#Set Splitting is one-call #P-complete. Registered in the Lax archive as Lax859101.NaeSatComplete.sharpSetSplitting_sharpP_oneCallComplete.