Restricting a counting problem to a definable class of instances

#2SAT, #HORN-SAT or #Monotone-2SAT count the models of a CNF formula of a certain shape, and are 0 on every other formula. That is #SAT restricted to a first-order definable class of instances (DescriptiveComplexity.CountingProblem.restrict), and two facts carry over from the unrestricted problem: membership in #P, by one more conjunct in the kernel (DescriptiveComplexity.SharpPDefinable.restrict), and one-call hardness, by any one-call reduction whose outputs all lie in the class (DescriptiveComplexity.OneCallReduction.restrict).

noncomputable def DescriptiveComplexity.CountingProblem.restrict {L : FirstOrder.Language} [L.IsRelational] (C : CountingProblem L) (P : L.Sentence) : CountingProblem L

A counting problem restricted to the instances satisfying a sentence: the count on those, 0 on the others.

Equations

• C.restrict P = { Count := fun (A : Type) (inst : L.Structure A) => if A ⊨ P then C.Count A else 0, iso_invariant := ⋯ }

theorem DescriptiveComplexity.CountingProblem.restrict_of_realize {L : FirstOrder.Language} [L.IsRelational] (C : CountingProblem L) (P : L.Sentence) (A : Type) [L.Structure A] (h : A ⊨ P) : (C.restrict P).Count A = C.Count A

theorem DescriptiveComplexity.CountingProblem.restrict_of_not_realize {L : FirstOrder.Language} [L.IsRelational] (C : CountingProblem L) (P : L.Sentence) (A : Type) [L.Structure A] (h : ¬A ⊨ P) : (C.restrict P).Count A = 0

def DescriptiveComplexity.kernelLift {L : FirstOrder.Language} (B : SOBlock) (P : L.Sentence) : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence

The sentence P, read over the vocabulary of a counting kernel.

Equations

• DescriptiveComplexity.kernelLift B P = FirstOrder.Language.LHom.sumInl.onSentence (FirstOrder.Language.LHom.sumInl.onSentence P)

theorem DescriptiveComplexity.realize_kernelLift {L : FirstOrder.Language} (B : SOBlock) (P : L.Sentence) (A : Type) [L.Structure A] [LinearOrder A] (ρ : B.Assignment A) : A ⊨ kernelLift B P ↔ A ⊨ P

theorem DescriptiveComplexity.SharpPDefinable.restrict {L : FirstOrder.Language} [L.IsRelational] {C : CountingProblem L} (hC : SharpPDefinable C) (P : L.Sentence) : SharpPDefinable (C.restrict P)

Restriction keeps #P-definability: the restricting sentence is one more conjunct of the kernel.

noncomputable def DescriptiveComplexity.OneCallReduction.restrict {L L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {C : CountingProblem L} {D : CountingProblem L'} (f : OneCallReduction C D) (P : L'.Sentence) (h : ∀ (A : Type) [inst : L.Structure A] [inst_1 : LinearOrder A] [Finite A] [Nonempty A], f.toRelInterpretation.MapRel A ⊨ P) : OneCallReduction C (D.restrict P)

A one-call reduction whose outputs all satisfy P is a one-call reduction into the restriction to P.

Equations

• f.restrict P h = { Tag := f.Tag, tagFinite := ⋯, dim := f.dim, toRelInterpretation := f.toRelInterpretation, dom_nonempty := ⋯, post := f.post, correct := ⋯ }