# Three dimensional matching expressed as SAT

The posting in the website Embedding SATISFIABILITY into 3-DIMENSIONAL MATCHING seeks $$3SAT$$ as a $$3$$ dimensional matching instance.

I am looking to solve the converse problem. How to solve three dimensional matching using SAT solvers?

I know 3dm is NP complete and so can be solved by SAT. How do you embed 3DM as a SAT instance to be solved by solvers?

You can express 3DM as SAT in several ways.

First, let us recall that in 3-dimensional matching we are given a list of triples $$T \subseteq X \times Y \times Z$$, consisting of triples $$(x_1,y_1,z_1),\ldots,(x_n,y_n,z_n)$$, and a number $$k$$, and the question is whether there are $$k$$ triples $$(x_{i_1},y_{i_1},z_{i_1}),\ldots,(x_{i_k},y_{i_k},z_{i_k})$$ such that $$x_{i_r} \neq x_{i_s}$$, $$y_{i_r} \neq y_{i_s}$$, $$z_{i_r} \neq z_{i_s}$$ for $$r \neq s$$.

Unary encoding

For every $$1 \leq r \leq k$$ and $$1 \leq i \leq n$$ we have a variable $$t_{r,i}$$, whose meaning is "$$i_r = i$$".

For every $$1 \leq r \leq k$$, we have the constraint $$\bigvee_{i=1}^n t_{r,i},$$ stating that some triple must be the $$r$$'th triple.

For every $$r \neq s$$ and $$i,j$$ (possibly $$i=j$$) such that $$x_i = x_j$$, or $$y_i = y_j$$, or $$z_i = z_j$$, we have the constraint $$\lnot t_{r,i} \lor \lnot t_{s,j},$$ stating that you cannot choose both the $$i$$'th triple and the $$j$$'th triple (when $$i = j$$, that you cannot choose the same triple twice).

Binary encoding

Let $$\ell = \lceil \log_2 n \rceil$$. For every $$1 \leq r \leq k$$ we have an $$\ell$$-tuple of variables $$\vec{t}_r$$ which encodes the index of the $$r$$'th triple. The constraints are:

• For all $$r$$, clauses encoding "$$\vec{t}_r \leq n$$". This can be encoded using at most $$\ell$$ clauses (for each $$r$$).
• For all $$r \neq s$$ and $$i,j$$ as in unary encoding, a clause encoding "$$\vec{t}_r \neq i$$ or $$\vec{t}_s \neq j$$".

I'll let you work out how to express these as clauses.