\myheading{Generating de Bruijn sequences using SMT solver}
\label{DeBruijnZ3}

(\MathForProg has a part about de Bruijn sequences.)

\renewcommand{\CURPATH}{equations/de_bruijn_SMT}

The following piece of quite esoteric code calculates number of leading zero bits
\footnote{\url{https://en.wikipedia.org/wiki/Find_first_set}}:

\begin{lstlisting}
int v[64]=
	{ -1,31, 8,30, -1, 7,-1,-1, 29,-1,26, 6, -1,-1, 2,-1,
	  -1,28,-1,-1, -1,19,25,-1, 5,-1,17,-1, 23,14, 1,-1,
	   9,-1,-1,-1, 27,-1, 3,-1, -1,-1,20,-1, 18,24,15,10,
	  -1,-1, 4,-1, 21,-1,16,11, -1,22,-1,12, 13,-1, 0,-1 };

int LZCNT(uint32_t x)
{
    x |= x >> 1;
    x |= x >> 2;
    x |= x >> 4;
    x |= x >> 8;
    x |= x >> 16;
    x *= 0x4badf0d;
    return v[x >> 26];
}
\end{lstlisting}

(This is usually done using simpler algorithm, but it will contain conditional jumps, which is bad for
CPUs starting at RISC. There are no conditional jumps in this algorithm.)

The magic number used here is called \emph{de Bruijn sequence},
and I once used bruteforce to find it (one of the results was \emph{0x4badf0d}, which is used here).
But what if we need magic number for 64-bit values?
Bruteforce is not an option here.

If you already read about these sequences in my blog or in other sources,
you can see that the 32-bit magic number is a number consisting
of 5-bit overlapping chunks, and all chunks must be unique, i.e., must not be repeating.

For 64-bit magic number, these are 6-bit overlapping chunks.

To find the magic number, one can find a Hamiltonian path of a de Bruijn graph.
But I've found that Z3 is also can do this, though, overkill, but this is more illustrative.

\lstinputlisting[style=custompy,caption=Z3Py program]{\CURPATH/64.py}

We just enumerate all overlapping 6-bit chunks and tell Z3 that they must be unique (see \TT{Distinct}).

\lstinputlisting[caption=The output]{\CURPATH/output.txt}

Overlapping chunks are clearly visible.
So the magic number is \emph{0x79c52dd0991abf60}.
Let's check:

\lstinputlisting[style=customc]{\CURPATH/64.c}

That works!

The problem is easy enough to be tackled MK85, although, it's not as fast as Z3, of course:
\href{\RepoURL/\CURPATH/64_MK85.py}{src},
\href{\RepoURL/\CURPATH/64_MK85.txt}{output}.