\myheading{Yet another explanation of modulo inverse using SMT-solvers}

\MathForProg has a part about modulo arithmetics and modulo inverse.

By which constant we must multiply a random number, so that the result would be as if we divided them by 3?

\begin{lstlisting}
from z3 import *

m=BitVec('m', 32)

s=Solver()

# wouldn't work for 10, etc
divisor=3

# random constant, must be divisible by divisor:
const=(0x1234567*divisor)

s.add(const*m == const/divisor)

print s.check()
print "%x" % s.model()[m].as_long()
\end{lstlisting}

The magic number is:

\begin{lstlisting}
sat
aaaaaaab
\end{lstlisting}

Indeed, this is modulo inverse of 3 modulo $2^{32}$: \url{https://www.wolframalpha.com/input/?i=PowerMod%5B3,-1,2%5E32%5D}.

Let's check using \href{https://yurichev.com/news/20191212_progcalc/}{my calculator}:

\begin{lstlisting}
[3] 123456*0xaaaaaaab
[3] (unsigned) 353492988371136 0x141800000a0c0 0b1010000011000000000000000000000001010000011000000
[4] 123456/3
[4] (unsigned) 41152 0xa0c0 0b1010000011000000
\end{lstlisting}

The problem is simple enough to be solved using MK85:

\lstinputlisting[style=customsmt]{equations/modinv/modinv.smt}

\lstinputlisting{equations/modinv/modinv.correct}

However, it wouldn't work for 10, because there are no modulo inverse of 10 modulo $2^{32}$, SMT solver would give "unsat".