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.

theorem DescriptiveComplexity.symmetrizeInterp_isQuantifierFree : symmetrizeInterp.IsQuantifierFree

The symmetrizing interpretation is quantifier-free.

@[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.

theorem DescriptiveComplexity.splitInterp_isQuantifierFree : splitInterp.IsQuantifierFree

The vertex-splitting interpretation is quantifier-free.

The two copies of a vertex

def DescriptiveComplexity.inPt {A : Type} (v : A) : splitInterp.Map A

The in-copy of a vertex in the split digraph.

Equations

• DescriptiveComplexity.inPt v = (true, fun (x : Fin 1) => v)

def DescriptiveComplexity.outPt {A : Type} (v : A) : splitInterp.Map A

The out-copy of a vertex in the split digraph.

Equations

• DescriptiveComplexity.outPt v = (false, fun (x : Fin 1) => v)

theorem DescriptiveComplexity.inPt_injective {A : Type} : Function.Injective inPt

theorem DescriptiveComplexity.inPt_eta {A : Type} (w : Fin 1 → A) : (true, w) = inPt (w 0)

theorem DescriptiveComplexity.outPt_eta {A : Type} (w : Fin 1 → A) : (false, w) = outPt (w 0)

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.

theorem DescriptiveComplexity.split_adj_internal {A : Type} [FirstOrder.Language.markedGraph.Structure A] (v : A) : MAGAdj (inPt v) (outPt v)

The internal arc of a vertex.

theorem DescriptiveComplexity.split_adj_crossing {A : Type} [FirstOrder.Language.markedGraph.Structure A] {u v : A} (h : MGAdj u v) : MAGAdj (outPt u) (inPt v)

The crossing arc attached to an arc of the input.

theorem DescriptiveComplexity.split_adj_cases {A : Type} [FirstOrder.Language.markedGraph.Structure A] {p q : splitInterp.Map A} (h : MAGAdj p q) : (∃ (v : A), p = inPt v ∧ q = outPt v) ∨ ∃ (u : A) (v : A), p = outPt u ∧ q = inPt v ∧ MGAdj u v

The arcs of the split digraph are the internal and the crossing ones.

theorem DescriptiveComplexity.split_marked_cases {A : Type} [FirstOrder.Language.markedGraph.Structure A] {p q : splitInterp.Map A} (h : MAGMarked p q) : ∃ (v : A), MGMarked v ∧ p = inPt v ∧ q = outPt v

The marked arcs of the split digraph are the internal arcs of the marked vertices.

theorem DescriptiveComplexity.split_marked_internal {A : Type} [FirstOrder.Language.markedGraph.Structure A] {v : A} (h : MGMarked v) : MAGMarked (inPt v) (outPt v)

The internal arc of a marked vertex is marked.

Counting on the internal arcs

theorem DescriptiveComplexity.ncard_internal_eq {A : Type} (P : A → Prop) (Q : splitInterp.Map A × splitInterp.Map A → Prop) (hshape : ∀ (pq : splitInterp.Map A × splitInterp.Map A), Q pq → ∃ (v : A), pq = (inPt v, outPt v)) (hP : ∀ (v : A), Q (inPt v, outPt v) ↔ P v) : {pq : splitInterp.Map A × splitInterp.Map A | Q pq}.ncard = {v : A | P v}.ncard

A relation on the split universe that only holds of internal arcs encodes the same number as the set of vertices whose internal arc it holds of.

Correctness of the splitting

def DescriptiveComplexity.cutArcs {A : Type} (C : A → Prop) (p q : splitInterp.Map A) : Prop

The arcs cut by the interpretation for a set C of vertices: the internal arcs of the members of C.

Equations

• DescriptiveComplexity.cutArcs C p q = ∃ (v : A), C v ∧ p = DescriptiveComplexity.inPt v ∧ q = DescriptiveComplexity.outPt v

noncomputable def DescriptiveComplexity.splitLvl {A : Type} (C : A → Prop) (p : splitInterp.Map A) : ℕ

The level of a copy in the order built from a feedback vertex set: the out-copies of removed vertices go to the bottom, their in-copies to the top, everything else in between.

Equations

• DescriptiveComplexity.splitLvl C p = if C (p.2 0) then if p.1 = true then 2 else 0 else 1

noncomputable def DescriptiveComplexity.splitLt {A : Type} (C : A → Prop) (Lt : A → A → Prop) (p q : splitInterp.Map A) : Prop

The order on the split digraph built from a certificate order of the input: levels first, then the input order, with the in-copy of a vertex just below its out-copy.

Equations

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

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.