The feedback problems are NP-complete

Umbrella file for Feedback Vertex Set and Feedback Arc Set (DescriptiveComplexity.FeedbackVertexSet, DescriptiveComplexity.FeedbackArcSet, defined in DescriptiveComplexity.Problems.Feedback.Defs), collecting the quantifier-free reductions of DescriptiveComplexity.Problems.Feedback.Reductions and deriving NP-completeness from

• DescriptiveComplexity.feedbackVertexSet_sigmaSODefinable and DescriptiveComplexity.feedbackArcSet_sigmaSODefinable (DescriptiveComplexity.Problems.Feedback.Membership): membership, by guessing the removed object, an order certifying acyclicity, and the threshold injection;
• DescriptiveComplexity.vertexCover_fo_reduction_feedbackVertexSet: hardness of Feedback Vertex Set, from the NP-hardness of Vertex Cover (DescriptiveComplexity.Problems.CliqueFamily), and so ultimately from the Cook–Levin theorem, with no machine model anywhere;
• DescriptiveComplexity.feedbackVertexSet_fo_reduction_feedbackArcSet: hardness of Feedback Arc Set, one step further along the chain.

The two problems live over different vocabularies – Feedback Vertex Set over marked graphs, Feedback Arc Set over arc-marked digraphs – because their thresholds count different things, so there is no analogue here of the transposition inside the set family: the chain Vertex Cover ≤ᶠᵒ Feedback Vertex Set ≤ᶠᵒ Feedback Arc Set is one-way. As with any complexity-theoretic statement, these results are about finite structures only (DescriptiveComplexity.ComplexityClass.mem_congr_finite/hard_congr_finite).

noncomputable def DescriptiveComplexity.vertexCover_fo_reduction_feedbackArcSet : FOReduction VertexCover FeedbackArcSet

Vertex Cover FO-reduces to Feedback Arc Set, by composing the symmetrization with the vertex splitting.

Equations

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

NP-completeness

theorem DescriptiveComplexity.feedbackVertexSet_mem_NP : NP.Mem FeedbackVertexSet

Feedback Vertex Set is in NP: it is Σ₁-definable.

theorem DescriptiveComplexity.feedbackVertexSet_NP_hard : NP.Hard FeedbackVertexSet

Feedback Vertex Set is NP-hard: Vertex Cover, which is NP-hard, reduces to it by symmetrizing the adjacency relation.

theorem DescriptiveComplexity.feedbackVertexSet_NP_complete : NP.Complete FeedbackVertexSet

Feedback Vertex Set is NP-complete, derived from the first-order reductions of this library and the Cook–Levin theorem.

theorem DescriptiveComplexity.feedbackArcSet_mem_NP : NP.Mem FeedbackArcSet

Feedback Arc Set is in NP: it is Σ₁-definable.

theorem DescriptiveComplexity.feedbackArcSet_NP_hard : NP.Hard FeedbackArcSet

Feedback Arc Set is NP-hard: Feedback Vertex Set, which is NP-hard, reduces to it by vertex splitting.

theorem DescriptiveComplexity.feedbackArcSet_NP_complete : NP.Complete FeedbackArcSet

Feedback Arc Set is NP-complete.