Three dimensional matching expressed as SAT

Question

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?

Answer 1

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.