#Cycle Cover: the permanent of a 0-1 matrix

A cycle cover of a digraph is a set of arcs leaving every vertex exactly once and entering every vertex exactly once: a permutation of the vertices along the arcs. The number of cycle covers is the permanent of the adjacency matrix (DescriptiveComplexity.sharpCycleCover_eq_bperm), and the number of perfect matchings of the bipartite graph whose two sides are two copies of the vertices, joined along the arcs. This is the problem Valiant 1979 proved #P-complete; its completeness is in DescriptiveComplexity.Problems.CycleCover.Completeness.

DescriptiveComplexity.SharpCycleCover is in #P (DescriptiveComplexity.sharpCycleCover_mem_sharpP): the cover is a guessed binary relation, checked first-order to be a bijection along the arcs.

def DescriptiveComplexity.IsCycleCover {A : Type} (R F : A → A → Prop) : Prop

F is a cycle cover of the relation R: a bijection of the universe along R.

Equations

• DescriptiveComplexity.IsCycleCover R F = ((∀ (x : A), ∃! y : A, F x y) ∧ (∀ (y : A), ∃! x : A, F x y) ∧ ∀ (x y : A), F x y → R x y)

noncomputable def DescriptiveComplexity.IsCycleCover.toFun {A : Type} {R F : A → A → Prop} (h : IsCycleCover R F) (x : A) : A

A cycle cover, as a permutation: x goes to the unique y with F x y.

Equations

• h.toFun x = Classical.choose ⋯

theorem DescriptiveComplexity.IsCycleCover.rel_toFun {A : Type} {R F : A → A → Prop} (h : IsCycleCover R F) (x : A) : F x (h.toFun x)

The kernel

inductive DescriptiveComplexity.CoverGuessBlockIx : Type

The relation variables of the block.

• nxt : CoverGuessBlockIx

  The guessed cover: nxt x y when the cover uses the arc from x to y.

@[reducible, inline]

abbrev DescriptiveComplexity.cvNxtSym : coverSOLang.Relations 2

The nxt symbol over the sum.

Equations

• DescriptiveComplexity.cvNxtSym = Sum.inr DescriptiveComplexity.cvNxtRel

@[reducible, inline]

abbrev DescriptiveComplexity.cvArcSym : coverSOLang.Relations 2

The arc symbol over the sum.

Equations

• DescriptiveComplexity.cvArcSym = Sum.inl FirstOrder.Language.dgArc

@[instance_reducible]

instance DescriptiveComplexity.instFintypeCoverGuessBlockIx : Fintype CoverGuessBlockIx

Equations

• DescriptiveComplexity.instFintypeCoverGuessBlockIx = { elems := [DescriptiveComplexity.CoverGuessBlockIx.nxt].toFinset, complete := DescriptiveComplexity.instFintypeCoverGuessBlockIx._proof_1 }

@[reducible, inline]

abbrev DescriptiveComplexity.coverSOLang : FirstOrder.Language

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

Equations

• DescriptiveComplexity.coverSOLang = FirstOrder.Language.digraph.sum DescriptiveComplexity.coverGuessBlock.lang

def DescriptiveComplexity.cvNxtRel : coverGuessBlock.lang.Relations 2

The nxt relation variable.

Equations

• DescriptiveComplexity.cvNxtRel = ⟨DescriptiveComplexity.CoverGuessBlockIx.nxt, DescriptiveComplexity.cvNxtRel._proof_1⟩

@[instance_reducible]

instance DescriptiveComplexity.instDecidableEqCoverGuessBlockIx : DecidableEq CoverGuessBlockIx

Equations

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

def DescriptiveComplexity.coverGuessBlock : SOBlock

The existential block of the Σ₁ definition: the cover, guessed as a binary relation.

Equations

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

def DescriptiveComplexity.nxtF {α : Type} (x y : α) : coverSOLang.Formula α

The guessed cover, as an atom.

Equations

• DescriptiveComplexity.nxtF x y = DescriptiveComplexity.cvNxtSym.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

noncomputable def DescriptiveComplexity.cycleCoverKernel : coverSOLang.Sentence

The first-order kernel: the guessed relation leaves and enters every element exactly once, along the arcs.

Equations

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

def DescriptiveComplexity.coverAssignEquiv (A : Type) : coverGuessBlock.Assignment A ≃ (A → A → Prop)

A binary relation, as an assignment of the block guessing the cover.

Equations

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

theorem DescriptiveComplexity.card_isCycleCover_eq_witnessCount (A : Type) [FirstOrder.Language.digraph.Structure A] : Nat.card { F : A → A → Prop // IsCycleCover (fun (x y : A) => DGArc x y) F } = witnessCount coverGuessBlock cycleCoverKernel A

The number of cycle covers is the number of witnesses of the kernel.

The problem

noncomputable def DescriptiveComplexity.SharpCycleCover : CountingProblem FirstOrder.Language.digraph

#Cycle Cover: the number of cycle covers of a digraph, i.e., the permanent of its adjacency matrix.

Equations

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

theorem DescriptiveComplexity.sharpCycleCover_eq_bperm (A : Type) [FirstOrder.Language.digraph.Structure A] [Fintype A] [DecidableEq A] [DecidableRel fun (x y : A) => DGArc x y] : SharpCycleCover.Count A = bperm fun (x y : A) => if DGArc x y then 1 else 0

#Cycle Cover is the permanent of the adjacency matrix.

theorem DescriptiveComplexity.sharpCycleCover_mem_sharpP : SharpP.Mem SharpCycleCover

#Cycle Cover is in #P.