\myheading{DFA accepting a binary substring divisible by prime number}
\label{DFA_prime}

\leveldown{}

\renewcommand{\CURPATH}{synth/DFA}

A problem: construct a regular expression accepting binary number divisible by 3.

"1111011" (123) is, "101010101011" (2731) is not.

Some discussion and the correct expressions:

\begin{itemize}
\item \url{https://stackoverflow.com/questions/7974655/regex-for-binary-multiple-of-3}
\item \url{https://stackoverflow.com/questions/844867/check-if-a-number-is-divisible-by-3}
\item \url{https://stackoverflow.com/questions/867279/regular-expression-to-define-some-binary-sequence}
\item \url{https://www.regextester.com/96234}
\end{itemize}

I couldn't generate \ac{RE}, but I can generate a minimal \ac{DFA}:

\lstinputlisting[style=custompy]{\CURPATH/2.py}

As you can see, it has testing procedure, which is, in turn, can be used instead of \ac{RE} matcher, if you really need to match
numbers divisible by 3.

States in double circles --- initial (\verb|S_0|) and accepting:

\begin{figure}[H]
\centering
\includegraphics[scale=0.7]{\CURPATH/DIVISOR_3_STATES_4.png}
\caption{DFA for numbers divisible by 3 (4 states) (minimal)}
\end{figure}

... is almost like the one someone posted \href{https://stackoverflow.com/questions/7974655/regex-for-binary-multiple-of-3}{here},
but my solution has two separate states as initial and accepting.

Some of solutions are hard to find manually.

\ac{DFA}s are bigger for prime numbers, of course, and smaller for even numbers.

\begin{figure}[H]
\centering
\includegraphics[scale=0.7]{\CURPATH/DIVISOR_2_STATES_2.png}
\caption{DFA for numbers divisible by 2 (2 states) (minimal)}
\end{figure}

\begin{figure}[H]
\centering
\includegraphics[scale=0.7]{\CURPATH/DIVISOR_4_STATES_3.png}
\caption{DFA for numbers divisible by 4 (3 states) (minimal)}
\end{figure}

\begin{figure}[H]
\centering
\includegraphics[scale=0.7]{\CURPATH/DIVISOR_5_STATES_6.png}
\caption{DFA for numbers divisible by 5 (6 states) (minimal)}
\end{figure}

\begin{figure}[H]
\centering
\includegraphics[scale=0.7]{\CURPATH/DIVISOR_6_STATES_4.png}
\caption{DFA for numbers divisible by 6 (4 states) (minimal)}
\end{figure}

\begin{figure}[H]
\centering
\includegraphics[scale=0.7]{\CURPATH/DIVISOR_7_STATES_8.png}
\caption{DFA for numbers divisible by 7 (8 states) (minimal)}
\end{figure}

\begin{figure}[H]
\centering
\includegraphics[scale=0.7]{\CURPATH/DIVISOR_8_STATES_4.png}
\caption{DFA for numbers divisible by 8 (4 states) (minimal)}
\end{figure}

\begin{figure}[H]
\centering
\includegraphics[scale=0.7]{\CURPATH/DIVISOR_9_STATES_10.png}
\caption{DFA for numbers divisible by 9 (10 states) (minimal)}
\end{figure}

\begin{figure}[H]
\centering
\includegraphics[scale=0.7]{\CURPATH/DIVISOR_10_STATES_6.png}
\caption{DFA for numbers divisible by 10 (6 states) (minimal)}
\end{figure}

These \ac{DFA}s above are guaranteed to be minimal.

The following \ac{DFA} may not be minimal.
I couldn't find it for 11 states after Z3 working for one hour, but I could find it for 12 states.
So it may be minimal, but may be not.

\begin{figure}[H]
\centering
\includegraphics[width=1.0\textwidth]{\CURPATH/DIVISOR_11_STATES_12.png}
\caption{DFA for numbers divisible by 11 (12 states) (may be not minimal)}
\end{figure}

But this is minimal:

\begin{figure}[H]
\centering
\includegraphics[scale=0.7]{\CURPATH/DIVISOR_12_STATES_5.png}
\caption{DFA for numbers divisible by 12 (5 states) (minimal)}
\end{figure}

May not be minimal again. Search failed for 11, 12, 13 states (one hour for each), but found for 14 states:

\begin{figure}[H]
\centering
\includegraphics[width=1.0\textwidth]{\CURPATH/DIVISOR_13_STATES_14.png}
\caption{DFA for numbers divisible by 13 (14 states) (may be not minimal)}
\end{figure}

\begin{figure}[H]
\centering
\includegraphics[scale=0.7]{\CURPATH/DIVISOR_14_STATES_8.png}
\caption{DFA for numbers divisible by 14 (8 states) (minimal)}
\end{figure}

May be not be minimal. Search failed for 10..15 states, but found for 16 states:

\begin{figure}[H]
\centering
\includegraphics[width=1.0\textwidth]{\CURPATH/DIVISOR_15_STATES_16.png}
\caption{DFA for numbers divisible by 15 (16 states) (may be not minimal)}
\end{figure}

\begin{figure}[H]
\centering
\includegraphics[scale=0.7]{\CURPATH/DIVISOR_16_STATES_5.png}
\caption{DFA for numbers divisible by 16 (5 states) (minimal)}
\end{figure}

\myheading{Further work}

Convert \ac{DFA}s to \ac{RE}...

\myheading{What about bruteforce?}

For 10 vertices, you have to enumerate $(10 \cdot 10) ^ {10} = 10^{20}$ \ac{DFA}s, or
$log_2{(10 \cdot 10) ^ {10}} \approx 66$ bits.

\myheading{The files}

\url{\RepoURL/\CURPATH}

\myheading{A problem from the ``Digital Logic RTL \& Verilog Interview Questions'' book}

\begin{figure}[H]
\centering
\includegraphics[width=0.8\textwidth]{\CURPATH/verilogcode.jpg}
\caption{A problem from the ``Digital Logic RTL \& Verilog Interview Questions'' book}
\end{figure}

I've found the problem \href{https://www.facebook.com/yuri.panchul/posts/10159286775398392}{here} (Russian Facebook post).
The book is available at amazon\footnote{\url{https://www.amazon.com/Digital-Logic-Verilog-Interview-Questions/dp/1512021466}}.
More information on \href{http://www.verilogcode.com/}{its website}.

\levelup{}