\myheading{TAOCP 7.1.1 exercises 4 and 5}

\renewcommand{\CURPATH}{synth/logic/TAOCP_711_4_and_5}

Found this exercise in \href{http://www.cs.utsa.edu/~wagner/knuth/fasc0b.pdf}{TAOCP section 7.1.1 (Boolean basics)}:

\begin{figure}[H]
\centering
\myfbox{\includegraphics[width=1\textwidth]{\CURPATH/page3.png}}
\caption{Page 3}
\end{figure}

\begin{figure}[H]
\centering
\myfbox{\includegraphics[width=1\textwidth]{\CURPATH/page34.png}}
\caption{Page 34}
\end{figure}

I'm not clever enough to solve this manually (yet),
but I could try using logic synthesis, as I did before.
As they say, ``machines should work; people should think''.

The modified Z3Py script:

\url{\RepoURL/\CURPATH/logic_for_TAOCP.py}

My solution for NAND:

\lstinputlisting[basicstyle=\ttfamily\small]{\CURPATH/nand.txt}

My solution for NAND with 0/1 constants:

\lstinputlisting[basicstyle=\ttfamily\small]{\CURPATH/nand_constants.txt}

My solution for ANDN:

\lstinputlisting[basicstyle=\ttfamily\small]{\CURPATH/andn.txt}

My solution for ANDN with 0/1 constants:

\lstinputlisting[basicstyle=\ttfamily\small]{\CURPATH/andn_constants.txt}

Correct answers from \ac{TAOCP}:

\begin{figure}[H]
\centering
\myfbox{\includegraphics[width=1\textwidth]{\CURPATH/page51.png}}
\caption{Page 51}
\end{figure}

My solutions are slightly different: I haven't "pass through" instruction, so sometimes a value is copied from the input to the output using NAND/ANDN.
Also, my versions are sometimes different, but correct and has the same length.

\myhrule{}

What about bruteforce?
Bruteforce for each ANDN and NAND instructions and 9 steps
requires enumerating of $3 \cdot 10^{11}$ possible solutions:

\begin{lstlisting}[caption=small,basicstyle=\ttfamily\small]
attempt, STEPS= 9
all possible code sequences,
if to find them using bruteforce: 3.0e+11
sat!
5 instructions for OUTPUTS TT (Knuth's representation)=0110
r0=input                 1100
r1=input                 1010
r2=input                 0000
r3=input                 1111
r4=ANDN r1, r0           0100
r5=ANDN r4, r3           1011
r6=ANDN r0, r1           0010
r7=ANDN r6, r5           1001
r8=ANDN r7, r3           0110
\end{lstlisting}

That's too much.