# 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.