# [isabelle] New AFP entry: Maximum Cardinality Matching

*To*: Isabelle Users <isabelle-users at cl.cam.ac.uk>
*Subject*: [isabelle] New AFP entry: Maximum Cardinality Matching
*From*: Tobias Nipkow <nipkow at in.tum.de>
*Date*: Mon, 15 Aug 2011 11:19:57 +0200
*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6; rv:5.0) Gecko/20110624 Thunderbird/5.0

Maximum Cardinality Matching
Christine Rizkallah
A matching in a graph G is a subset M of the edges of G such that no two
share an endpoint. A matching has maximum cardinality if its cardinality
is at least as large as that of any other matching. An odd-set cover OSC
of a graph G is a labeling of the nodes of G with integers such that
every edge of G is either incident to a node labeled 1 or connects two
nodes labeled with the same number i ≥ 2. This article proves Edmonds
theorem: Let M be a matching in a graph G and let OSC be an odd-set
cover of G. For any i ≥ 0, let n(i) be the number of nodes labeled i. If
|M| = n(1) + ∑i ≥ 2(n(i) div 2), then M is a maximum cardinality matching.
http://afp.sourceforge.net/entries/Max-Card-Matching.shtml

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*