#Feedback Arc Set: counting the feedback arc sets of the threshold size

The counting version of DescriptiveComplexity.FeedbackArcSet: the number of sets of arcs, with exactly as many elements as the marked relation, whose removal leaves an acyclic digraph (DescriptiveComplexity.FasOfSize).

A solution is a set of arcs of the graph. The decision problem does not ask for that – removing a pair that is not an arc removes nothing – but a count has to: otherwise every solution could be padded with pairs that are not arcs, in as many ways as there are such pairs.

The support is not the decision problem, for the reason it is not for Set Cover: a feedback arc set smaller than the threshold extends to one of exactly that size only while arcs remain, so with a threshold above the number of arcs Feedback Arc Set may hold and the count be 0. The support is “some feedback arc set has exactly the threshold size” (DescriptiveComplexity.sharpFeedbackArcSet_support_iff).

Membership in #P (DescriptiveComplexity.sharpFeedbackArcSet_mem_sharpP) combines the two unique certificates at hand: the transitive closure for acyclicity (DescriptiveComplexity.IsAcyclicClosure), and the monotone bijection between two sets of pairs for the size (DescriptiveComplexity.sharpPDefinable_of_sizedPairs). Parsimonious hardness is in DescriptiveComplexity.Problems.Feedback.CountingArcHardness.

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

The relation F is a set of arcs whose removal leaves an acyclic digraph, with exactly as many pairs as the marked relation.

Equations

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

def DescriptiveComplexity.fasOfSizeEquiv {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')) : { F : B → B → Prop // Finite B ∧ FasOfSizeOn AdjB KB F } ≃ { F : A → A → Prop // Finite A ∧ FasOfSizeOn AdjA KA F }

The feedback arc sets of the threshold size transport along an equivalence commuting with the two relations.

Equations

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

The counting problem

def DescriptiveComplexity.FasOfSize (A : Type) [FirstOrder.Language.markedArcGraph.Structure A] (F : A → A → Prop) : Prop

The relation F is a feedback arc set with exactly as many arcs as the marked relation has pairs, in a finite arc-marked digraph.

Equations

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

noncomputable def DescriptiveComplexity.SharpFeedbackArcSet : CountingProblem FirstOrder.Language.markedArcGraph

#Feedback Arc Set: the number of feedback arc sets with exactly as many arcs as the marked relation has pairs.

Equations

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

theorem DescriptiveComplexity.sharpFeedbackArcSet_support_iff (A : Type) [FirstOrder.Language.markedArcGraph.Structure A] [Finite A] : SharpFeedbackArcSet.support.Holds A ↔ ∃ (F : A → A → Prop), FasOfSize A F

The support of #Feedback Arc Set: some feedback arc set has exactly the threshold size. Registered in the Lax archive as Lax280166.FeedbackArcSetComplete.sharpFeedbackArcSet_support_iff.

theorem DescriptiveComplexity.feedbackArcSet_of_sharpFeedbackArcSet_support (A : Type) [FirstOrder.Language.markedArcGraph.Structure A] [Finite A] (h : SharpFeedbackArcSet.support.Holds A) : FeedbackArcSet.Holds A

The support of #Feedback Arc Set implies Feedback Arc Set; the converse fails when the threshold exceeds the number of arcs. Registered in the Lax archive as Lax280166.FeedbackArcSetComplete.feedbackArcSet_of_sharpFeedbackArcSet_support.

Membership

@[reducible, inline]

abbrev DescriptiveComplexity.faTcSym : fasCountLang.Relations 2

The tc symbol over the sum.

Equations

• DescriptiveComplexity.faTcSym = Sum.inr DescriptiveComplexity.faTcRel

inductive DescriptiveComplexity.FasCountBlockIx : Type

The relation variables of the block.

• cut : FasCountBlockIx

  The removed arcs.

• tc : FasCountBlockIx

  The transitive closure of the arcs that are not removed.

@[reducible, inline]

abbrev DescriptiveComplexity.faMarkedSym : fasCountLang.Relations 2

The marked symbol over the sum.

Equations

• DescriptiveComplexity.faMarkedSym = Sum.inl FirstOrder.Language.magMarked

@[instance_reducible]

instance DescriptiveComplexity.instDecidableEqFasCountBlockIx : DecidableEq FasCountBlockIx

Equations

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

def DescriptiveComplexity.faCutRel : fasCountBlock.lang.Relations 2

The cut relation variable.

Equations

• DescriptiveComplexity.faCutRel = ⟨DescriptiveComplexity.FasCountBlockIx.cut, DescriptiveComplexity.faCutRel._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.fasCountLang : FirstOrder.Language

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

Equations

• DescriptiveComplexity.fasCountLang = FirstOrder.Language.markedArcGraph.sum DescriptiveComplexity.fasCountBlock.lang

@[reducible, inline]

abbrev DescriptiveComplexity.faAdjSym : fasCountLang.Relations 2

The adj symbol over the sum.

Equations

• DescriptiveComplexity.faAdjSym = Sum.inl FirstOrder.Language.magAdj

@[instance_reducible]

instance DescriptiveComplexity.instFintypeFasCountBlockIx : Fintype FasCountBlockIx

Equations

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

def DescriptiveComplexity.faTcRel : fasCountBlock.lang.Relations 2

The tc relation variable.

Equations

• DescriptiveComplexity.faTcRel = ⟨DescriptiveComplexity.FasCountBlockIx.tc, DescriptiveComplexity.faTcRel._proof_1⟩

def DescriptiveComplexity.fasCountBlock : SOBlock

The block of the counting definition of Feedback Arc Set: the removed arcs, and the transitive closure of the others.

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.faCutSym : fasCountLang.Relations 2

The cut symbol over the sum.

Equations

• DescriptiveComplexity.faCutSym = Sum.inr DescriptiveComplexity.faCutRel

theorem DescriptiveComplexity.sharpFeedbackArcSet_mem_sharpP : SharpP.Mem SharpFeedbackArcSet

#Feedback Arc Set is in #P: the size is certified by the monotone bijection between pairs, and acyclicity by the transitive closure.