#Clique is parsimoniously #P-complete

DescriptiveComplexity.sharpClique_sharpP_parsimoniousComplete, by a reduction from #1-in-SAT (DescriptiveComplexity.sharpOneInSat_ordered_parsimonious_sharpClique).

The reduction of DescriptiveComplexity.Problems.CliqueFamily.FromSat is not parsimonious: a clique picks one true literal in each clause, and a satisfying assignment usually offers several. Under exactly-one satisfaction the choice is forced, provided a vertex says all that choosing it entails. So an occurrence vertex (c, x, s) here stands for “(x, s) is the true literal of c, and every other literal of c is false”, which fixes the value of every variable of c (DescriptiveComplexity.OneInToClique.ForceAt), and two occurrence vertices of distinct clauses are adjacent when the values they fix agree (DescriptiveComplexity.OneInToClique.Clash). A vertex whose own demands are contradictory – its clause holds another variable with both signs – is adjacent to nothing.

A singleton is a clique whatever the graph, so the threshold is kept away from 1: each clause c also has a clause vertex (cl, (c, c)), adjacent to every other clause vertex and to every consistent occurrence vertex, and the marked set has two elements per clause. A clique of that size holds every clause vertex and one occurrence vertex per clause (DescriptiveComplexity.OneInToClique.clique_slots), pairwise in agreement: an exactly-one model, and each model arises once (DescriptiveComplexity.OneInToClique.solEquiv). A clause with no literal has no occurrence vertex, so the count is 0, as it should be.

The formulas do not mention the order; as in the decision reduction, the packaging is ordered because both counts are of finite structures only.

The semantic side

def DescriptiveComplexity.OneInToClique.ForceAt {A : Type} [FirstOrder.Language.sat.Structure A] (c x : A) (s : Bool) (y : A) (t b : Bool) : Prop

Choosing (x, s) as the one true literal of the clause c gives the variable y the value b, as read on the occurrence (y, t) of c: the literal (y, t) is true exactly when it is the chosen one.

Equations

• DescriptiveComplexity.OneInToClique.ForceAt c x s y t b = (DescriptiveComplexity.SatOcc.OccIn c y t ∧ (b = t ↔ y = x ∧ t = s))

def DescriptiveComplexity.OneInToClique.Clash {A : Type} [FirstOrder.Language.sat.Structure A] (c x : A) (s : Bool) (c' x' : A) (s' : Bool) : Prop

The choices (c, x, s) and (c', x', s') disagree: some variable is made true by the first and false by the second.

Equations

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

The formulas and the interpretation

def DescriptiveComplexity.OneInToClique.forceAtF {α : Type} (s t b : Bool) (c x y : α) : SatOcc.satOrd.Formula α

DescriptiveComplexity.OneInToClique.ForceAt, as a formula: the signs are parameters.

Equations

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

noncomputable def DescriptiveComplexity.OneInToClique.clashF {α : Type} (s s' : Bool) (c x c' x' : α) : SatOcc.satOrd.Formula α

DescriptiveComplexity.OneInToClique.Clash, as a formula.

Equations

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

noncomputable def DescriptiveComplexity.OneInToClique.soundF {α : Type} (s : Bool) (c x : α) : SatOcc.satOrd.Formula α

DescriptiveComplexity.OneInToClique.Sound, as a formula.

Equations

• DescriptiveComplexity.OneInToClique.soundF s c x = DescriptiveComplexity.SatOcc.occF s c x ⊓ FirstOrder.Language.BoundedFormula.not (DescriptiveComplexity.OneInToClique.clashF s s c x c x)

noncomputable def DescriptiveComplexity.OneInToClique.validF {α : Type} : SatCliqueTag → α → α → SatOcc.satOrd.Formula α

DescriptiveComplexity.OneInToClique.Valid, as a formula.

Equations

• DescriptiveComplexity.OneInToClique.validF DescriptiveComplexity.SatCliqueTag.pos x✝¹ x✝ = DescriptiveComplexity.OneInToClique.soundF true x✝¹ x✝
• DescriptiveComplexity.OneInToClique.validF DescriptiveComplexity.SatCliqueTag.neg x✝¹ x✝ = DescriptiveComplexity.OneInToClique.soundF false x✝¹ x✝
• DescriptiveComplexity.OneInToClique.validF DescriptiveComplexity.SatCliqueTag.cl x✝¹ x✝ = DescriptiveComplexity.SatOcc.eqF x✝¹ x✝ ⊓ DescriptiveComplexity.SatOcc.clF x✝¹

noncomputable def DescriptiveComplexity.OneInToClique.sepSF (s₁ s₂ : Bool) : SatOcc.satOrd.Formula (Fin 2 × Fin 2)

DescriptiveComplexity.OneInToClique.SepS, as a formula. The free variable (i, j) is the j-th component of the i-th vertex.

Equations

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

noncomputable def DescriptiveComplexity.OneInToClique.sepF : SatCliqueTag → SatCliqueTag → SatOcc.satOrd.Formula (Fin 2 × Fin 2)

DescriptiveComplexity.OneInToClique.Sep, as a formula.

Equations

• DescriptiveComplexity.OneInToClique.sepF DescriptiveComplexity.SatCliqueTag.pos DescriptiveComplexity.SatCliqueTag.pos = DescriptiveComplexity.OneInToClique.sepSF true true
• DescriptiveComplexity.OneInToClique.sepF DescriptiveComplexity.SatCliqueTag.pos DescriptiveComplexity.SatCliqueTag.neg = DescriptiveComplexity.OneInToClique.sepSF true false
• DescriptiveComplexity.OneInToClique.sepF DescriptiveComplexity.SatCliqueTag.neg DescriptiveComplexity.SatCliqueTag.pos = DescriptiveComplexity.OneInToClique.sepSF false true
• DescriptiveComplexity.OneInToClique.sepF DescriptiveComplexity.SatCliqueTag.neg DescriptiveComplexity.SatCliqueTag.neg = DescriptiveComplexity.OneInToClique.sepSF false false
• DescriptiveComplexity.OneInToClique.sepF x✝¹ x✝ = ⊤

noncomputable def DescriptiveComplexity.OneInToClique.adjF (t₁ t₂ : SatCliqueTag) : SatOcc.satOrd.Formula (Fin 2 × Fin 2)

The adjacency formulas of the interpretation, by tag.

Equations

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

def DescriptiveComplexity.OneInToClique.markedF : SatCliqueTag → SatOcc.satOrd.Formula (Fin 1 × Fin 2)

The mark formulas of the interpretation, by tag.

Equations

• DescriptiveComplexity.OneInToClique.markedF DescriptiveComplexity.SatCliqueTag.neg = ⊥
• DescriptiveComplexity.OneInToClique.markedF x✝ = DescriptiveComplexity.SatOcc.eqF (0, 0) (0, 1) ⊓ DescriptiveComplexity.SatOcc.clF (0, 0)

noncomputable def DescriptiveComplexity.OneInToClique.oneInToClique : FOInterpretation SatOcc.satOrd FirstOrder.Language.markedGraph SatCliqueTag 2

The interpretation producing, from an ordered CNF structure, the clique instance whose threshold-size cliques are its exactly-one models.

Equations

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

Characterizations of the interpreted relations

Naming the vertices

def DescriptiveComplexity.OneInToClique.mkPt {A : Type} (t : SatCliqueTag) (c x : A) : oneInToClique.Map A

The vertex of tag t at the pair (c, x).

Equations

• DescriptiveComplexity.OneInToClique.mkPt t c x = (t, ![c, x])

The two sides of the bijection

def DescriptiveComplexity.OneInToClique.cliqueOf {A : Type} [FirstOrder.Language.sat.Structure A] (ν : A → Prop) (p : oneInToClique.Map A) : Prop

The clique of an assignment: every clause vertex, and the occurrence vertices of its true literals.

Equations

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

def DescriptiveComplexity.OneInToClique.modelOf {A : Type} [FirstOrder.Language.sat.Structure A] (S : oneInToClique.Map A → Prop) (y : A) : Prop

The assignment of a clique: the variables some occurrence vertex of the clique makes true.

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.OneInToClique.Slot (A : Type) [FirstOrder.Language.sat.Structure A] : Type

The slots of a clique of the threshold size: two per clause.

Equations

• DescriptiveComplexity.OneInToClique.Slot A = ({ c : A // DescriptiveComplexity.SatOcc.IsCl c } ⊕ { c : A // DescriptiveComplexity.SatOcc.IsCl c })

Correctness

theorem DescriptiveComplexity.OneInToClique.cliqueOfSize_cliqueOf {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] {ν : A → Prop} (hν : OneInProper ν) : CliqueOfSize (oneInToClique.Map A) (cliqueOf ν)

The clique of an exactly-one assignment has the threshold size.

theorem DescriptiveComplexity.OneInToClique.clique_slots {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] {S : oneInToClique.Map A → Prop} (hS : CliqueOfSize (oneInToClique.Map A) S) (c : A) (hc : SatOcc.IsCl c) : S (mkPt SatCliqueTag.cl c c) ∧ ∃ (x : A) (s : Bool), S (mkPt (SatCliqueTag.ofSign s) c x)

A clique of the threshold size fills every slot: it holds every clause vertex, and an occurrence vertex of every clause.

theorem DescriptiveComplexity.OneInToClique.oneInModel_modelOf {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] {S : oneInToClique.Map A → Prop} (hS : CliqueOfSize (oneInToClique.Map A) S) : OneInModel A (modelOf S)

The assignment of a clique of the threshold size is an exactly-one model.

theorem DescriptiveComplexity.OneInToClique.cliqueOf_modelOf {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] {S : oneInToClique.Map A → Prop} (hS : CliqueOfSize (oneInToClique.Map A) S) : cliqueOf (modelOf S) = S

A clique of the threshold size is the clique of its assignment.

theorem DescriptiveComplexity.OneInToClique.modelOf_cliqueOf {A : Type} [FirstOrder.Language.sat.Structure A] {ν : A → Prop} (hν : OneInModel A ν) : modelOf (cliqueOf ν) = ν

An exactly-one model is the assignment of its clique.

noncomputable def DescriptiveComplexity.OneInToClique.solEquiv (A : Type) [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] : { ν : A → Prop // OneInModel A ν } ≃ { S : oneInToClique.Map A → Prop // CliqueOfSize (oneInToClique.Map A) S }

The cliques of the threshold size of the interpreted graph are the exactly-one models of the CNF formula, bijectively.

Equations

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

theorem DescriptiveComplexity.OneInToClique.sharpClique_map (A : Type) [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] : SharpClique.Count (oneInToClique.Map A) = SharpOneInSAT.Count A

Correctness of the interpretation, for counting.

noncomputable def DescriptiveComplexity.sharpOneInSat_ordered_parsimonious_sharpClique : OrderedParsimoniousReduction SharpOneInSAT SharpClique

#1-in-SAT reduces parsimoniously to #Clique.

Equations

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

theorem DescriptiveComplexity.sharpClique_sharpP_parsimoniousHard : SharpP.ParsimoniousHard SharpClique

#Clique is parsimoniously #P-hard.

theorem DescriptiveComplexity.sharpClique_sharpP_parsimoniousComplete : SharpP.ParsimoniousComplete SharpClique

#Clique is parsimoniously #P-complete, counting the cliques of exactly the threshold size. Registered in the Lax archive as Lax280166.CliqueComplete.sharpClique_sharpP_parsimoniousComplete.

theorem DescriptiveComplexity.sharpClique_sharpP_complete : SharpP.Complete SharpClique

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