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).

NP-completeness #

source

theorem DescriptiveComplexity.feedbackVertexSet_mem_NP :

NP.Mem FeedbackVertexSet

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

Dependency graph

source

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.

Dependency graph

source

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. Registered in the Lax archive as Lax799700.Feedback.feedbackVertexSet_NP_complete.

Dependency graph

source

theorem DescriptiveComplexity.feedbackArcSet_mem_NP :

NP.Mem FeedbackArcSet

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

Dependency graph

source

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.

Dependency graph

source

theorem DescriptiveComplexity.feedbackArcSet_NP_complete :

NP.Complete FeedbackArcSet

Feedback Arc Set is NP-complete. Registered in the Lax archive as Lax799700.Feedback.feedbackArcSet_NP_complete.

Dependency graph