\myheading{MaxSAT}

MaxSAT problem is a problem where as many clauses should be satisfied, as possible, but maybe not all.

(Usual) clauses which \emph{must} be satisfied, called \emph{hard clauses}.
Clauses which \emph{should} be satisfied, called \emph{soft clauses}.

MaxSAT solver tries to satisfy all \emph{hard clauses} and as much \emph{soft clauses}, as possible.

*.wcnf files are used, the format is almost the same as in DIMACS files, like:

\begin{lstlisting}
p wcnf 207 796 208
208 1 0
208 2 0
208 3 0
208 4 0

...

1 -152 0
1 -153 0
1 -154 0
1 155 0
1 -156 0
1 -157 0
\end{lstlisting}

Each clause is written as in DIMACS file, but the first number if weight.
MaxSAT solver tries to maximize clauses with bigger weights first.

If the weight has \emph{top weight}, the clause is \emph{hard clause} and must always be satisfied.
\emph{Top weight} is set in header.
In our case, it's 208.

Some well-known MaxSAT solvers are Open-WBO\footnote{\url{http://sat.inesc-id.pt/open-wbo}}, etc.