#Feedback Vertex Set

The counting version of DescriptiveComplexity.FeedbackVertexSet: the number of sets of vertices, with exactly as many elements as the marked set, whose removal leaves an acyclic digraph (DescriptiveComplexity.FvsOfSize). Its support is Feedback Vertex Set (DescriptiveComplexity.sharpFeedbackVertexSet_support_iff), and it is parsimoniously #P-complete (DescriptiveComplexity.sharpFeedbackVertexSet_sharpP_parsimoniousComplete).

The certificate of acyclicity

Acyclicity is not first-order, and the Σ₁ definition of the decision problem certifies it by a strict partial order containing the surviving arcs (DescriptiveComplexity.acyclicRel_iff_exists_order). There are many – any linear extension will do – so they cannot be counted. The counting kernel asks for the least one, the transitive closure, which is first-order checkable though not first-order definable: a transitive irreflexive relation containing the arcs is their transitive closure as soon as each of its pairs starts with an arc (DescriptiveComplexity.IsAcyclicClosure, DescriptiveComplexity.IsAcyclicClosure.eq_transGen). Irreflexivity is what makes that last condition bite: without it, a relation relating everything to everything on a cycle would pass.

Hardness

The reduction from Vertex Cover of DescriptiveComplexity.Problems.Feedback.Reductions is parsimonious as it stands: it turns every edge into a 2-cycle, so the feedback vertex sets of the output are the vertex covers of the input, the same sets (DescriptiveComplexity.cover_iff_acyclic_symmetrized).

The transitive closure of an acyclic relation, first-order

def DescriptiveComplexity.IsAcyclicClosure {A : Type} (E T : A → A → Prop) : Prop

The relation T is a transitive, irreflexive relation containing E, each pair of which starts with a pair of E: on a finite type, the transitive closure of E, which is then acyclic.

Equations

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

theorem DescriptiveComplexity.IsAcyclicClosure.acyclic {A : Type} {E T : A → A → Prop} (h : IsAcyclicClosure E T) : AcyclicRel E

A relation with such a closure is acyclic.

theorem DescriptiveComplexity.IsAcyclicClosure.eq_transGen {A : Type} [Finite A] {E T : A → A → Prop} (h : IsAcyclicClosure E T) : T = Relation.TransGen E

The certificate is unique: it is the transitive closure.

The generic property

def DescriptiveComplexity.FeedbackOfSizeOn {A : Type} (Adjp : A → A → Prop) (Kp C : A → Prop) : Prop

The removal of the set C leaves an acyclic digraph, and C has exactly as many elements as the Kp-marked set.

Equations

• DescriptiveComplexity.FeedbackOfSizeOn Adjp Kp C = (DescriptiveComplexity.AcyclicRel (DescriptiveComplexity.SurvivingArc Adjp C) ∧ {x : A | C x}.ncard = {x : A | Kp x}.ncard)

def DescriptiveComplexity.feedbackOfSizeEquiv {A B : Type} (u : B ≃ A) {AdjB : B → B → Prop} {KB : B → Prop} {AdjA : A → A → Prop} {KA : A → Prop} (hadj : ∀ (b b' : B), AdjB b b' ↔ AdjA (u b) (u b')) (hK : ∀ (b : B), KB b ↔ KA (u b)) : { C : B → Prop // Finite B ∧ FeedbackOfSizeOn AdjB KB C } ≃ { C : A → Prop // Finite A ∧ FeedbackOfSizeOn AdjA KA C }

The feedback vertex sets of the threshold size transport along an equivalence commuting with the two predicates.

Equations

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

theorem DescriptiveComplexity.cover_iff_acyclic_symmetrized {A : Type} (Adjp : A → A → Prop) (C : A → Prop) : (∀ (x y : A), x ≠ y → Adjp x y → C x ∨ C y) ↔ AcyclicRel (SurvivingArc (fun (x y : A) => x ≠ y ∧ (Adjp x y ∨ Adjp y x)) C)

A set meets every edge iff its removal leaves the symmetrized graph acyclic: every edge has become a 2-cycle, and killing the 2-cycles removes every arc.

The counting problem

def DescriptiveComplexity.FvsOfSize (A : Type) [FirstOrder.Language.markedGraph.Structure A] (C : A → Prop) : Prop

The set C is a feedback vertex set with exactly as many vertices as the marked set, in a finite marked digraph.

Equations

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

noncomputable def DescriptiveComplexity.SharpFeedbackVertexSet : CountingProblem FirstOrder.Language.markedGraph

#Feedback Vertex Set: the number of feedback vertex sets with exactly as many vertices as the marked set.

Equations

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

theorem DescriptiveComplexity.sharpFeedbackVertexSet_support_iff (A : Type) [FirstOrder.Language.markedGraph.Structure A] [Finite A] : SharpFeedbackVertexSet.support.Holds A ↔ FeedbackVertexSet.Holds A

The support of #Feedback Vertex Set is Feedback Vertex Set: a feedback vertex set at most as large as the marked set extends to one of exactly that size. Registered in the Lax archive as Lax280166.FeedbackVertexSetComplete.sharpFeedbackVertexSet_support_iff.

Membership

inductive DescriptiveComplexity.FvsCountBlockIx : Type

The relation variables of the block.

• sel : FvsCountBlockIx

  The removed set.

• tc : FvsCountBlockIx

  The transitive closure of the surviving arcs.

@[reducible, inline]

abbrev DescriptiveComplexity.fcMarkedSym : fvsCountLang.Relations 1

The marked symbol over the sum.

Equations

• DescriptiveComplexity.fcMarkedSym = Sum.inl FirstOrder.Language.mgMarked

def DescriptiveComplexity.fcSelRel : fvsCountBlock.lang.Relations 1

The sel relation variable.

Equations

• DescriptiveComplexity.fcSelRel = ⟨DescriptiveComplexity.FvsCountBlockIx.sel, DescriptiveComplexity.fcSelRel._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.fcSelSym : fvsCountLang.Relations 1

The sel symbol over the sum.

Equations

• DescriptiveComplexity.fcSelSym = Sum.inr DescriptiveComplexity.fcSelRel

@[reducible, inline]

abbrev DescriptiveComplexity.fcTcSym : fvsCountLang.Relations 2

The tc symbol over the sum.

Equations

• DescriptiveComplexity.fcTcSym = Sum.inr DescriptiveComplexity.fcTcRel

def DescriptiveComplexity.fcTcRel : fvsCountBlock.lang.Relations 2

The tc relation variable.

Equations

• DescriptiveComplexity.fcTcRel = ⟨DescriptiveComplexity.FvsCountBlockIx.tc, DescriptiveComplexity.fcTcRel._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.fcAdjSym : fvsCountLang.Relations 2

The adj symbol over the sum.

Equations

• DescriptiveComplexity.fcAdjSym = Sum.inl FirstOrder.Language.mgAdj

def DescriptiveComplexity.fvsCountBlock : SOBlock

The block of the counting definition of Feedback Vertex Set: the removed set, and the transitive closure of the surviving arcs.

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.fvsCountLang : FirstOrder.Language

The vocabulary of the kernel: the instance expanded by the block.

Equations

• DescriptiveComplexity.fvsCountLang = FirstOrder.Language.markedGraph.sum DescriptiveComplexity.fvsCountBlock.lang

@[instance_reducible]

instance DescriptiveComplexity.instFintypeFvsCountBlockIx : Fintype FvsCountBlockIx

Equations

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

@[instance_reducible]

instance DescriptiveComplexity.instDecidableEqFvsCountBlockIx : DecidableEq FvsCountBlockIx

Equations

• DescriptiveComplexity.instDecidableEqFvsCountBlockIx x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

Hardness

theorem DescriptiveComplexity.sharpFeedbackVertexSet_symmetrize_map (A : Type) [FirstOrder.Language.markedGraph.Structure A] : SharpFeedbackVertexSet.Count (symmetrizeInterp.Map A) = SharpVertexCover.Count A

The feedback vertex sets of the symmetrized graph are the vertex covers.

noncomputable def DescriptiveComplexity.sharpVertexCover_parsimonious_sharpFeedbackVertexSet : ParsimoniousReduction SharpVertexCover SharpFeedbackVertexSet

#Vertex Cover reduces parsimoniously to #Feedback Vertex Set, by symmetrizing the adjacency relation.

Equations

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

theorem DescriptiveComplexity.sharpFeedbackVertexSet_sharpP_parsimoniousHard : SharpP.ParsimoniousHard SharpFeedbackVertexSet

#Feedback Vertex Set is parsimoniously #P-hard.

theorem DescriptiveComplexity.sharpFeedbackVertexSet_sharpP_parsimoniousComplete : SharpP.ParsimoniousComplete SharpFeedbackVertexSet

#Feedback Vertex Set is parsimoniously #P-complete, counting the feedback vertex sets of exactly the threshold size. Registered in the Lax archive as Lax280166.FeedbackVertexSetComplete.sharpFeedbackVertexSet_sharpP_parsimoniousComplete.

theorem DescriptiveComplexity.sharpFeedbackVertexSet_sharpP_complete : SharpP.Complete SharpFeedbackVertexSet

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