1
$\begingroup$

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?

$\endgroup$
1
2
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.