Polynomial-time edge lists and perfect-matching instances

The edge list of a graph (Cslib.Complexity.Graph.edgeList) and its perfect-matching instance (Cslib.Complexity.Graph.perfectMatchingInstance) are computable in polynomial time from the encoded graph Cslib.Complexity.encGraph. The instance's variables are written in binary.

Main results

• Cslib.Complexity.Graph.computableInPolyTime_edgeList: the edge list.
• Cslib.Complexity.Graph.computableInPolyTime_perfectMatchingInstance: the perfect-matching instance.

theorem Cslib.Complexity.Graph.computableInPolyTime_edgeList : Turing.MultiTapeTM.ComputableInPolyTime edgeList encGraph (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat))

Listing the edges of G.induced is polynomial-time.

theorem Cslib.Complexity.Graph.computableInPolyTime_perfectMatchingInstance : Turing.MultiTapeTM.ComputableInPolyTime perfectMatchingInstance encGraph (encCSP Turing.MultiTapeTM.encUnit Turing.MultiTapeTM.encNat)

Building the perfect-matching instance of a graph is polynomial-time.