Documentation

DescriptiveComplexity.Problems.DominatingSet.CountingHardness

#Dominating Set is parsimoniously `#P`-complete #

DescriptiveComplexity.sharpDominatingSet_sharpP_parsimoniousComplete, by a reduction from #SAT (DescriptiveComplexity.sharpSat_parsimonious_sharpDominatingSet), order-free.

The reduction of DescriptiveComplexity.Problems.DominatingSet.Reduction, from Set Cover, is not parsimonious, and cannot be made so by adjusting it: a dominating set may hold element vertices, and a cover smaller than the threshold can be padded with one. What a count of dominating sets of a given size needs is a graph in which that size leaves no slack. Here:

each variable x of the formula has two literal vertices (lit true, x) and (lit false, x), adjacent, and two private vertices (priv b, x), each adjacent to the two literal vertices of x and to nothing else;
each clause c has a vertex (cl, c), adjacent to the literal vertices of its literals;
the threshold is the number of variables.

A private vertex is dominated from within the four vertices of its variable, so a dominating set meets each such group, and at the threshold size it meets each exactly once and holds nothing else. The one vertex of a group has to dominate both private vertices, which are not adjacent: it is a literal vertex (DescriptiveComplexity.SatToDom.dom_structure). So the dominating sets of the threshold size are the assignments of the variables of the formula, and dominating the clause vertices is satisfying the clauses (DescriptiveComplexity.SatToDom.solEquiv).

Junk – a tagged element that is not a variable, or not a clause – has to be dominated too, and is made adjacent to every literal vertex. That needs a literal vertex in the set, which a formula with a clause provides; a formula with no clause at all has one model, and is sent to the edgeless graph with everything marked, which has one dominating set of the threshold size (DescriptiveComplexity.SatToDom.NoCl).

inductive DescriptiveComplexity.SatToDom.SDTag :

Tags of the reduction.

lit (s : Bool) : SDTag
The vertex of the literal of sign s of a variable.
priv (b : Bool) : SDTag
One of the two private vertices of a variable.
cl : SDTag
The vertex of a clause.

Instances For

Dependency graph

def DescriptiveComplexity.SatToDom.instDecidableEqSDTag.decEq (x✝ x✝¹ : SDTag) :

Decidable (x✝ = x✝¹)

Equations

Instances For

Dependency graph

@[instance_reducible]

instance DescriptiveComplexity.SatToDom.instDecidableEqSDTag :

DecidableEq SDTag

Equations

DescriptiveComplexity.SatToDom.instDecidableEqSDTag = DescriptiveComplexity.SatToDom.instDecidableEqSDTag.decEq

Dependency graph

@[instance_reducible]

instance DescriptiveComplexity.SatToDom.instFintypeSDTag :

Equations

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

Dependency graph

instance DescriptiveComplexity.SatToDom.instNonemptySDTag :

Dependency graph

The semantic side #

def DescriptiveComplexity.SatToDom.NoCl (A : Type) [FirstOrder.Language.sat.Structure A] :

The formula has no clause at all.

Equations

DescriptiveComplexity.SatToDom.NoCl A = ¬∃ (c : A), DescriptiveComplexity.SatOcc.IsCl c

Instances For

Dependency graph

The formulas and the interpretation #

noncomputable def DescriptiveComplexity.SatToDom.noClF {α : Type} :

FirstOrder.Language.sat.Formula α

DescriptiveComplexity.SatToDom.NoCl, as a formula.

Equations

DescriptiveComplexity.SatToDom.noClF = FirstOrder.Language.BoundedFormula.not (FirstOrder.Language.Formula.iExs Unit (DescriptiveComplexity.ThreeSatToSat.clF (Sum.inr ())))

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.SatToDom.targetF {α : Type} (s : Bool) (x : α) :

SDTag → α → FirstOrder.Language.sat.Formula α

DescriptiveComplexity.SatToDom.Target, as a formula.

Equations

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

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.SatToDom.litDomF {α : Type} :

SDTag → α → SDTag → α → FirstOrder.Language.sat.Formula α

DescriptiveComplexity.SatToDom.LitDom, as a formula.

Equations

One or more equations did not get rendered due to their size.
DescriptiveComplexity.SatToDom.litDomF x✝³ x✝² x✝¹ x✝ = ⊥

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.SatToDom.adjF (t₁ t₂ : SDTag) :

FirstOrder.Language.sat.Formula (Fin 2 × Fin 1)

The adjacency formulas of the interpretation, by tag.

Equations

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

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.SatToDom.markedF (t : SDTag) :

FirstOrder.Language.sat.Formula (Fin 1 × Fin 1)

The mark formulas of the interpretation, by tag.

Equations

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

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.SatToDom.sdInterp :

FOInterpretation FirstOrder.Language.sat FirstOrder.Language.markedGraph SDTag 1

The interpretation producing, from a CNF structure, the graph whose dominating sets of the threshold size are its models.

Equations

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

Instances For

Dependency graph

The points #

def DescriptiveComplexity.SatToDom.sdPt {A : Type} (t : SDTag) (x : A) :

The vertex of tag t over the element x.

Equations

DescriptiveComplexity.SatToDom.sdPt t x = (t, fun (x_1 : Fin 1) => x)

Instances For

Dependency graph

Characterization of the two relations #

The two sides of the bijection #

def DescriptiveComplexity.SatToDom.domOf {A : Type} [FirstOrder.Language.sat.Structure A] (ν : A → Prop) (p : sdInterp.Map A) :

The dominating set of an assignment: the vertices of its true literals – or everything, when there is no clause.

Equations

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

Instances For

Dependency graph

def DescriptiveComplexity.SatToDom.modelOf {A : Type} [FirstOrder.Language.sat.Structure A] (D : sdInterp.Map A → Prop) (x : A) :

The assignment of a dominating set: the variables whose positive literal vertex it holds.

Equations

DescriptiveComplexity.SatToDom.modelOf D x = (D (DescriptiveComplexity.SatToDom.sdPt (DescriptiveComplexity.SatToDom.SDTag.lit true) x) ∧ DescriptiveComplexity.SatOccurs A x)

Instances For

Dependency graph

Correctness #

theorem DescriptiveComplexity.SatToDom.domSetOfSize_domOf {A : Type} [FirstOrder.Language.sat.Structure A] [Finite A] {ν : A → Prop} (hν : SatModel A ν) :

DomSetOfSize (sdInterp.Map A) (domOf ν)

The dominating set of a model is one, of the threshold size.

Dependency graph

theorem DescriptiveComplexity.SatToDom.dom_structure {A : Type} [FirstOrder.Language.sat.Structure A] [Finite A] (hne : ¬NoCl A) {D : sdInterp.Map A → Prop} (hD : DomSetOfSize (sdInterp.Map A) D) :

(∀ (t : SDTag) (x : A), D (sdPt t x) → ∃ (s : Bool), t = SDTag.lit s ∧ SatOccurs A x) ∧ (∀ (x : A), SatOccurs A x → ∃ (s : Bool), D (sdPt (SDTag.lit s) x)) ∧ ∀ (t t' : SDTag) (x : A), D (sdPt t x) → D (sdPt t' x) → t = t'

A dominating set of the threshold size is an assignment: it consists of literal vertices of variables, one per variable.

Dependency graph

theorem DescriptiveComplexity.SatToDom.satModel_modelOf {A : Type} [FirstOrder.Language.sat.Structure A] [Finite A] {D : sdInterp.Map A → Prop} (hD : DomSetOfSize (sdInterp.Map A) D) :

SatModel A (modelOf D)

The assignment of a dominating set of the threshold size is a model.

Dependency graph

theorem DescriptiveComplexity.SatToDom.domOf_modelOf {A : Type} [FirstOrder.Language.sat.Structure A] [Finite A] {D : sdInterp.Map A → Prop} (hD : DomSetOfSize (sdInterp.Map A) D) :

domOf (modelOf D) = D

A dominating set of the threshold size is the dominating set of its assignment.

Dependency graph

theorem DescriptiveComplexity.SatToDom.modelOf_domOf {A : Type} [FirstOrder.Language.sat.Structure A] {ν : A → Prop} (hν : SatModel A ν) :

modelOf (domOf ν) = ν

A model is the assignment of its dominating set.

Dependency graph

def DescriptiveComplexity.SatToDom.solEquiv (A : Type) [FirstOrder.Language.sat.Structure A] [Finite A] :

{ ν : A → Prop // SatModel A ν } ≃ { D : sdInterp.Map A → Prop // DomSetOfSize (sdInterp.Map A) D }

The dominating sets of the threshold size of the interpreted graph are the models of the CNF formula, bijectively.

Equations

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

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.sharpSat_parsimonious_sharpDominatingSet :

ParsimoniousReduction SharpSAT SharpDominatingSet

#SAT reduces parsimoniously to #Dominating Set, without an order.

Equations

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

Instances For

Dependency graph

theorem DescriptiveComplexity.sharpDominatingSet_sharpP_parsimoniousHard :

SharpP.ParsimoniousHard SharpDominatingSet

#Dominating Set is parsimoniously #P-hard.

Dependency graph

theorem DescriptiveComplexity.sharpDominatingSet_sharpP_parsimoniousComplete :

SharpP.ParsimoniousComplete SharpDominatingSet

#Dominating Set is parsimoniously #P-complete, counting the dominating sets of exactly the threshold size. Registered in the Lax archive as Lax280166.DominatingSetComplete.sharpDominatingSet_sharpP_parsimoniousComplete.

Dependency graph

theorem DescriptiveComplexity.sharpDominatingSet_sharpP_complete :

SharpP.Complete SharpDominatingSet

SharpDominatingSet is #P-complete: parsimoniously, hence under subtractive reductions.

Dependency graph