Solution (source code)

= Solution

The <Hall marriage theorem> says that a <bipartite graph> with classes $A,B$ has a <matching in a graph>[matching] saturating $A$ if and only if
$$
|N(S)|\geq|S|
\qquad\text{for every }S\subseteq A,
$$
where $N(S)$ is the <graph neighbourhood> of $S$. Necessity follows because the matching sends the vertices of $S$ to distinct vertices of $N(S)$.

For sufficiency, add vertices $x,y$, join $x$ to every vertex of $A$, and join every vertex of $B$ to $y$. Let $W$ be an $x$-$y$ vertex separator, and write $W_A=W\cap A$ and $W_B=W\cap B$. If an edge joined a vertex of $A\setminus W_A$ to a vertex of $B\setminus W_B$, it would give an $x$-$y$ path avoiding $W$. Hence
$$
N(A\setminus W_A)\subseteq W_B.
$$
Hall's condition gives
$$
|W_B|\geq|N(A\setminus W_A)|
\geq|A\setminus W_A|,
$$
and therefore $|W|\geq|A|$. By <Menger theorem>, there are $|A|$ internally vertex-disjoint $x$-$y$ paths. Each has the form $xaby$ with $a\in A$ and $b\in B$; disjointness makes all the $a$ and all the $b$ distinct. Their middle edges form a matching saturating $A$.