Solution (source code)

= Solution

For distinct $x,x'\in X$ and distinct $y,y'\in Y$, take all clauses
$$
\neg(p_{x,y}\wedge p_{x,y'}),
\qquad
\neg(p_{x,y}\wedge p_{x',y}).
$$
The first family says that each $x$ is paired with at most one $y$; the second says that each $y$ is paired with at most one $x$. There is no existence clause, so the domain may be any subset of $X$. Thus the relations $f_v$ are exactly the injective partial <functions> from $X$ to $Y$.