Directed HAM Cycles with Additional Constraints to SAT
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.