#Feedback Arc Set is parsimoniously #P-complete

DescriptiveComplexity.sharpFeedbackArcSet_sharpP_parsimoniousComplete, by a reduction from #1-in-SAT (DescriptiveComplexity.sharpOneInSat_ordered_parsimonious_sharpFeedbackArcSet).

The reduction is the composite of two interpretations, and the second is correct only on the outputs of the first:

• DescriptiveComplexity.OneInToClique.oneInToClique sends a CNF formula to a marked graph whose cliques of the threshold size are its exactly-one models – and which has no larger clique (DescriptiveComplexity.OneInToClique.ncard_clique_le);
• DescriptiveComplexity.CliqueFas.cliqueFasInterp sends a marked graph to its conflict split graph (DescriptiveComplexity.Problems.Feedback.SplitBundle), whose feedback arc sets of the threshold size are the cliques of the threshold size of the graph provided it has no larger clique (DescriptiveComplexity.CliqueFas.sharpFeedbackArcSet_cliqueFas).

So this is not a reduction from #Clique: on a graph with a clique above the threshold the second interpretation counts too much, a feedback arc set being free to waste arcs. A composition under a promise is what DescriptiveComplexity.OrderedParsimoniousReduction.transPromise provides.

The tagged pairs that are no vertex of the split graph are isolated, and an isolated vertex changes nothing to a set of arcs (DescriptiveComplexity.fasOfSizeOnEmbEquiv): no domain formula is needed.

Feedback arc sets ignore isolated vertices

The interpretation

inductive DescriptiveComplexity.CliqueFas.SBTag : Type

Tags of the interpretation: the kinds of vertices of the conflict split graph.

• vin : SBTag

  The entry copy of a vertex, at diagonal pairs.

• vout : SBTag

  The exit copy of a vertex, at diagonal pairs.

• mid (j : Bool) : SBTag

  The middle of one of the two paths from the first component to the second.

@[instance_reducible]

instance DescriptiveComplexity.CliqueFas.instDecidableEqSBTag : DecidableEq SBTag

Equations

• DescriptiveComplexity.CliqueFas.instDecidableEqSBTag = DescriptiveComplexity.CliqueFas.instDecidableEqSBTag.decEq

def DescriptiveComplexity.CliqueFas.instDecidableEqSBTag.decEq (x✝ x✝¹ : SBTag) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.CliqueFas.instDecidableEqSBTag.decEq DescriptiveComplexity.CliqueFas.SBTag.vin DescriptiveComplexity.CliqueFas.SBTag.vin = isTrue ⋯
• DescriptiveComplexity.CliqueFas.instDecidableEqSBTag.decEq DescriptiveComplexity.CliqueFas.SBTag.vin (DescriptiveComplexity.CliqueFas.SBTag.mid j) = isFalse ⋯
• DescriptiveComplexity.CliqueFas.instDecidableEqSBTag.decEq DescriptiveComplexity.CliqueFas.SBTag.vout DescriptiveComplexity.CliqueFas.SBTag.vout = isTrue ⋯
• DescriptiveComplexity.CliqueFas.instDecidableEqSBTag.decEq DescriptiveComplexity.CliqueFas.SBTag.vout (DescriptiveComplexity.CliqueFas.SBTag.mid j) = isFalse ⋯
• DescriptiveComplexity.CliqueFas.instDecidableEqSBTag.decEq (DescriptiveComplexity.CliqueFas.SBTag.mid j) DescriptiveComplexity.CliqueFas.SBTag.vin = isFalse ⋯
• DescriptiveComplexity.CliqueFas.instDecidableEqSBTag.decEq (DescriptiveComplexity.CliqueFas.SBTag.mid j) DescriptiveComplexity.CliqueFas.SBTag.vout = isFalse ⋯

instance DescriptiveComplexity.CliqueFas.instFiniteSBTag : Finite SBTag

instance DescriptiveComplexity.CliqueFas.instNonemptySBTag : Nonempty SBTag

def DescriptiveComplexity.CliqueFas.adjF {α : Type} (x y : α) : FirstOrder.Language.markedGraph.Formula α

x and y are adjacent, as a formula.

Equations

• DescriptiveComplexity.CliqueFas.adjF x y = FirstOrder.Language.mgAdj.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

def DescriptiveComplexity.CliqueFas.eqF {α : Type} (x y : α) : FirstOrder.Language.markedGraph.Formula α

x = y, as a formula.

Equations

• DescriptiveComplexity.CliqueFas.eqF x y = (FirstOrder.Language.var x).equal (FirstOrder.Language.var y)

noncomputable def DescriptiveComplexity.CliqueFas.gateF {α : Type} : FirstOrder.Language.markedGraph.Formula α

Some vertex is marked, as a formula.

Equations

• DescriptiveComplexity.CliqueFas.gateF = FirstOrder.Language.Formula.iExs Unit (FirstOrder.Language.mgMarked.formula₁ (FirstOrder.Language.var (Sum.inr ())))

def DescriptiveComplexity.CliqueFas.confF {α : Type} (x y : α) : FirstOrder.Language.markedGraph.Formula α

x and y are in conflict, as a formula.

Equations

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

noncomputable def DescriptiveComplexity.CliqueFas.arcF : SBTag → SBTag → FirstOrder.Language.markedGraph.Formula (Fin 2 × Fin 2)

The arc formulas of the conflict split graph, by tags. The free variable (i, j) is the j-th component of the i-th vertex.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.CliqueFas.arcF x✝¹ x✝ = ⊥

noncomputable def DescriptiveComplexity.CliqueFas.markF : SBTag → SBTag → FirstOrder.Language.markedGraph.Formula (Fin 2 × Fin 2)

The mark formulas, by tags: the internal arcs of the unmarked vertices.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.CliqueFas.markF x✝¹ x✝ = ⊥

noncomputable def DescriptiveComplexity.CliqueFas.cliqueFasInterp : FOInterpretation FirstOrder.Language.markedGraph FirstOrder.Language.markedArcGraph SBTag 2

The interpretation drawing the conflict split graph of a marked graph.

Equations

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

The interpreted graph is the conflict split graph, plus isolated points

theorem DescriptiveComplexity.CliqueFas.sharpFeedbackArcSet_cliqueFas (H : Type) [FirstOrder.Language.markedGraph.Structure H] [Finite H] (hprom : (¬∃ (z : H), MGMarked z) ∨ ∀ (S : H → Prop), (∀ (x y : H), S x → S y → x ≠ y → MGAdj x y) → {x : H | S x}.ncard ≤ {x : H | MGMarked x}.ncard) : SharpFeedbackArcSet.Count (cliqueFasInterp.Map H) = SharpClique.Count H

Correctness of the interpretation, under the promise: on a marked graph with no marked vertex, or with no clique larger than its marked set, the feedback arc sets of the threshold size of the conflict split graph are as many as the cliques of the threshold size.

The promise, and a composition under it

theorem DescriptiveComplexity.OneInToClique.ncard_clique_le {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] (hne : ∃ (p : oneInToClique.Map A), MGMarked p) {S : oneInToClique.Map A → Prop} (hS : ∀ (p q : oneInToClique.Map A), S p → S q → p ≠ q → MGAdj p q) : {p : oneInToClique.Map A | S p}.ncard ≤ {p : oneInToClique.Map A | MGMarked p}.ncard

The clique instance of a CNF formula has no clique larger than its marked set, as soon as it has a marked vertex: a clique with two vertices fills distinct slots, and one vertex is no more than two per clause.

def DescriptiveComplexity.FOInterpretation.liftOrd {L₂ L₃ : FirstOrder.Language} {Tag : Type} {d : ℕ} (f : FOInterpretation L₂ L₃ Tag d) : FOInterpretation (L₂.sum FirstOrder.Language.order) L₃ Tag d

An order-free interpretation, over the ordered expansion: its formulas ignore the order.

Equations

• f.liftOrd = { relFormula := fun {n : ℕ} (R : L₃.Relations n) (t : Fin n → Tag) => FirstOrder.Language.LHom.sumInl.onFormula (f.relFormula R t) }

def DescriptiveComplexity.FOInterpretation.liftOrdLEquiv {L₂ L₃ : FirstOrder.Language} [L₃.IsRelational] {Tag : Type} {d : ℕ} (f : FOInterpretation L₂ L₃ Tag d) (A : Type) [L₂.Structure A] [LinearOrder A] : L₃.Equiv (f.Map A) (f.liftOrd.Map A)

Lifting an interpretation to the ordered expansion does not change the structure it defines.

Equations

• f.liftOrdLEquiv A = { toEquiv := Equiv.refl (f.Map A), map_fun' := ⋯, map_rel' := ⋯ }

noncomputable def DescriptiveComplexity.OrderedParsimoniousReduction.transPromise {L₁ L₂ L₃ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] [L₃.IsRelational] {C : CountingProblem L₁} {D : CountingProblem L₂} {E : CountingProblem L₃} (g : OrderedParsimoniousReduction C D) {Tag : Type} [Finite Tag] [Nonempty Tag] {d : ℕ} (f : FOInterpretation L₂ L₃ Tag d) (hf : ∀ (A : Type) [inst : L₁.Structure A] [inst_1 : LinearOrder A] [Finite A] [Nonempty A], D.Count (g.toInterpretation.Map A) = E.Count (f.Map (g.toInterpretation.Map A))) : OrderedParsimoniousReduction C E

Composition under a promise: an ordered parsimonious reduction followed by an interpretation that is only known to preserve the count on the outputs of the reduction. This is what a reduction through instances with no slack needs, the second step being wrong on the others.

Equations

• g.transPromise f hf = { Tag := Tag × (Fin d → g.Tag), tagFinite := ⋯, tagNonempty := ⋯, dim := d * g.dim, toInterpretation := f.liftOrd.comp g.toInterpretation.ordExtend, correct := ⋯ }

noncomputable def DescriptiveComplexity.sharpOneInSat_ordered_parsimonious_sharpFeedbackArcSet : OrderedParsimoniousReduction SharpOneInSAT SharpFeedbackArcSet

#1-in-SAT reduces parsimoniously to #Feedback Arc Set: the clique instance of the formula, then its conflict split graph.

Equations

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

theorem DescriptiveComplexity.sharpFeedbackArcSet_sharpP_parsimoniousHard : SharpP.ParsimoniousHard SharpFeedbackArcSet

#Feedback Arc Set is parsimoniously #P-hard.

theorem DescriptiveComplexity.sharpFeedbackArcSet_sharpP_parsimoniousComplete : SharpP.ParsimoniousComplete SharpFeedbackArcSet

#Feedback Arc Set is parsimoniously #P-complete, counting the feedback arc sets of exactly the threshold size. Registered in the Lax archive as Lax280166.FeedbackArcSetComplete.sharpFeedbackArcSet_sharpP_parsimoniousComplete.

theorem DescriptiveComplexity.sharpFeedbackArcSet_sharpP_complete : SharpP.Complete SharpFeedbackArcSet

SharpFeedbackArcSet is #P-complete: parsimoniously, hence under subtractive reductions.