Counting feedback vertex and arc sets

Lax280166.CountingFeedbackSets · concepts/Lax280166/CountingFeedbackSets.lean · lax-280166

definition

Loading review…

Natural Language Statement

Definition

On a finite directed graph with $k$ marked vertices, #Feedback Vertex Set counts the sets of exactly $k$ vertices whose removal leaves no directed cycle. On a finite directed graph with a marked relation of $k$ pairs, #Feedback Arc Set counts the sets of exactly $k$ arcs whose removal leaves no directed cycle.

Concept map

10 concepts; 25 descendants hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Lean source view on GitHub

Show types on hover

1	import Mathlib.Tactic.FinCases
2	import Mathlib.Order.PiLex
3	import Mathlib.Data.Prod.Lex
4	import Mathlib.Data.Fintype.EquivFin
5	import Mathlib.ModelTheory.Order
6	import Mathlib.ModelTheory.Semantics
7	import Mathlib.ModelTheory.Complexity
8	import Mathlib.Logic.Equiv.Fin.Basic
9	import Mathlib.Data.Fintype.Lattice
10	import Mathlib.Data.Finite.Sigma
11	import Mathlib.Order.Lattice.Nat
12	import Mathlib.Data.Set.Card
13	import Mathlib.Data.Fintype.Pigeonhole
14	import Mathlib.Dynamics.FixedPoints.Basic
15	import Mathlib.ModelTheory.Syntax
16	import Mathlib.Algebra.Order.BigOperators.Group.Finset
17	import Mathlib.Data.Fintype.Card
18	import Mathlib.SetTheory.Cardinal.Finite
19	import Mathlib.Data.Fintype.Sort
20	import Mathlib.Order.Hom.Set
21	import Mathlib.Logic.Equiv.Prod
22	import Mathlib.Data.Set.Finite.Lemmas
23	import Lax799700.CliqueFamily
24	import Lax799700.Feedback
25	import Mathlib.SetTheory.Cardinal.Finite
26	import Lax366625.CountingProblems
27
28	/-!
29	---
30	title: Counting feedback vertex and arc sets
31	type: definition
32	---
33	On a finite directed graph with $k$ marked vertices, #Feedback Vertex Set
34	counts the sets of exactly $k$ vertices whose removal leaves no directed
35	cycle. On a finite directed graph with a marked relation of $k$ pairs,
36	#Feedback Arc Set counts the sets of exactly $k$ arcs whose removal leaves no
37	directed cycle.
38	-/
39
40	namespace Lax280166.CountingFeedbackSets
41
42	open Lax799700.CliqueFamily Lax799700.Feedback
43
44	open FirstOrder
45
46	open Language Structure
47
48	section Generic
49
50	variable {A B : Type}
51
52	/-- The removal of the set `C` leaves an acyclic digraph, and `C` has exactly
53	as many elements as the `Kp`-marked set. -/
54	def FeedbackOfSizeOn (Adjp : A → A → Prop) (Kp : A → Prop) (C : A → Prop) : Prop :=
55	AcyclicRel (SurvivingArc Adjp C) ∧ {x \| C x}.ncard = {x \| Kp x}.ncard
56
57	end Generic
58
59	section Problem
60
61	variable (A : Type) [markedGraph.Structure A]
62
63	/-- The set `C` is a feedback vertex set with exactly as many vertices as the
64	marked set, in a finite marked digraph. -/
65	def FvsOfSize (C : A → Prop) : Prop :=
66	Finite A ∧ FeedbackOfSizeOn (fun x y : A => MGAdj x y) (fun x => MGMarked x) C
67
68	end Problem
69
70	open FirstOrder
71
72	open Language Structure
73
74	section Generic
75
76	variable {A B : Type}
77
78	/-- The relation `F` is a set of arcs whose removal leaves an acyclic digraph,
79	with exactly as many pairs as the marked relation. -/
80	def FasOfSizeOn (Adjp Kp : A → A → Prop) (F : A → A → Prop) : Prop :=
81	(∀ a b, F a b → Adjp a b) ∧ AcyclicRel (UncutArc Adjp F) ∧
82	{p : A × A \| F p.1 p.2}.ncard = {p : A × A \| Kp p.1 p.2}.ncard
83
84	end Generic
85
86	section Problem
87
88	variable (A : Type) [markedArcGraph.Structure A]
89
90	/-- The relation `F` is a feedback arc set with exactly as many arcs as the
91	marked relation has pairs, in a finite arc-marked digraph. -/
92	def FasOfSize (F : A → A → Prop) : Prop :=
93	Finite A ∧ FasOfSizeOn (fun a b : A => MAGAdj a b) (fun a b => MAGMarked a b) F
94
95	end Problem
96
97	open Lax366625.CountingProblems
98
99	/-- #Feedback Vertex Set, as a counting problem. -/
100	noncomputable def SharpFeedbackVertexSet : CountingProblem Lax799700.CliqueFamily.markedGraph :=
101	CountingProblem.ofFun fun A _ =>
102	Nat.card {C : A → Prop // FvsOfSize A C}
103
104	/-- #Feedback Arc Set, as a counting problem. -/
105	noncomputable def SharpFeedbackArcSet : CountingProblem Lax799700.Feedback.markedArcGraph :=
106	CountingProblem.ofFun fun A _ =>
107	Nat.card {F : A → A → Prop // FasOfSize A F}
108
109	end Lax280166.CountingFeedbackSets
110

Builds on

Used by

From Mathlib

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

Loading discussion…

Lax Lean Archive

Counting feedback vertex and arc sets

Flags

Flag this concept

Natural Language Statement

Definition

Lean source view on GitHub

Discussion

Settings

Your comments