# Directed HAM Cycles with Additional Constraints to SAT

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?

• What do you mean with "direction"?
– orlp
Dec 4, 2018 at 10:07
• 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$. Dec 4, 2018 at 17:36

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.