2
$\begingroup$

The $n$ dimensional hypercube $Q_n$ is a graph that has a vertex $v_s$ for each string $s \in \{0, 1\}^n$ and an edge between two vertices $v_s$ and $v_t$ if and only if the Hamming distance between $s$ and $t$ is $1$.

I would like to find directed hamiltonian cycles in this graph that satisfy a certain property, and was thinking of feeding my problem to a SAT solver. The problem can be encoded as follows. We define a variable $x_{si}$ to denote that the vertex $v_s$ appears in the $i$-th position of the cycle. Then, for each $s \in \{0,1\}^n$, we define the contraints $\bigvee_{i} x_{si}$ (each vertex appears in one position of the cycle) and $\neg x_{si} \vee \neg x_{sj}$ for all $i \neq j$ (each vertex appears at most once in the cycle). Finally, we also require the constraints $\neg x_{si} \vee \neg x_{t(i+1)}$ for all pairs of strings $s$ and $t$ that have Hamming distance greater than $1$ (i.e pairs of vertices that do not have an edge cannot appear consecutively in the cycle ordering).

Now, I would like to add the following requirement on my cycle. For some specified integer parameter $k$, we must be able to partition the vertices of the graph into vertex disjoint copies of $Q_k$ such that the vertices in a specific copy of $Q_k$ are all assigned the same "direction". How can I capture this set of requirements easily in my reduction?

$\endgroup$
  • $\begingroup$ What do you mean with "direction"? $\endgroup$ – orlp Dec 4 '18 at 10:07
  • $\begingroup$ The vertices in copies of $Q_k$ will agree on $n-k$ coordinates. So say that in the cycle, if the successor of one of those vertices is obtained by flipping the $i$-th coordinate, then the same must be true for all of the vertices in that copy of $Q_k$. $\endgroup$ – user340082710 Dec 4 '18 at 17:36
3
+25
$\begingroup$

Encodings like this are notoriously slippery, so (of course) please carefully verify any outputs in case I've made a mistake somewhere.

Please assume that all unbound variables are universally quantified; i.e., I write $\bigvee_i\ p_{si}$ instead of $\forall s\ \bigvee_i\ p_{si}$.

Defining the partitions

First, define partition variables:

$p_{si} = \text{vertex $s$ is in partition $i$}$.

Basic partition constraints

Partitions are disjoint:

for $s \neq t$: $\lnot (p_{si} \land p_{ti})$.

Every string is part of one partition:

$\bigvee_i\ p_{si}$.

Coordinate matching within partitions

This is a little tricky. First, we need to define which hypercube each partition corresponds to. We specify this by defining which coordinates each partition matches on:

$m_{ij} = \text{partition $i$ requires coordinate $j$ to match}$.

Now we need to say that partition $i$ requires exactly $n-r$ coordinates to match (I'm going to use $r$ where OP uses $k$, because I need to use k as an index below):

$\sum_j m_{ij} = n - r$.

Computing the sum

Sums, of course, are not directly supported in the SAT model. We can handle this by computing the sum with propositional logic:

$a_{ijk} = \text{for partition $i$, the sum over the first $j$ bits of $m$ is $k$}$.

The sum across the first $j$ bits for partition $i$ must be uniquely defined:

for $k_1 \neq k_2$, $\lnot (a_{ijk_1} \land a_{ijk_2})$.

We could require each sum to be defined at least once, but we don't need to; we take care of that for free when we define how addition works:

$a_{i1k} \iff m_{i1}$

$a_{ijk} \land m_{ij} \implies a_{i(j+1)(k+1)}$

$a_{ijk} \land \lnot m_{ij} \implies a_{i(j+1)k}$

Now we can set what the sum needs to be:

$a_{in(n-r)} = \texttt{true}$

(Again, I use $r$ where OP uses $k$ to avoid confusion with $k$ as an index.)

Constraining matches

Strings in the same partition match at the required coordinates:

$(m_{ij} \land p_{si} \land p_{ti}) \implies \text{strings $s$ and $t$ match at position $j$}$.

The RHS of that implication is just a set of constants that we can precompute as true or false.

Enforcing cycle direction within partitions

To encode direction, we can precompute constants for a neighbor relation between strings:

$d_{sti} = \text{$s$ and $t$ are identical, except at position $i$, where $s$ is 0 and $t$ is 1}$.

We'll also define a variable to encode which strings follow which strings:

$f_{st} = \text{$t$ immediately follows $s$ in the cycle}$.

$f_{st} \iff \bigvee_i x_{si} \land x_{t(i+1)}$.

Now we're ready to encode cycle direction:

$[\bigvee_i (p_{si} \land p_{ti})] \implies [\bigvee_{uvj}\ (f_{su} \land f_{tv} \land [(d_{suj} \land d_{tvj}) \lor (d_{usj} \land d_{vtj})]$.

If $s$ and $t$ are in the same partition, then there is one specific bit position $j$ where the strings $u$ and $v$ that follow $s$ and $t$ in the cycle differ (and specifically differ in the same direction: 0 to 1 or 1 to 0).

I don't know that much about SAT solvers, but it may be that the last line produces an unwieldy number of terms. It may be possible to define further 'intermediate' variables like $f_{st}$ that break things up more and reduce the combinatorial explosion.

$\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.