\myheading{A poor man’s MaxSMT}

\renewcommand{\CURPATH}{solvers/MK85}

First, what is incremental SAT?
When a SAT-solver is \textit{warmed up}, and you want only to alter list of clauses slightly by adding
one, why to reset it?
In my toy SMT solver, I use incremental SAT for model counting, or getting all models:
see the
\href{\MKURL}{picosat\_get\_all\_models()}
function.

Also, many SAT solvers supports \textit{assumptions}.
That is you supply a list of clauses + \textit{temporary} clauses that will be dropped each time.

Now a digression: this is my own binary search implementation:

\lstinputlisting[style=customc,basicstyle=\ttfamily\tiny]{\CURPATH/MaxSMT/binsearch.c}

You wouldn't use it, but I wrote it because it's fits so nicely on SAT.

To solve an optimization problem, you want to find some \textit{optimum} variable, that is minimized
or maximized.
Like in my implementation of binary search, I can try bit by bit, but these are added as assumptions.

\lstinputlisting[style=customc,basicstyle=\ttfamily\tiny]{\CURPATH/MaxSMT/1.c}
( \url{\MKURL} )

For the popsicle problem (\ref{popsicles}):

\begin{lstlisting}
idx=15 trying true
got UNSAT
idx=15 trying false
got SAT
idx=14 trying true
got UNSAT
idx=14 trying false
got SAT
idx=13 trying true
got UNSAT
idx=13 trying false
got SAT
idx=12 trying true
got UNSAT
idx=12 trying false
got SAT
idx=11 trying true
got UNSAT
idx=11 trying false
got SAT
idx=10 trying true
got UNSAT
idx=10 trying false
got SAT
idx=9 trying true
got UNSAT
idx=9 trying false
got SAT
idx=8 trying true
got UNSAT
idx=8 trying false
got SAT
idx=7 trying true
got UNSAT
idx=7 trying false
got SAT
idx=6 trying true
got UNSAT
idx=6 trying false
got SAT
idx=5 trying true
got UNSAT
idx=5 trying false
got SAT
idx=4 trying true
got UNSAT
idx=4 trying false
got SAT
idx=3 trying true
got SAT
idx=2 trying true
got SAT
idx=1 trying true
got UNSAT
idx=1 trying false
got SAT
idx=0 trying true
got SAT
...
run_poor_mans_MaxSMT() begin -> true, val=13
\end{lstlisting}

It works slower than if using Open-WBO, but sometimes even faster than Z3!

This is as well: \ref{beer_can}.

And this is close to LEXSAT, see exercise and solution from the \ac{TAOCP}, section 7.2.2.2:

\begin{figure}[H]
\centering
\myfbox{\includegraphics[width=1\textwidth]{\CURPATH/MaxSMT/exercise.png}}
\caption{The exercise}
\end{figure}

\begin{figure}[H]
\centering
\myfbox{\includegraphics[width=1\textwidth]{\CURPATH/MaxSMT/solution.png}}
\caption{The solution}
\end{figure}