Feedback Vertex Set and Feedback Arc Set: definitions

The two feedback problems of Karp 1972 on directed graphs – the adjacency relation of a structure is an arbitrary binary relation, so a FirstOrder.Language.markedGraph-structure already is a digraph:

• DescriptiveComplexity.FeedbackVertexSet: is there a set of at most k vertices whose removal leaves an acyclic digraph? The threshold k is the cardinality of the marked set, the unary encoding of DescriptiveComplexity.Numbers.Unary, so the vocabulary is that of marked graphs;
• DescriptiveComplexity.FeedbackArcSet: is there a set of at most k arcs whose removal leaves an acyclic digraph? Its objective counts arcs, and a set of arcs can have quadratically many elements, which a marked subset of the universe cannot reach. The threshold therefore moves one arity up: the vocabulary FirstOrder.Language.markedArcGraph marks a binary relation, and the number it encodes is the Set.ncard of the corresponding set of pairs (DescriptiveComplexity.nonempty_embedding_iff_ncard_le₂). This is still the unary encoding – order-free and isomorphism-invariant – simply read at arity 2.

Acyclicity, and why it stays first-order checkable

Acyclicity is a transitive-closure condition (DescriptiveComplexity.AcyclicRel: no vertex is reachable from itself along a nonempty path, Relation.TransGen supplying “nonempty path”), so it is not first-order. It is however equivalent to the existence of a strict partial order containing every surviving arc (DescriptiveComplexity.acyclicRel_iff_exists_order) – the order being the transitive closure itself in the interesting direction. Guessing that order alongside the removed set is what puts both problems in Σ₁ (DescriptiveComplexity.Problems.Feedback.Membership), and it is also what makes the reduction of DescriptiveComplexity.Problems.Feedback.Reductions provable without any manipulation of cycles: each direction builds an order from another one.

Both problems are instances of the same generic property of a relation on a type – DescriptiveComplexity.FeedbackOn removes vertices, DescriptiveComplexity.FeedbackArcOn removes arcs – with the same acyclicity kit underneath, which is what the shared certificate lemmas exploit.

Self-loops are cycles under this reading, as they should be: a self-loop at a vertex forces that vertex (resp. that arc) into the removed set.

inductive FirstOrder.Language.markedArcGraphRel : ℕ → Type

Relation symbols of the language of arc-marked digraphs.

• adj : markedArcGraphRel 2

  adj a b: there is an arc from a to b.

• markedArc : markedArcGraphRel 2

  markedArc a b: the pair (a, b) belongs to the marked relation.

def FirstOrder.Language.instDecidableEqMarkedArcGraphRel.decEq {a✝ : ℕ} (x✝ x✝¹ : markedArcGraphRel a✝) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance FirstOrder.Language.instDecidableEqMarkedArcGraphRel {a✝ : ℕ} : DecidableEq (markedArcGraphRel a✝)

Equations

• FirstOrder.Language.instDecidableEqMarkedArcGraphRel = FirstOrder.Language.instDecidableEqMarkedArcGraphRel.decEq

def FirstOrder.Language.markedArcGraph : Language

The relational language of arc-marked digraphs: a digraph together with a marked binary relation, whose cardinality (as a set of pairs) serves as threshold.

Equations

• FirstOrder.Language.markedArcGraph = { Functions := fun (x : ℕ) => Empty, Relations := FirstOrder.Language.markedArcGraphRel }

instance FirstOrder.Language.instIsRelationalMarkedArcGraph : Language.markedArcGraph.IsRelational

@[reducible, inline]

abbrev FirstOrder.Language.magAdj : Language.markedArcGraph.Relations 2

The adjacency symbol of arc-marked digraphs.

Equations

• FirstOrder.Language.magAdj = FirstOrder.Language.markedArcGraphRel.adj

@[reducible, inline]

abbrev FirstOrder.Language.magMarked : Language.markedArcGraph.Relations 2

The mark symbol of arc-marked digraphs.

Equations

• FirstOrder.Language.magMarked = FirstOrder.Language.markedArcGraphRel.markedArc

Acyclicity and its first-order certificate

def DescriptiveComplexity.AcyclicRel {A : Type} (R : A → A → Prop) : Prop

A relation is acyclic if no element is reachable from itself along a nonempty path.

Equations

• DescriptiveComplexity.AcyclicRel R = ∀ (x : A), ¬Relation.TransGen R x x

theorem DescriptiveComplexity.acyclicRel_iff_exists_order {A : Type} (R : A → A → Prop) : AcyclicRel R ↔ ∃ (Lt : A → A → Prop), (∀ (x y z : A), Lt x y → Lt y z → Lt x z) ∧ (∀ (x : A), ¬Lt x x) ∧ ∀ (a b : A), R a b → Lt a b

Acyclicity is first-order certifiable: a relation is acyclic exactly when some strict partial order contains it. The order is the transitive closure in one direction; in the other, a cycle would give Lt x x. This is what a Σ₁ definition guesses, and what the reductions between the two feedback problems build.

theorem DescriptiveComplexity.AcyclicRel.of_equiv {A B : Type} (u : B ≃ A) {RB : B → B → Prop} {RA : A → A → Prop} (hR : ∀ (a a' : A), RA a a' → RB (u.symm a) (u.symm a')) (h : AcyclicRel RB) : AcyclicRel RA

Acyclicity transports along an equivalence commuting with the two relations.

The generic properties

def DescriptiveComplexity.SurvivingArc {A : Type} (Adjp : A → A → Prop) (Cp : A → Prop) (a b : A) : Prop

An arc surviving the removal of the Cp-vertices: both endpoints are outside Cp and the arc is present.

Equations

• DescriptiveComplexity.SurvivingArc Adjp Cp a b = (¬Cp a ∧ ¬Cp b ∧ Adjp a b)

def DescriptiveComplexity.UncutArc {A : Type} (Adjp Fp : A → A → Prop) (a b : A) : Prop

An arc surviving the removal of the Fp-arcs: the arc is present and not removed.

Equations

• DescriptiveComplexity.UncutArc Adjp Fp a b = (Adjp a b ∧ ¬Fp a b)

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

Some set of vertices whose removal makes the digraph acyclic is at most as large as the number encoded by the Kp-marked elements: “some feedback vertex set is at most as large as the marked set”.

Equations

• DescriptiveComplexity.FeedbackOn Adjp Kp = ∃ (C : A → Prop), DescriptiveComplexity.AcyclicRel (DescriptiveComplexity.SurvivingArc Adjp C) ∧ {x : A | C x}.ncard ≤ {x : A | Kp x}.ncard

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

Some set of arcs whose removal makes the digraph acyclic is at most as large as the number encoded by the Kp-marked pairs: “some feedback arc set is at most as large as the marked relation”.

Equations

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

The certified forms

The shape the second-order definitions guess: the removed set (of vertices or of arcs), a strict partial order certifying that what survives is acyclic, and an injection into the marked set (resp. the marked relation) witnessing the threshold.

theorem DescriptiveComplexity.feedbackOn_iff_certificate {A : Type} [Finite A] (Adjp : A → A → Prop) (Kp : A → Prop) : FeedbackOn Adjp Kp ↔ ∃ (C : A → Prop), (∃ (Lt : A → A → Prop), (∀ (x y z : A), Lt x y → Lt y z → Lt x z) ∧ (∀ (x : A), ¬Lt x x) ∧ ∀ (a b : A), SurvivingArc Adjp C a b → Lt a b) ∧ Nonempty ({ x : A // C x } ↪ { x : A // Kp x })

The feedback-vertex-set property, with acyclicity certified by an order and the threshold by an injection.

theorem DescriptiveComplexity.feedbackArcOn_iff_certificate {A : Type} [Finite A] (Adjp Kp : A → A → Prop) : FeedbackArcOn Adjp Kp ↔ ∃ (F : A → A → Prop), (∃ (Lt : A → A → Prop), (∀ (x y z : A), Lt x y → Lt y z → Lt x z) ∧ (∀ (x : A), ¬Lt x x) ∧ ∀ (a b : A), UncutArc Adjp F a b → Lt a b) ∧ Nonempty ({ p : A × A // F p.1 p.2 } ↪ { p : A × A // Kp p.1 p.2 })

The feedback-arc-set property, with acyclicity certified by an order and the threshold by an injection of pairs.

Transport along equivalences

theorem DescriptiveComplexity.FeedbackOn.of_equiv {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)) (h : FeedbackOn AdjB KB) : FeedbackOn AdjA KA

FeedbackOn transports along an equivalence commuting with the two predicates.

theorem DescriptiveComplexity.FeedbackArcOn.of_equiv {A B : Type} (u : B ≃ A) {AdjB KB : B → B → Prop} {AdjA KA : A → A → Prop} (hadj : ∀ (b b' : B), AdjB b b' ↔ AdjA (u b) (u b')) (hK : ∀ (b b' : B), KB b b' ↔ KA (u b) (u b')) (h : FeedbackArcOn AdjB KB) : FeedbackArcOn AdjA KA

FeedbackArcOn transports along an equivalence commuting with the two relations.

theorem DescriptiveComplexity.FeedbackOn.equiv_iff {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)) : FeedbackOn AdjB KB ↔ FeedbackOn AdjA KA

FeedbackOn transports along an equivalence, iff version.

theorem DescriptiveComplexity.FeedbackArcOn.equiv_iff {A B : Type} (u : B ≃ A) {AdjB KB : B → B → Prop} {AdjA KA : A → A → Prop} (hadj : ∀ (b b' : B), AdjB b b' ↔ AdjA (u b) (u b')) (hK : ∀ (b b' : B), KB b b' ↔ KA (u b) (u b')) : FeedbackArcOn AdjB KB ↔ FeedbackArcOn AdjA KA

FeedbackArcOn transports along an equivalence, iff version.

Vertex covers are feedback vertex sets of the symmetrized graph

theorem DescriptiveComplexity.coverOn_iff_feedbackOn {A : Type} (Adjp : A → A → Prop) (Kp : A → Prop) : CoverOn Adjp Kp ↔ FeedbackOn (fun (x y : A) => x ≠ y ∧ (Adjp x y ∨ Adjp y x)) Kp

The reduction of Vertex Cover, semantically: a set meets every edge of a digraph iff it kills every cycle of the digraph symmetrized off the diagonal. Killing all 2-cycles already removes every arc, which is why no cycle of any length survives.

The two problems

def DescriptiveComplexity.MAGAdj {A : Type} [FirstOrder.Language.markedArcGraph.Structure A] (a b : A) : Prop

Adjacency in an arc-marked digraph.

Equations

• DescriptiveComplexity.MAGAdj a b = FirstOrder.Language.Structure.RelMap FirstOrder.Language.magAdj ![a, b]

def DescriptiveComplexity.MAGMarked {A : Type} [FirstOrder.Language.markedArcGraph.Structure A] (a b : A) : Prop

Membership in the marked relation of an arc-marked digraph.

Equations

• DescriptiveComplexity.MAGMarked a b = FirstOrder.Language.Structure.RelMap FirstOrder.Language.magMarked ![a, b]

def DescriptiveComplexity.HasSmallFeedbackSet (A : Type) [FirstOrder.Language.markedGraph.Structure A] : Prop

A marked graph has a feedback vertex set at most as large as its marked set. (Finiteness of the universe is part of the property: cardinality thresholds are only meaningful on finite structures.)

Equations

• DescriptiveComplexity.HasSmallFeedbackSet A = (Finite A ∧ DescriptiveComplexity.FeedbackOn DescriptiveComplexity.MGAdj DescriptiveComplexity.MGMarked)

def DescriptiveComplexity.HasSmallFeedbackArcSet (A : Type) [FirstOrder.Language.markedArcGraph.Structure A] : Prop

An arc-marked digraph has a feedback arc set at most as large as its marked relation.

Equations

• DescriptiveComplexity.HasSmallFeedbackArcSet A = (Finite A ∧ DescriptiveComplexity.FeedbackArcOn DescriptiveComplexity.MAGAdj DescriptiveComplexity.MAGMarked)

theorem DescriptiveComplexity.hasSmallFeedbackSet_iso {A B : Type} [FirstOrder.Language.markedGraph.Structure A] [FirstOrder.Language.markedGraph.Structure B] (e : FirstOrder.Language.markedGraph.Equiv A B) : HasSmallFeedbackSet A ↔ HasSmallFeedbackSet B

The feedback-vertex-set threshold property is isomorphism-invariant.

theorem DescriptiveComplexity.hasSmallFeedbackArcSet_iso {A B : Type} [FirstOrder.Language.markedArcGraph.Structure A] [FirstOrder.Language.markedArcGraph.Structure B] (e : FirstOrder.Language.markedArcGraph.Equiv A B) : HasSmallFeedbackArcSet A ↔ HasSmallFeedbackArcSet B

The feedback-arc-set threshold property is isomorphism-invariant.

def DescriptiveComplexity.FeedbackVertexSet : DecisionProblem FirstOrder.Language.markedGraph

FEEDBACK VERTEX SET, as a problem on marked graphs: is there a set of vertices at most as large as the marked set whose removal leaves an acyclic digraph?

Equations

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

def DescriptiveComplexity.FeedbackArcSet : DecisionProblem FirstOrder.Language.markedArcGraph

FEEDBACK ARC SET, as a problem on arc-marked digraphs: is there a set of arcs at most as large as the marked relation whose removal leaves an acyclic digraph?

Equations

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