\myheading{A poor man’s MaxSMT}

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]{\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.

\begin{lstlisting}[style=customc]
// poor man's MaxSMT
// if we minimize, first try false, then true
// if we maximize, do contrariwise
bool run_poor_mans_MaxSMT(struct ctx* ctx)
{
	if (verbose>0)
		printf ("%s() begin\n", __FUNCTION__);
	assert (ctx->maxsat==true);
	struct PicoSAT *p=picosat_init ();

	add_clauses_to_picosat(ctx, p);

	if (ctx->write_CNF_file)
	{
		write_CNF(ctx, "tmp.cnf");
		printf ("CNF file written to tmp.cnf\n");
	};

	int array[ctx->min_max_var->width];
	int res;
	// do this starting at the MSB moving towards the LSB:
	for (int idx=ctx->min_max_var->width-1; idx>=0; idx--)
	{
		// try the first false/true
		array[idx]=ctx->min_or_max==false ? 0 : 1;
		if (verbose>0)
			printf ("idx=%d trying %s\n", idx, ctx->min_or_max==false ? "false" : "true");
		picosat_assume (p, (ctx->min_or_max==false ? -1 : 1) * (ctx->min_max_var->SAT_var+idx));

		res=picosat_sat (p,-1);
		if (res==10)
		{
			if (verbose>0)
				printf ("got SAT\n");
			if (idx!=0)
			{
				// add a newly discovered correct bit as a clause
				// but do this only if this is not the last bit
				// if the bit is the last/lowest (idx==0), we want to prevent PicoSAT to be switched out of SAT state
				// (PicoSAT do this after picosat_add() call)
				// because we are fetching result sooner afterwards
				picosat_add (p, (ctx->min_or_max==false ? -1 : 1) * (ctx->min_max_var->SAT_var+idx));
				picosat_add (p, 0);
			}
			// proceed to the next bit:
			continue;
		};
		if (verbose>0)
			printf ("got UNSAT\n");
		assert (res==20); // must be in UNSAT state

		// try the second false/true
		array[idx]=ctx->min_or_max==false ? 1 : 0;
		if (verbose>0)
			printf ("idx=%d trying %s\n", idx, ctx->min_or_max==false ? "true" : "false");
		picosat_assume (p, (ctx->min_or_max==false ? 1 : -1) * (ctx->min_max_var->SAT_var+idx));

		res=picosat_sat (p,-1);
		if (res==10)
		{
			if (verbose>0)
				printf ("got SAT\n");
			if (idx!=0)
			{
				picosat_add (p, (ctx->min_or_max==false ? 1 : -1) * (ctx->min_max_var->SAT_var+idx));
				picosat_add (p, 0);
			};
		}
		else if (res==20)
		{
			if (verbose>0)
			{
				printf ("got UNSAT\n");
				printf ("%s() begin -> false\n", __FUNCTION__);
			};
			// UNSAT for both false and true for this bit at idx, return UNSAT for this instance:
			return false;
		}
		else
		{
			assert(0);
		};
	};
	// must have a solution at this point
	fill_variables_from_picosat(ctx, p);
	// construct a value from array[]:
	ctx->min_max_var->val=SAT_solution_to_value(array, ctx->min_max_var->width);
	if (verbose>0)
		printf ("%s() begin -> true, val=%llu\n", __FUNCTION__, ctx->min_max_var->val);
	return true;
};
\end{lstlisting}

( \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
\frame{\includegraphics[scale=0.6]{\CURPATH/MaxSMT/exercise.png}}
\caption{The exercise}
\end{figure}

% FIXME: unfull frame...
\begin{figure}[H]
\centering
\frame{\includegraphics[scale=0.6]{\CURPATH/MaxSMT/solution.png}}
\caption{The solution}
\end{figure}