The conflict split graph: feedback arc sets with no slack

The graph behind the parsimonious hardness of #Feedback Arc Set, on a vertex type of its own (DescriptiveComplexity.SplitBundle.SB).

The textbook reduction to Feedback Arc Set splits each vertex a into an internal arc vin a → vout a, cutting which stands for removing a. It is not parsimonious, for two reasons, and the graph of this file removes both.

• A crossing arc can be cut instead of an internal one. Here two vertices in conflict are joined by two parallel paths in each direction (vout a → mid j a b → vin b, j : Bool), so a crossing arc alone cuts nothing, and cutting a whole bundle costs two arcs where an internal arc costs one.
• A solution can be padded: a superset of a feedback arc set is one. So the instance has to leave no slack, and that is a property of the source. The conflict relation here is “distinct and not adjacent both ways” in a graph whose cliques are at most as large as the marked set (the promise of DescriptiveComplexity.SplitBundle.card_fas_eq_card_clique), and the threshold is the number of unmarked vertices. Keeping an internal arc is keeping a vertex, the kept vertices have to be pairwise adjacent, and there are too many of them to keep unless nothing is wasted.

The count then goes through (DescriptiveComplexity.SplitBundle.internal_of_fas): a feedback arc set of the threshold size with b arcs outside the internal ones cuts at most b / 2 bundles, the vertices that are neither cut nor at the source of a cut bundle form a clique, and the promise bounds that clique. Hence b = 0: the feedback arc sets of the threshold size are the complements of the cliques of the threshold size, bijectively.

A graph with no marked vertex has one clique of the threshold size, the empty one, and no promise to offer; it is sent to the graph with no arc.

inductive DescriptiveComplexity.SplitBundle.SB (A : Type) : Type

The vertices of the conflict split graph.

• vin {A : Type} (a : A) : SB A

  The entry copy of a vertex.

• vout {A : Type} (a : A) : SB A

  The exit copy of a vertex.

• mid {A : Type} (j : Bool) (a b : A) : SB A

  The middle of one of the two parallel paths from a to b.

instance DescriptiveComplexity.SplitBundle.instFiniteSB {A : Type} [Finite A] : Finite (SB A)

def DescriptiveComplexity.SplitBundle.Conf {A : Type} (Adj : A → A → Prop) (a b : A) : Prop

Two vertices are in conflict: distinct, and not adjacent both ways.

Equations

• DescriptiveComplexity.SplitBundle.Conf Adj a b = (a ≠ b ∧ (¬Adj a b ∨ ¬Adj b a))

theorem DescriptiveComplexity.SplitBundle.Conf.symm {A : Type} {Adj : A → A → Prop} {a b : A} (h : Conf Adj a b) : Conf Adj b a

def DescriptiveComplexity.SplitBundle.SArc {A : Type} (Adj : A → A → Prop) (K : A → Prop) : SB A → SB A → Prop

The arcs of the conflict split graph – none if no vertex is marked.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.SplitBundle.SArc Adj K (DescriptiveComplexity.SplitBundle.SB.vin a) (DescriptiveComplexity.SplitBundle.SB.vout b) = ((∃ (z : A), K z) ∧ a = b)
• DescriptiveComplexity.SplitBundle.SArc Adj K x✝¹ x✝ = False

def DescriptiveComplexity.SplitBundle.SMark {A : Type} (K : A → Prop) : SB A → SB A → Prop

The marked arcs: the internal arcs of the unmarked vertices.

Equations

• DescriptiveComplexity.SplitBundle.SMark K (DescriptiveComplexity.SplitBundle.SB.vin a) (DescriptiveComplexity.SplitBundle.SB.vout b) = ((∃ (z : A), K z) ∧ a = b ∧ ¬K a)
• DescriptiveComplexity.SplitBundle.SMark K x✝¹ x✝ = False

def DescriptiveComplexity.SplitBundle.FS {A : Type} (S : A → Prop) : SB A → SB A → Prop

The feedback arc set of a set of vertices: the internal arcs of the others.

Equations

• DescriptiveComplexity.SplitBundle.FS S (DescriptiveComplexity.SplitBundle.SB.vin a) (DescriptiveComplexity.SplitBundle.SB.vout b) = (a = b ∧ ¬S a)
• DescriptiveComplexity.SplitBundle.FS S x✝¹ x✝ = False

From a clique to a feedback arc set

From a feedback arc set to a clique

theorem DescriptiveComplexity.SplitBundle.internal_of_fas {A : Type} (Adj : A → A → Prop) (K : A → Prop) [Finite A] (hK : ∃ (z : A), K z) (hP : ∀ (S : A → Prop), (∀ (x y : A), S x → S y → x ≠ y → Adj x y) → {x : A | S x}.ncard ≤ {x : A | K x}.ncard) {F : SB A → SB A → Prop} (hF : FasOfSizeOn (SArc Adj K) (SMark K) F) : (CliqueOfSizeOn Adj K fun (a : A) => ¬F (SB.vin a) (SB.vout a)) ∧ F = FS fun (a : A) => ¬F (SB.vin a) (SB.vout a)

A feedback arc set of the threshold size consists of internal arcs, and the vertices it keeps are a clique of the threshold size – provided no clique is larger than the marked set.

theorem DescriptiveComplexity.SplitBundle.card_fas_eq_card_clique {A : Type} (Adj : A → A → Prop) (K : A → Prop) [Finite A] (hprom : (¬∃ (z : A), K z) ∨ ∀ (S : A → Prop), (∀ (x y : A), S x → S y → x ≠ y → Adj x y) → {x : A | S x}.ncard ≤ {x : A | K x}.ncard) : Nat.card { F : SB A → SB A → Prop // FasOfSizeOn (SArc Adj K) (SMark K) F } = Nat.card { S : A → Prop // CliqueOfSizeOn Adj K S }

The feedback arc sets of the threshold size of the conflict split graph are the cliques of the threshold size, as many: provided the graph has no marked vertex, or no clique larger than its marked set.