*Bounty: 50*

*Bounty: 50*

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?