Documentation

DescriptiveComplexity.Problems.Feedback.Membership

The feedback problems are existential second-order definable #

The membership half of the NP-completeness of both feedback problems: DescriptiveComplexity.feedbackVertexSet_sigmaSODefinable and DescriptiveComplexity.feedbackArcSet_sigmaSODefinable.

Acyclicity is not first-order, but its certificate is (DescriptiveComplexity.acyclicRel_iff_exists_order), so both definitions have the same five-clause shape. A single existential block guesses

the removed object – a set of vertices for Feedback Vertex Set (arity 1), a set of arcs for Feedback Arc Set (arity 2);
a strict partial order certifying that what survives is acyclic (arity 2);
an injection of the removed object into the marked set, witnessing the threshold – arity 2 for Feedback Vertex Set, where it maps vertices to vertices, and arity 4 for Feedback Arc Set, where it maps pairs to pairs, the threshold living one arity up (the unary encoding read at arity 2, see DescriptiveComplexity.nonempty_embedding_iff_ncard_le₂);

and the kernel checks transitivity, irreflexivity, that every surviving arc goes forward in the order, and that the injection is total and injective. The arity-4 atom is the only thing the second definition needs beyond the first, and it costs nothing beyond DescriptiveComplexity.realize_rel₄ (DescriptiveComplexity.Interpretation), Mathlib's Formula.realize_rel₁/₂ stopping at arity 2.

@[reducible, inline]

abbrev DescriptiveComplexity.fvsSOLang :

FirstOrder.Language

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

Equations

DescriptiveComplexity.fvsSOLang = FirstOrder.Language.markedGraph.sum DescriptiveComplexity.feedbackGuessBlock.lang

Instances For

Dependency graph

def DescriptiveComplexity.fLtRel :

feedbackGuessBlock.lang.Relations 2

The lt relation variable.

Equations

DescriptiveComplexity.fLtRel = ⟨DescriptiveComplexity.FeedbackGuessBlockIx.lt, DescriptiveComplexity.fLtRel._proof_1 ⟩

Instances For

Dependency graph

@[instance_reducible]

instance DescriptiveComplexity.instDecidableEqFeedbackGuessBlockIx :

DecidableEq FeedbackGuessBlockIx

Equations

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

Dependency graph

inductive DescriptiveComplexity.FeedbackGuessBlockIx :

The relation variables of the block.

set : FeedbackGuessBlockIx
The guessed removed set.
lt : FeedbackGuessBlockIx
The guessed strict partial order certifying acyclicity.
inj : FeedbackGuessBlockIx
The guessed injection of the removed set into the marked set.

Instances For

Dependency graph

@[reducible, inline]

abbrev DescriptiveComplexity.fSetSym :

fvsSOLang.Relations 1

The set symbol over the sum.

Equations

DescriptiveComplexity.fSetSym = Sum.inr DescriptiveComplexity.fSetRel

Instances For

Dependency graph

@[reducible, inline]

abbrev DescriptiveComplexity.fMarkedSym :

fvsSOLang.Relations 1

The marked symbol over the sum.

Equations

DescriptiveComplexity.fMarkedSym = Sum.inl FirstOrder.Language.mgMarked

Instances For

Dependency graph

@[reducible, inline]

abbrev DescriptiveComplexity.fInjSym :

fvsSOLang.Relations 2

The inj symbol over the sum.

Equations

DescriptiveComplexity.fInjSym = Sum.inr DescriptiveComplexity.fInjRel

Instances For

Dependency graph

@[reducible, inline]

abbrev DescriptiveComplexity.fAdjSym :

fvsSOLang.Relations 2

The adj symbol over the sum.

Equations

DescriptiveComplexity.fAdjSym = Sum.inl FirstOrder.Language.mgAdj

Instances For

Dependency graph

def DescriptiveComplexity.fSetRel :

feedbackGuessBlock.lang.Relations 1

The set relation variable.

Equations

DescriptiveComplexity.fSetRel = ⟨DescriptiveComplexity.FeedbackGuessBlockIx.set, DescriptiveComplexity.fSetRel._proof_1 ⟩

Instances For

Dependency graph

def DescriptiveComplexity.feedbackGuessBlock :

The single existential block of the Σ₁ definition of Feedback Vertex Set: the removed set (unary), a strict partial order certifying acyclicity (binary), and an injection of the removed set into the marked set (binary).

Equations

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

Instances For

Dependency graph

@[instance_reducible]

instance DescriptiveComplexity.instFintypeFeedbackGuessBlockIx :

Fintype FeedbackGuessBlockIx

Equations

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

Dependency graph

def DescriptiveComplexity.fInjRel :

feedbackGuessBlock.lang.Relations 2

The inj relation variable.

Equations

DescriptiveComplexity.fInjRel = ⟨DescriptiveComplexity.FeedbackGuessBlockIx.inj, DescriptiveComplexity.fInjRel._proof_1 ⟩

Instances For

Dependency graph

@[reducible, inline]

abbrev DescriptiveComplexity.fLtSym :

fvsSOLang.Relations 2

The lt symbol over the sum.

Equations

DescriptiveComplexity.fLtSym = Sum.inr DescriptiveComplexity.fLtRel

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.feedbackKernel :

fvsSOLang.Sentence

The first-order kernel of the Σ₁ definition of Feedback Vertex Set.

Equations

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

Instances For

Dependency graph

theorem DescriptiveComplexity.feedbackVertexSet_sigmaSODefinable :

SigmaSODefinable 1 FeedbackVertexSet

Feedback Vertex Set is Σ₁-definable: existentially guess the removed set, a strict partial order certifying that the rest is acyclic, and an injection of the removed set into the marked set, then check all five conditions first-order. Since NP is defined as Σ₁-definability, this is the membership half of the NP-completeness of Feedback Vertex Set.

Dependency graph

Feedback Arc Set #

def DescriptiveComplexity.fasInjRel :

feedbackArcGuessBlock.lang.Relations 4

The inj relation variable.

Equations

DescriptiveComplexity.fasInjRel = ⟨DescriptiveComplexity.FeedbackArcGuessBlockIx.inj, DescriptiveComplexity.fasInjRel._proof_1 ⟩

Instances For

Dependency graph

def DescriptiveComplexity.feedbackArcGuessBlock :

The single existential block of the Σ₁ definition of Feedback Arc Set: the removed set of arcs (binary), a strict partial order certifying acyclicity (binary), and an injection of the removed arcs into the marked relation (quaternary: it maps pairs to pairs).

Equations

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

Instances For

Dependency graph

@[reducible, inline]

abbrev DescriptiveComplexity.fasMarkedSym :

fasSOLang.Relations 2

The marked symbol over the sum.

Equations

DescriptiveComplexity.fasMarkedSym = Sum.inl FirstOrder.Language.magMarked

Instances For

Dependency graph

def DescriptiveComplexity.fasCutRel :

feedbackArcGuessBlock.lang.Relations 2

The cut relation variable.

Equations

DescriptiveComplexity.fasCutRel = ⟨DescriptiveComplexity.FeedbackArcGuessBlockIx.cut, DescriptiveComplexity.fasCutRel._proof_1 ⟩

Instances For

Dependency graph

@[instance_reducible]

instance DescriptiveComplexity.instFintypeFeedbackArcGuessBlockIx :

Fintype FeedbackArcGuessBlockIx

Equations

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

Dependency graph

@[reducible, inline]

abbrev DescriptiveComplexity.fasInjSym :

fasSOLang.Relations 4

The inj symbol over the sum.

Equations

DescriptiveComplexity.fasInjSym = Sum.inr DescriptiveComplexity.fasInjRel

Instances For

Dependency graph

@[reducible, inline]

abbrev DescriptiveComplexity.fasLtSym :

fasSOLang.Relations 2

The lt symbol over the sum.

Equations

DescriptiveComplexity.fasLtSym = Sum.inr DescriptiveComplexity.fasLtRel

Instances For

Dependency graph

@[instance_reducible]

instance DescriptiveComplexity.instDecidableEqFeedbackArcGuessBlockIx :

DecidableEq FeedbackArcGuessBlockIx

Equations

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

Dependency graph

@[reducible, inline]

abbrev DescriptiveComplexity.fasSOLang :

FirstOrder.Language

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

Equations

DescriptiveComplexity.fasSOLang = FirstOrder.Language.markedArcGraph.sum DescriptiveComplexity.feedbackArcGuessBlock.lang

Instances For

Dependency graph

@[reducible, inline]

abbrev DescriptiveComplexity.fasCutSym :

fasSOLang.Relations 2

The cut symbol over the sum.

Equations

DescriptiveComplexity.fasCutSym = Sum.inr DescriptiveComplexity.fasCutRel

Instances For

Dependency graph

@[reducible, inline]

abbrev DescriptiveComplexity.fasAdjSym :

fasSOLang.Relations 2

The adj symbol over the sum.

Equations

DescriptiveComplexity.fasAdjSym = Sum.inl FirstOrder.Language.magAdj

Instances For

Dependency graph

inductive DescriptiveComplexity.FeedbackArcGuessBlockIx :

The relation variables of the block.

cut : FeedbackArcGuessBlockIx
The removed set of arcs.
lt : FeedbackArcGuessBlockIx
The strict partial order certifying acyclicity.
inj : FeedbackArcGuessBlockIx
The injection of the removed arcs into the marked relation.

Instances For

Dependency graph

def DescriptiveComplexity.fasLtRel :

feedbackArcGuessBlock.lang.Relations 2

The lt relation variable.

Equations

DescriptiveComplexity.fasLtRel = ⟨DescriptiveComplexity.FeedbackArcGuessBlockIx.lt, DescriptiveComplexity.fasLtRel._proof_1 ⟩

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.feedbackArcKernel :

fasSOLang.Sentence

The first-order kernel of the Σ₁ definition of Feedback Arc Set.

Equations

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

Instances For

Dependency graph

theorem DescriptiveComplexity.feedbackArcSet_sigmaSODefinable :

SigmaSODefinable 1 FeedbackArcSet

Feedback Arc Set is Σ₁-definable: existentially guess the removed arcs, a strict partial order certifying that the rest is acyclic, and an injection of the removed arcs into the marked relation – a quaternary relation variable, the threshold being carried by pairs. Since NP is defined as Σ₁-definability, this is the membership half of the NP-completeness of Feedback Arc Set.

Dependency graph