\myheading{Minimal Unsatisfiable Subformula}
\label{MUS}

\leveldown{}

\renewcommand{\CURPATH}{other/MUS}
  
It's a bit frustrating to get a depressing 'UNSAT' message from a SAT solver, and nothing else.
What can you do for diagnostics?
What can you do to fix your SAT instance?
What can you do to unclog your (overconstrained) instance?

In some other place of this book,
I used UNSAT core generation in Z3 to get a list of conflicting cells in spreadsheet \ref{spreadsheet_unsat}.
Here I'll see what can be done for a SAT instance.

I'll use this problem from D.Knuth's TAOCP 7.1.1\footnote{\url{http://www.cs.utsa.edu/~wagner/knuth/fasc0b.pdf\#page=18\&zoom=200,-6,389}}:

\begin{figure}[H]
\centering
\frame{\includegraphics[width=0.8\textwidth]{\CURPATH/taocp1.png}}
\end{figure}

\begin{figure}[H]
\centering
\frame{\includegraphics[width=0.8\textwidth]{\CURPATH/taocp2.png}}
\end{figure}

I'm assigning 1..7 SAT variables to t,u,v,w,x,y,z variables and translating this to a CNF file
(lines prefixed with "c " are comments, of course):

\lstinputlisting[style=customsat]{\CURPATH/1.cnf}

The instance is UNSAT, of course. Now I'm running PicoMUS utility from Picosat SAT solver,
that extracts \ac{MUS}:

\begin{lstlisting}
c [picomus] WARNING: no output file given
c [picomus] WARNING: PicoSAT compiled without trace generation
c [picomus] WARNING: core extraction disabled
s UNSATISFIABLE
c [picomus] computed MUS of size 8 out of 16 (50%)
v 2
v 4
v 5
v 6
v 9
v 10
v 14
v 15
v 0
\end{lstlisting}

This is a list of clauses.
If all of them are removed from your instances, it will be transformed from UNSAT to SAT.
Let's see, what are these clauses?
 
\begin{lstlisting}
-2 -7 0 # 2     -u -z
2 7 0   # 4     u z
-6 7 0  # 5     -y z
1 -5 0  # 6     t -x
-1 -7 0 # 9     -t -z
-3 6 0  # 10    -v y
-2 3 0  # 15    -u v
\end{lstlisting}

These are indeed clauses with variables that are in the
vicious cycle\footnote{\url{https://en.wikipedia.org/wiki/Virtuous\_circle\_and\_vicious\_circle}}
according to D.Knuth.

Note that the \ac{MUS} is not the smallest possible (sub)set, but just a set that you can use for diagnostics.
\textit{Minimal} in \ac{MUS} means that is cannot be reduced in its form.
However, smallest \ac{MUS}es are still possible to exist, but PicoMUS isn't guaranteed to find a smallest \ac{MUS}.

Now there is another tool in Picosat: PicoMCS, that extracts \ac{MCS}.
What can it say?

\begin{lstlisting}
s UNSATISFIABLE
v 10 0
v 14 0
v 15 0
v 2 0
v 5 0
v 6 0
v 8 4 0
v 9 0
\end{lstlisting}

Each line in list is a list of clauses. If a list of clauses is removed from your instances, it transforms from UNSAT to SAT.
Indeed, 10th clause is an element of \textit{vicious cycle}.
And so is 15th, etc.
But 14th clause is not. But removing it from the instance will solve the problem.
Also, if 8th and 4th clauses are both to be removed from the instance, it will be SAT, but not one-by-one.

Why not always using PicoMCS instead of PicoMUS? It's way slower.
And in practice, you can be satisfied with larger \ac{MUS}.

Now what if we can represent each clause as weighted and use MaxSAT solver?
(The same Open-WBO, I use so often.)

I prepend each clause with '1', that is a (smallest) weight of each clause:

\begin{lstlisting}
p wcnf 7 16 1000
1 -1 -4 0
1 -2 -7 0
1 2 -6 0
1 2 7 0
1 -6 7 0
1 1 -5 0
1 7 0
1 -5 7 0
1 -1 -7 0
1 -3 6 0
1 3 -4 0
1 3 -6 0
1 -4 -6 0
1 2 5 0
1 -2 3 0
1 -3 -5 0
\end{lstlisting}

... and asking Open-WBO MaxSAT solver to find such an assignment, that can satisfy as many clauses, as possible:

\begin{lstlisting}
s OPTIMUM FOUND
v -1 2 3 -4 -5 6 7
\end{lstlisting}

Let's see, which clauses gets satisfied with this assignment?
I manually added comments to the \ac{WCNF} instance:

\begin{lstlisting}
p wcnf 7 16 1000
1 -1 -4 0       # -t -w         OK
1 -2 -7 0       # -u -z         UNSAT
1 2 -6 0        # u y           OK
1 2 7 0         # u z           OK
1 -6 7 0        # -y z          OK
1 1 -5 0        # t -x          OK
1 1 7 0         # t z           OK
1 -5 7 0        # -x z          OK
1 -1 -7 0       # -t -z         OK
1 -3 6 0        # -v y          OK
1 3 -4 0        # v -w          OK
1 3 -6 0        # v -y          OK
1 -4 -6 0       # -w -y         OK
1 2 5 0         # y x           OK
1 -2 3 0        # -u v          OK
1 -3 -5 0       # -v -x         OK
\end{lstlisting}

The only 2nd clause is to be removed to break the \textit{vicious cycle}.

Again, MaxSAT solvers are way slower than \ac{MUS} extractors.
So they cannot be always used in practice.

\myheading{MUSer2}

This is a tool\footnote{\url{https://github.com/meelgroup/muser}}
acting as a front-end \ac{MUS} extractor on top of a SAT-solver like MiniSat, PicoSat, Glucose, UBCSAT, etc.
Unlike PicoMUS, it produces a \ac{CNF} file for our example, but it contains 8 clauses as well:

\lstinputlisting[style=customsat]{\CURPATH/muser2-output.cnf}

\levelup{}