reductions – How to convert Bipartite Perfect Matching to SAT?

Since 3-SAT is NP-complete you can take any algorithm that decides bipartite perfect matching and use the construction from Cook-Levin’s theorem. A direct construction is as follows.

Let $G=(U+V, E)$ be the bipartire graph with $|U| le |V|$ and no isolated vertices.
Create a boolean variable $x_e$ for each edge $e in E$. Intuitively, $x_e$ is set to true iff $e$ is selected in the matching.

Then, for all (unordered) pairs of distinct edges ${e, f}$ such that $e$ and $f$ share an endpoint, add the clause $(overline{x}_e vee overline{x}_f)$. These clauses ensure that the selected edges form a matching.

Finally, for each vertex $u in U$, create a new clause $bigveelimits_{ e=(u,v) in E} x_e$. Intuitively, this clause is satisfied iff $u$ is matched.

The SAT formula $varphi$ obtained as the conjunction of all the above clauses is satisfiable iff $G$ admits a perfect matching. To obtain a 3-SAT formula you can apply the standard transformation from SAT to 3-SAT.
Essentially, you can suitably duplicate and pad clauses with less than $3$ literals, while a generic clause $(ell_1 vee ell_2 vee dots, ell_k)$ with $k > 3$ literals can be replaced by the two clauses $(ell_1 vee ell_2 vee y) wedge (overline{y} vee ell_3 vee ell_4 vee dots vee ell_k)$, where $y$ is a new variable. Repeat the above transformation until all clauses have exactly 3 literals.