\myheading{Stable marriage problem}

\renewcommand{\CURPATH}{other/stable_marriage}

See also in
\href{https://en.wikipedia.org/wiki/Stable_marriage_problem}{Wikipedia} and 
\href{https://rosettacode.org/wiki/Stable_marriage_problem}{Rosetta code}.

Layman's explanation in Russian: \url{https://lenta.ru/articles/2012/10/15/nobel/}.

One interesting use of it:

\begin{framed}
\begin{quotation}
The Internet infrastructure company Akamai, cofounded by Tom Leighton, also uses a variation of the Mating Ritual to assign web traffic to its servers.

In the early days, Akamai used other combinatorial optimization algorithms that got to be too slow as the number of servers (over 65,000 in 2010) and requests (over 800 billion per day) increased. Akamai switched to a Ritual-like approach, since a Ritual is fast and can be run in a distributed manner. In this case, web requests correspond to women and web servers correspond to men. The web requests have preferences based on latency and packet loss, and the web servers have preferences based on cost of bandwidth and co-location.
\end{quotation}
\end{framed}
( Eric Lehman, F Thomson Leighton, Albert R Meyer - Mathematics for Computer Science ) 

My solution is much less efficient, because much simpler/better algorithm exists (Gale/Shapley algorithm),
but I did it to demonstrate the essence of the problem plus as a yet another SMT-solvers and Z3 demonstration.

See comments:

\lstinputlisting[style=custompy]{\CURPATH/stable.py}

( The source code: \url{\RepoURL/\CURPATH/stable.py} )

Result is seems to be correct:

\begin{lstlisting}
sat

ManChoice:
abe <-> ivy
bob <-> cath
col <-> dee
dan <-> fay
ed <-> jan
fred <-> bea
gav <-> gay
hal <-> eve
ian <-> hope
jon <-> abi

WomanChoice:
abi <-> jon
bea <-> fred
cath <-> bob
dee <-> col
eve <-> hal
fay <-> dan
gay <-> gav
hope <-> ian
ivy <-> abe
jan <-> ed
\end{lstlisting}

This is what we did in plain English language.
``Connect men and women somehow, we don't care how.
But no pair must exist of those who prefer each other (simultaneously) over their current spouses''.
Gale/Shapley algorithm uses ``steps'' to ``stabilize'' marriage.
There are no ``steps'', all pairs are married couples already.

Another important thing to notice: only one solution must exist.

\begin{lstlisting}[style=custompy]
...

results=[]

# enumerate all possible solutions:
while True:
    if s.check() == sat:
        m = s.model()
        #print m
        results.append(m)
        block = []
        for d in m:
            c=d()
            block.append(c != m[d])
        s.add(Or(block))
    else:
        print "results total=", len(results)
        break

...
\end{lstlisting}

( The source code: \url{\RepoURL/\CURPATH/stable2.py} )

That reports only 1 model available, which is correct indeed.

Wojciech Niedbala fixed chained If's, but I left the old version, so readers can see a difference...

\begin{lstlisting}[style=custompy]
...

def _if_x(x, ind, i):
    if i == len(x) - 1:
        return If(x[i] == ind, i, -1)
    return If(x[i] == ind, i, _if_x(x, ind, i+1))


def _if_xy(x, y, i):
    if i == len(y) - 1:
        return If(x == y[i], i, -1)
    return If(x == y[i], i, _if_xy(x, y, i+1))

...

    s.add(WomanChoice[i]== _if_x(ManChoice, i, 0))

...

    s.add (ManChoiceInOwnRating[m]== _if_xy(ManChoice[m], ManPrefer[m], 0))
\end{lstlisting}

( The source code: \url{\RepoURL/\CURPATH/stable_fixed.py} )