#Cycle Cover is one-call #P-complete

Valiant's theorem (Valiant 1979): the permanent of a 0-1 matrix, i.e., the number of cycle covers of a digraph or of perfect matchings of a bipartite graph, is #P-complete. The reduction here is from #1-in-SAT, and it is a one-call reduction: the number of exactly-one models is read off the one permanent asked for, by a remainder and a quotient (DescriptiveComplexity.sharpOneInSat_oneCall_sharpCycleCover).

The route, file by file:

• DescriptiveComplexity.Problems.CycleCover.Base: the base graph of the formula, and the evaluation of each term of the XOR sum;
• DescriptiveComplexity.Problems.CycleCover.Models: the consistent choices are the exactly-one models, so that the base graph with Valiant's gadgets attached has permanent 4 ^ t * N, t the number of occurrences and N the number of models;
• DescriptiveComplexity.Permanent.Widths: the 0-1 ladder expansion of that integer matrix has permanent congruent to it modulo 2 ^ L + 1, L the number of levels, with 4 ^ t * N ≤ 2 ^ L;
• DescriptiveComplexity.Problems.CycleCover.Formulas and DescriptiveComplexity.Problems.CycleCover.Drawing: the ladder expansion is first-order definable over the ordered expansion of the formula.

theorem DescriptiveComplexity.SatCover.bperm_attachedM {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Fintype A] : bperm attachedM = 4 ^ Nat.card (Occ A) * ↑(SharpOneInSAT.Count A)

The permanent of the attached matrix is 4 ^ t times the number of exactly-one models.

theorem DescriptiveComplexity.SatCover.sharpOneInSat_le {A : Type} [FirstOrder.Language.sat.Structure A] [Finite A] : SharpOneInSAT.Count A ≤ 2 ^ Nat.card (Occ A)

The number of exactly-one models is at most 2 ^ t.

theorem DescriptiveComplexity.SatCover.sharpCycleCover_drawInterp {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Fintype A] [Nonempty A] : SharpCycleCover.Count (drawInterp.MapRel A) = bperm (ladder 3 (widths attachedM))

The number of cycle covers of the drawing is the permanent of the ladder expansion of the attached matrix.

noncomputable def DescriptiveComplexity.sharpOneInSat_oneCall_sharpCycleCover : OneCallReduction SharpOneInSAT SharpCycleCover

#1-in-SAT reduces to #Cycle Cover with one call: the number of exactly-one models is the permanent of the drawn digraph, modulo 2 ^ L + 1 for L the number of levels, divided by 4 ^ t for t the number of occurrences.

Equations

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

theorem DescriptiveComplexity.sharpCycleCover_sharpP_oneCallHard : SharpP.OneCallHard SharpCycleCover

#Cycle Cover is one-call #P-hard.

theorem DescriptiveComplexity.sharpCycleCover_sharpP_oneCallComplete : SharpP.OneCallComplete SharpCycleCover

Valiant's theorem: #Cycle Cover, the permanent of a 0-1 matrix, is one-call #P-complete (Valiant 1979).