\myheading{Finding optimal beer can size using SMT solver}
\label{beer_can}

\leveldown{}

This is classic calculus problem: given a volume of a can, find such a height and radius of a can, so that you'll
spent least material to make it (tin, or whatever you use).

Since my toy SMT-solver MK85 supports only integers (in bitvectors) instead of reals, I can try to solve this problem
on integers.
What to do with $\pi$?
Let's round it to 3.

\begin{lstlisting}[style=customsmt]
(declare-fun AlmostPi () (_ BitVec 16))
(assert (= AlmostPi (_ bv3 16)))

; unknowns
(declare-fun Radius () (_ BitVec 16))
(declare-fun Height () (_ BitVec 16))

; There are may not be solutions for Volume=10000, since this we work on integers
; So let's ask for solution for Volume somewhere in between 10000 and 10500...
(declare-fun Volume () (_ BitVec 16))
(assert (bvuge Volume (_ bv10000 16)))
(assert (bvule Volume (_ bv10500 16)))

; r*r
(declare-fun Radius2 () (_ BitVec 16))
(assert (= Radius2 (bvmul_no_overflow Radius Radius)))

; pi*r*r
(declare-fun AreaOfBase () (_ BitVec 16))
(assert (= AreaOfBase (bvmul_no_overflow Radius2 AlmostPi)))

; 2*pi*r
(declare-fun Circumference () (_ BitVec 16))
(assert (= Circumference (bvmul_no_overflow (bvmul_no_overflow Radius AlmostPi) (_ bv2 16))))

; Volume = Height * AreaOfBase
(assert (= Volume (bvmul_no_overflow Height AreaOfBase)))

; surface of cylinder = Circumference * Height + 2*AreaOfBase
(declare-fun SurfaceOfCylinder () (_ BitVec 16))
(assert (= SurfaceOfCylinder (bvadd (bvmul_no_overflow Circumference Height) (bvmul_no_overflow AreaOfBase (_ bv2 16)))))

(minimize SurfaceOfCylinder)

(check-sat)
(get-model)
\end{lstlisting}

The solution:

\begin{lstlisting}
sat
(model
        (define-fun AlmostPi () (_ BitVec 16) (_ bv3 16)) ; 0x3
        (define-fun AreaOfBase () (_ BitVec 16) (_ bv507 16)) ; 0x1fb
        (define-fun Circumference () (_ BitVec 16) (_ bv78 16)) ; 0x4e
        (define-fun Height () (_ BitVec 16) (_ bv20 16)) ; 0x14
        (define-fun Radius () (_ BitVec 16) (_ bv13 16)) ; 0xd
        (define-fun Radius2 () (_ BitVec 16) (_ bv169 16)) ; 0xa9
        (define-fun SurfaceOfCylinder () (_ BitVec 16) (_ bv2574 16)) ; 0xa0e
        (define-fun Volume () (_ BitVec 16) (_ bv10140 16)) ; 0x279c
)
\end{lstlisting}

For Volume=10140, Radius=13, Height=20.
Hard to believe, but this is almost correct.
I can check it with Wolfram Mathematica:

\begin{lstlisting}
In[]:= FindMinimum[{2*Pi*r*h + Pi*r*r*2, h*Pi*r*r == 10000 }, {r, h}]
Out[]= {2569.5, {r -> 11.6754, h -> 23.3509}}
\end{lstlisting}

Error is ~3.

Using my toy solver and $\pi$ fixed to 3, perhaps, my results cannot be used in practice, however, we can deduce a general rule:
height must be the same as diameter, so that you'll spent minimum tin (or other material) to make it.

Probably, the can will not be suitable for stacking, packing, transporting, or holding in hand, but this is the most economical way to produce them.

\myheading{A jar}

What about a jar (a can without top (or bottom))?

\begin{lstlisting}[style=customsmt]
...
; surface of jar = Circumference * Height + AreaOfBase
(declare-fun SurfaceOfJar () (_ BitVec 16))
(assert (= SurfaceOfJar (bvadd (bvmul_no_overflow Circumference Height) AreaOfBase)))

(minimize SurfaceOfJar)
...
\end{lstlisting}

\begin{lstlisting}
sat
(model
        (define-fun AlmostPi () (_ BitVec 16) (_ bv3 16)) ; 0x3
        (define-fun AreaOfBase () (_ BitVec 16) (_ bv675 16)) ; 0x2a3
        (define-fun Circumference () (_ BitVec 16) (_ bv90 16)) ; 0x5a
        (define-fun Height () (_ BitVec 16) (_ bv15 16)) ; 0xf
        (define-fun Radius () (_ BitVec 16) (_ bv15 16)) ; 0xf
        (define-fun Radius2 () (_ BitVec 16) (_ bv225 16)) ; 0xe1
        (define-fun SurfaceOfJar () (_ BitVec 16) (_ bv2025 16)) ; 0x7e9
        (define-fun Volume () (_ BitVec 16) (_ bv10125 16)) ; 0x278d
)
\end{lstlisting}

For Volume=10125, Radius=15 and Height=15.
We can see that for jar, the height must be equal to the radius. Let's recheck in Mathematica:

\begin{lstlisting}
In[]:= FindMinimum[{2*Pi*r*h + Pi*r*r, h*Pi*r*r == 10000 }, {r, h}]
Out[]= {2039.41, {r -> 14.7101, h -> 14.7101}}
\end{lstlisting}

Correct!

Yes, you've been probably taught in school to solve this using paper and pencil, but...
The fun thing is that I never knew calculus at all, but I could write my toy bit-blaster, which can give such answers.
And thanks to Open-WBO, which is used in my MK85 as external MaxSAT solver.

Since I'm using non-standard SMT-LIB function \verb|bvmul_no_overflow|, this will not work on other SMT solvers.
For Z3, \verb|bvumul_noovfl| is to be used: \url{https://github.com/Z3Prover/z3/issues/574}

See also: \url{https://demonstrations.wolfram.com/MinimizingTheSurfaceAreaOfACylinderWithAFixedVolume/}

\levelup{}