SelMajSAT and SelEqSAT: complete problems for PP and C₌P

A CNF formula with a selected variable (FirstOrder.Language.satSel), and the two counts of its models by the value of that variable (DescriptiveComplexity.SharpSelSAT true, DescriptiveComplexity.SharpSelSAT false), both in #P. The two decision problems comparing them:

• SelMajSAT (DescriptiveComplexity.SelMajSAT): the selected variable is true in more models than it is false – PP-complete (DescriptiveComplexity.selMajSat_PP_complete), the form the classical MajSAT of Gill 1977 takes when the instance may not count its own variables;
• SelEqSAT (DescriptiveComplexity.SelEqSAT): it is true in exactly as many models as it is false – C₌P-complete (DescriptiveComplexity.selEqSat_CeqP_complete).

Hardness is one construction for both: a problem of either class compares the witness counts of two kernels; the pair kernel of DescriptiveComplexity.Counting.KernelPair puts them in one kernel with a selector, the parsimonious Tseitin interpretation turns it into a CNF formula whose models are its witnesses, and the selected variable is the one of the selector (DescriptiveComplexity.PairSel.pairTseitinInterp). The models in which the selected variable is true are then the witnesses of the first kernel, and the others those of the second.

@[reducible, inline]

abbrev FirstOrder.Language.smSel : Language.selMark.Relations 1

sel x: the variable x is selected.

Equations

• FirstOrder.Language.smSel = FirstOrder.Language.selMarkRel.sel

inductive FirstOrder.Language.selMarkRel : ℕ → Type

The relation symbols of the language.

• sel : selMarkRel 1

  sel x: the variable x is selected.

def FirstOrder.Language.instDecidableEqSelMarkRel.decEq {a✝ : ℕ} (x✝ x✝¹ : selMarkRel a✝) : Decidable (x✝ = x✝¹)

Equations

• FirstOrder.Language.instDecidableEqSelMarkRel.decEq FirstOrder.Language.selMarkRel.sel FirstOrder.Language.selMarkRel.sel = isTrue FirstOrder.Language.instDecidableEqSelMarkRel.decEq._proof_1

def FirstOrder.Language.selMark : Language

The symbol selecting a variable.

Equations

• FirstOrder.Language.selMark = { Functions := fun (x : ℕ) => Empty, Relations := FirstOrder.Language.selMarkRel }

@[instance_reducible]

instance FirstOrder.Language.instDecidableEqSelMarkRel {a✝ : ℕ} : DecidableEq (selMarkRel a✝)

Equations

• FirstOrder.Language.instDecidableEqSelMarkRel = FirstOrder.Language.instDecidableEqSelMarkRel.decEq

instance FirstOrder.Language.instIsRelationalSelMark : Language.selMark.IsRelational

@[reducible, inline]

abbrev FirstOrder.Language.satSel : Language

The relational language of CNF formulas with a selected variable.

Equations

• FirstOrder.Language.satSel = FirstOrder.Language.sat.sum FirstOrder.Language.selMark

@[reducible, inline]

abbrev DescriptiveComplexity.ssSel : FirstOrder.Language.satSel.Relations 1

“Is selected”, in the vocabulary of CNF formulas with a selected variable.

Equations

• DescriptiveComplexity.ssSel = Sum.inr FirstOrder.Language.smSel

@[instance_reducible]

instance DescriptiveComplexity.satSelStructure (A : Type) [FirstOrder.Language.satSel.Structure A] : FirstOrder.Language.sat.Structure A

A CNF formula with a selected variable is a CNF formula.

Equations

• DescriptiveComplexity.satSelStructure A = FirstOrder.Language.LHom.sumInl.reduct A

def DescriptiveComplexity.satSelEquiv {A B : Type} [FirstOrder.Language.satSel.Structure A] [FirstOrder.Language.satSel.Structure B] (e : FirstOrder.Language.satSel.Equiv A B) : FirstOrder.Language.sat.Equiv A B

The forgetful isomorphism of the underlying CNF formulas.

Equations

• DescriptiveComplexity.satSelEquiv e = { toEquiv := e.toEquiv, map_fun' := ⋯, map_rel' := ⋯ }

The two counts

def DescriptiveComplexity.SelModel (A : Type) [FirstOrder.Language.satSel.Structure A] (b : Bool) (ν : A → Prop) : Prop

A model of the formula in which every selected variable has the value b.

Equations

• DescriptiveComplexity.SelModel A b ν = (DescriptiveComplexity.SatModel A ν ∧ ∀ (x : A), FirstOrder.Language.Structure.RelMap DescriptiveComplexity.ssSel ![x] → (ν x ↔ b = true))

@[reducible, inline]

abbrev DescriptiveComplexity.selSOLang : FirstOrder.Language

The vocabulary of the kernel: CNF formulas with a selected variable, and the truth-assignment variable.

Equations

• DescriptiveComplexity.selSOLang = FirstOrder.Language.satSel.sum DescriptiveComplexity.satAssignBlock.lang

@[reducible, inline]

abbrev DescriptiveComplexity.kSelSym : selSOLang.Relations 1

“Is selected”, in the kernel's vocabulary.

Equations

• DescriptiveComplexity.kSelSym = Sum.inl DescriptiveComplexity.ssSel

@[reducible, inline]

abbrev DescriptiveComplexity.kNuSelSym : selSOLang.Relations 1

The truth-assignment symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.kNuSelSym = Sum.inr DescriptiveComplexity.satNuSym

def DescriptiveComplexity.selHom : satSOLang →ᴸ selSOLang

The kernel of #SAT, read in the kernel's vocabulary.

Equations

• DescriptiveComplexity.selHom = FirstOrder.Language.LHom.sumInl.sumMap (FirstOrder.Language.LHom.id DescriptiveComplexity.satAssignBlock.lang)

noncomputable def DescriptiveComplexity.selKernel (b : Bool) : selSOLang.Sentence

The kernel: a model of the formula, in which every selected variable has the value b.

Equations

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

instance DescriptiveComplexity.selHom_isExpansionOn {A : Type} [FirstOrder.Language.satSel.Structure A] (ρ : satAssignBlock.Assignment A) : selHom.IsExpansionOn A

theorem DescriptiveComplexity.card_selModel_eq_witnessCount {A : Type} [FirstOrder.Language.satSel.Structure A] (b : Bool) : Nat.card { ν : A → Prop // SelModel A b ν } = witnessCount satAssignBlock (selKernel b) A

noncomputable def DescriptiveComplexity.SharpSelSAT (b : Bool) : CountingProblem FirstOrder.Language.satSel

The number of models of a CNF formula in which the selected variable has the value b.

Equations

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

The two problems

noncomputable def DescriptiveComplexity.SelMajSAT : DecisionProblem FirstOrder.Language.satSel

SelMajSAT: the selected variable is true in more models than it is false.

Equations

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

noncomputable def DescriptiveComplexity.SelEqSAT : DecisionProblem FirstOrder.Language.satSel

SelEqSAT: the selected variable is true in exactly as many models as it is false.

Equations

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

theorem DescriptiveComplexity.selMajSat_mem_PP : PP.Mem SelMajSAT

theorem DescriptiveComplexity.selEqSat_mem_CeqP : CeqP.Mem SelEqSAT

Hardness: the Tseitin formula of a pair kernel, with the selector

selected

@[reducible, inline]

abbrev DescriptiveComplexity.PairSel.pairZ (B B' : SOBlock) : (pairBlock B B').ι

The selector of the pair block.

Equations

• DescriptiveComplexity.PairSel.pairZ B B' = Sum.inr (Sum.inr ())

@[reducible, inline]

abbrev DescriptiveComplexity.PairSel.PB (B B' : SOBlock) : SOBlock

The block and the kernel of the pair, abbreviated.

Equations

• DescriptiveComplexity.PairSel.PB B B' = DescriptiveComplexity.pairBlock B B'

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.PairSel.PK {L : FirstOrder.Language} (B B' : SOBlock) (φ : (L.sum B.lang).Sentence) (φ' : (L.sum B'.lang).Sentence) : (L.sum (PB B B').lang).Sentence

The pair kernel, abbreviated.

Equations

• DescriptiveComplexity.PairSel.PK B B' φ φ' = DescriptiveComplexity.pairKernel B B' φ φ'

noncomputable def DescriptiveComplexity.PairSel.pairTseitinInterp {L : FirstOrder.Language} (B B' : SOBlock) (φ : (L.sum B.lang).Sentence) (φ' : (L.sum B'.lang).Sentence) : FOInterpretation (L.sum FirstOrder.Language.order) FirstOrder.Language.satSel (SharpTseitinTag (PB B B') (PK B B' φ φ')) (tseitinDim (PB B B') (PK B B' φ φ'))

The Tseitin formula of the pair kernel, with the selector's variable selected.

Equations

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

def DescriptiveComplexity.PairSel.satEquiv {L : FirstOrder.Language} {B B' : SOBlock} {φ : (L.sum B.lang).Sentence} {φ' : (L.sum B'.lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] : FirstOrder.Language.sat.Equiv ((pairTseitinInterp B B' φ φ').Map A) ((sharpTseitinInterp (PB B B') (PK B B' φ φ')).Map A)

The underlying CNF formula is the parsimonious Tseitin formula.

Equations

• DescriptiveComplexity.PairSel.satEquiv = { toEquiv := Equiv.refl ((DescriptiveComplexity.PairSel.pairTseitinInterp B B' φ φ').Map A), map_fun' := ⋯, map_rel' := ⋯ }

theorem DescriptiveComplexity.PairSel.sharpSelSat_eq {L : FirstOrder.Language} {B B' : SOBlock} {φ : (L.sum B.lang).Sentence} {φ' : (L.sum B'.lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (b : Bool) : (SharpSelSAT b).Count ((pairTseitinInterp B B' φ φ').Map A) = Nat.card { w : Witness (PB B B') (PK B B' φ φ') A // pairSel ↑w ↔ b = true }

The models with the selected variable at b are the witnesses of the pair kernel whose selector is b. Registered in the Lax archive as Lax175070.CountingValues.sharpSelSat_eq.

theorem DescriptiveComplexity.PairSel.sharpSelSat_true {L : FirstOrder.Language} {B B' : SOBlock} {φ : (L.sum B.lang).Sentence} {φ' : (L.sum B'.lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : (SharpSelSAT true).Count ((pairTseitinInterp B B' φ φ').Map A) = witnessCount B φ A

theorem DescriptiveComplexity.PairSel.sharpSelSat_false {L : FirstOrder.Language} {B B' : SOBlock} {φ : (L.sum B.lang).Sentence} {φ' : (L.sum B'.lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : (SharpSelSAT false).Count ((pairTseitinInterp B B' φ φ').Map A) = witnessCount B' φ' A

noncomputable def DescriptiveComplexity.CountDefinable.orderedReduction_sel {L : FirstOrder.Language} [L.IsRelational] (R : ℕ → ℕ → Prop) {P : DecisionProblem L} (B : SOBlock) (φ : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence) (B' : SOBlock) (φ' : ((L.sum FirstOrder.Language.order).sum B'.lang).Sentence) (h : ∀ (A : Type) [inst : L.Structure A] [inst_1 : LinearOrder A] [Finite A] [Nonempty A], P.Holds A ↔ R (witnessCount B φ A) (witnessCount B' φ' A)) : OrderedFOReduction P { Holds := fun (A : Type) (inst : FirstOrder.Language.satSel.Structure A) => R ((SharpSelSAT true).Count A) ((SharpSelSAT false).Count A), iso_invariant := ⋯ }

Every problem defined by a relation between two witness counts reduces to the comparison of the two counts of a CNF formula by its selected variable.

Equations

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

theorem DescriptiveComplexity.selMajSat_PP_hard : PP.Hard SelMajSAT

theorem DescriptiveComplexity.selEqSat_CeqP_hard : CeqP.Hard SelEqSAT

theorem DescriptiveComplexity.selMajSat_PP_complete : PP.Complete SelMajSAT

SelMajSAT is PP-complete. Registered in the Lax archive as Lax175070.SelectedSatComplete.selMajSat_PP_complete.

theorem DescriptiveComplexity.selEqSat_CeqP_complete : CeqP.Complete SelEqSAT

SelEqSAT is C₌P-complete. Registered in the Lax archive as Lax175070.SelectedSatComplete.selEqSat_CeqP_complete.