Documentation

CslibFrontier.Computability.Complexity.Problems.Graph.PerfectMatching

Perfect matchings as an exactly-one instance #

The perfect matchings of the graph G.induced of a vertex and edge list G : Graph are the models of a Holant instance (Cslib.Complexity.Graph.perfectMatchingInstance): one Boolean variable for each edge, and one exactly-one constraint for each vertex on its incident edges. The edges are listed by Cslib.Complexity.Graph.edgeList, which keeps the edges of G between distinct declared vertices and erases repetitions in either orientation, so that its positions are the edges of G.induced. The exactly-one partition function of the instance is the number of perfect matchings (Cslib.Complexity.Graph.partitionFunction_perfectMatchingInstance).

Every variable occurs in the constraints of the two ends of its edge (Cslib.Complexity.Graph.count_vars_perfectMatchingInstance), and the constraint of a vertex has at most as many variables as the vertex has neighbours (Cslib.Complexity.Graph.length_le_of_mem_perfectMatchingInstance).

Main definitions #

Main results #

source
def Cslib.Complexity.Graph.perfectMatchingInstance (G : Graph) :
Logic.PL.CSP Unit ℕ

The perfect-matching instance of G: a variable for each position of G.edgeList, and an exactly-one constraint for each distinct declared vertex on the positions of its incident edges.

Instances For

    The instance #

    source
    theorem Cslib.Complexity.Graph.mem_vars_perfectMatchingInstance {G : Graph} {x : ℕ} :
    x ∈ G.perfectMatchingInstance.vars ↔ x < G.edgeList.length

    The variables of the perfect-matching instance are the positions of the edge list.

    source
    theorem Cslib.Complexity.Graph.partitionFunction_perfectMatchingInstance (G : Graph) :
    Logic.PL.CSP.partitionFunction Logic.PL.CSP.exactlyOneWeight G.perfectMatchingInstance = Nat.card { M : G.induced.Subgraph // M.IsPerfectMatching }

    The exactly-one partition function of the perfect-matching instance is the number of perfect matchings of G.induced.

    Occurrences and arities #

    source
    theorem Cslib.Complexity.Graph.length_perfectMatchingInstance (G : Graph) :
    List.length G.perfectMatchingInstance = G.vertices.toFinset.card

    The constraints of the perfect-matching instance: one for each distinct declared vertex.

    source
    theorem Cslib.Complexity.Graph.count_vars_perfectMatchingInstance (G : Graph) (x : ℕ) :
    List.count x G.perfectMatchingInstance.vars ≤ 2

    Every variable occurs at most twice: in the constraints of the two ends of its edge.

    source
    theorem Cslib.Complexity.Graph.length_le_of_mem_perfectMatchingInstance {G : Graph} {d : ℕ} (hdeg : ∀ (v : { v : ℕ // v ∈ G.vertices }), Nat.card ↑(G.induced.neighborSet v) ≤ d) {c : Logic.PL.Constraint Unit ℕ} (hc : c ∈ G.perfectMatchingInstance) :
    c.2.length ≤ d

    A vertex constraint has at most as many variables as the vertex has neighbours.

    source
    theorem Cslib.Complexity.Graph.card_neighborSet_le {G : Graph} (v : { v : ℕ // v ∈ G.vertices }) :
    Nat.card ↑(G.induced.neighborSet v) ≤ (List.filter (fun (e : ℕ × ℕ) => incident e ↑v) G.edgeList).length

    A vertex has at most as many neighbours as edge-list entries at it, so a degree bound can be checked on the edge list.