Hardness of the feedback problems

Two quantifier-free first-order reductions, both of dimension 1:

• DescriptiveComplexity.vertexCover_fo_reduction_feedbackVertexSet: Vertex Cover reduces to Feedback Vertex Set, by symmetrizing the adjacency relation off the diagonal (DescriptiveComplexity.symmetrizeInterp, tag Unit). Every edge of the input becomes a 2-cycle, so a set of vertices kills every cycle iff it meets every edge – killing all 2-cycles already removes every arc (DescriptiveComplexity.coverOn_iff_feedbackOn). The marked set is copied, so there is no counting step at all.

• DescriptiveComplexity.feedbackVertexSet_fo_reduction_feedbackArcSet: Feedback Vertex Set reduces to Feedback Arc Set, by the classical vertex splitting (DescriptiveComplexity.splitInterp, tag Bool): each vertex v becomes an in-copy DescriptiveComplexity.inPt and an out-copy DescriptiveComplexity.outPt joined by an internal arc, and each arc (u, v) of the input becomes the crossing arc from u's out-copy to v's in-copy. Cutting the internal arc of v is deleting the vertex v; the marked relation marks exactly the internal arcs of the marked vertices, so the threshold is preserved on the nose.

Splitting, without ever manipulating a cycle

The correctness of the splitting is where the certificate form of acyclicity (DescriptiveComplexity.acyclicRel_iff_exists_order) pays off: both directions build a strict partial order out of another one, and no cycle is ever decomposed.

• Forward, a feedback vertex set C of the input with certificate order Lt gives the order DescriptiveComplexity.splitLt: the out-copies of C go to the bottom, the in-copies of C to the top, and everything else keeps Lt (with the in-copy of a vertex just below its out-copy). Every uncut arc goes forward in it – the case that needs Lt is exactly a crossing arc between two vertices outside C, which is a surviving arc of the input.
• Backward, a feedback arc set F of the split graph gives back the set of source vertices of the arcs in F, which is no larger (Set.ncard_image_le), and the order fun u v => Lt' (inPt u) (inPt v). For an input arc (u, v) with both endpoints outside that set, neither the internal arc of u nor the crossing arc (u_out, v_in) can be in F, since both have source vertex u; so both go forward in Lt', and transitivity closes the case.

Vertex Cover reduces to Feedback Vertex Set

def DescriptiveComplexity.symmetrizeInterp : FOInterpretation FirstOrder.Language.markedGraph FirstOrder.Language.markedGraph Unit 1

The symmetrizing interpretation: adjacency becomes off-diagonal adjacency in either direction – so every edge becomes a 2-cycle – and marks are kept.

Equations

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

@[simp]

theorem DescriptiveComplexity.symmetrize_adj {A : Type} [FirstOrder.Language.markedGraph.Structure A] (w₁ w₂ : Fin 1 → A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.mgAdj ![((), w₁), ((), w₂)] ↔ w₁ 0 ≠ w₂ 0 ∧ (FirstOrder.Language.Structure.RelMap FirstOrder.Language.mgAdj ![w₁ 0, w₂ 0] ∨ FirstOrder.Language.Structure.RelMap FirstOrder.Language.mgAdj ![w₂ 0, w₁ 0])

@[simp]

theorem DescriptiveComplexity.symmetrize_marked {A : Type} [FirstOrder.Language.markedGraph.Structure A] (w : Fin 1 → A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.mgMarked ![((), w)] ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.mgMarked ![w 0]

theorem DescriptiveComplexity.hasSmallVertexCover_iff_feedback_map (A : Type) [FirstOrder.Language.markedGraph.Structure A] : HasSmallVertexCover A ↔ HasSmallFeedbackSet (symmetrizeInterp.Map A)

Correctness of the symmetrizing interpretation.

def DescriptiveComplexity.vertexCover_fo_reduction_feedbackVertexSet : FOReduction VertexCover FeedbackVertexSet

Vertex Cover FO-reduces to Feedback Vertex Set, by symmetrizing the adjacency relation: every edge becomes a 2-cycle, so the feedback vertex sets are exactly the vertex covers.

Equations

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

Feedback Vertex Set reduces to Feedback Arc Set

The vertex-splitting interpretation: the tag true carries the in-copy of a vertex and the tag false its out-copy.

def DescriptiveComplexity.splitInterp : FOInterpretation FirstOrder.Language.markedGraph FirstOrder.Language.markedArcGraph Bool 1

The vertex-splitting interpretation: v becomes an in-copy and an out-copy joined by an internal arc, an arc (u, v) becomes the crossing arc from u's out-copy to v's in-copy, and the marked relation marks the internal arcs of the marked vertices.

Equations

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

The two copies of a vertex

The arcs and marks of the split digraph

@[simp]

theorem DescriptiveComplexity.split_adj_in_out {A : Type} [FirstOrder.Language.markedGraph.Structure A] (w₁ w₂ : Fin 1 → A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.magAdj ![(true, w₁), (false, w₂)] ↔ w₁ 0 = w₂ 0

@[simp]

theorem DescriptiveComplexity.split_adj_out_in {A : Type} [FirstOrder.Language.markedGraph.Structure A] (w₁ w₂ : Fin 1 → A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.magAdj ![(false, w₁), (true, w₂)] ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.mgAdj ![w₁ 0, w₂ 0]

@[simp]

theorem DescriptiveComplexity.split_adj_in_in {A : Type} [FirstOrder.Language.markedGraph.Structure A] (w₁ w₂ : Fin 1 → A) : ¬FirstOrder.Language.Structure.RelMap FirstOrder.Language.magAdj ![(true, w₁), (true, w₂)]

@[simp]

theorem DescriptiveComplexity.split_adj_out_out {A : Type} [FirstOrder.Language.markedGraph.Structure A] (w₁ w₂ : Fin 1 → A) : ¬FirstOrder.Language.Structure.RelMap FirstOrder.Language.magAdj ![(false, w₁), (false, w₂)]

@[simp]

theorem DescriptiveComplexity.split_marked_in_out {A : Type} [FirstOrder.Language.markedGraph.Structure A] (w₁ w₂ : Fin 1 → A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.magMarked ![(true, w₁), (false, w₂)] ↔ w₁ 0 = w₂ 0 ∧ FirstOrder.Language.Structure.RelMap FirstOrder.Language.mgMarked ![w₁ 0]

@[simp]

theorem DescriptiveComplexity.split_marked_in_in {A : Type} [FirstOrder.Language.markedGraph.Structure A] (w₁ w₂ : Fin 1 → A) : ¬FirstOrder.Language.Structure.RelMap FirstOrder.Language.magMarked ![(true, w₁), (true, w₂)]

@[simp]

theorem DescriptiveComplexity.split_marked_out_in {A : Type} [FirstOrder.Language.markedGraph.Structure A] (w₁ w₂ : Fin 1 → A) : ¬FirstOrder.Language.Structure.RelMap FirstOrder.Language.magMarked ![(false, w₁), (true, w₂)]

@[simp]

theorem DescriptiveComplexity.split_marked_out_out {A : Type} [FirstOrder.Language.markedGraph.Structure A] (w₁ w₂ : Fin 1 → A) : ¬FirstOrder.Language.Structure.RelMap FirstOrder.Language.magMarked ![(false, w₁), (false, w₂)]

The interface used by the correctness proofs

Rather than the raw characterizations, the proofs below use the two arc constructors and the two “only these” lemmas, which never mention the shape of an element of the interpreted universe.

Counting on the internal arcs

Correctness of the splitting

theorem DescriptiveComplexity.hasSmallFeedbackSet_iff_feedbackArc_map (A : Type) [FirstOrder.Language.markedGraph.Structure A] : HasSmallFeedbackSet A ↔ HasSmallFeedbackArcSet (splitInterp.Map A)

Correctness of the vertex splitting: a graph has a feedback vertex set at most as large as its marked set iff the split digraph has a feedback arc set at most as large as its marked relation.

def DescriptiveComplexity.feedbackVertexSet_fo_reduction_feedbackArcSet : FOReduction FeedbackVertexSet FeedbackArcSet

Feedback Vertex Set FO-reduces to Feedback Arc Set, by vertex splitting: deleting a vertex becomes cutting its internal arc.

Equations

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