Max-SAT is the optimization version of SAT where the goal is to
satisfy the maximum number of clauses. It is considered one of the
fundamental combinatorial optimization problems and many important
problems can be naturally expressed as Max-SAT.

In this talk we introduce {\sc MiniMaxSat} a new Max-SAT solver that is
built on top of {\sc MiniSAT+}. It incorporates the best current SAT
and Max-SAT techniques. It can handle hard clauses (clauses of
mandatory satisfaction as in SAT), soft clauses (clauses whose
falsification is penalized by a cost) as well as pseudo-boolean
objective functions and constraints.  Its main features are: learning
and backjumping on hard clauses; resolution-based and
substraction-based lower bounding; and lazy propagation with the
two-watched literals scheme.  Our empirical evaluation comparing a
wide set of solving alternatives on a broad set of optimization
benchmarks indicates that the performance of {\sc MiniMaxSat} is
usually close to the best specialized alternative and, in some cases,
even better.

This is joint work with Javier Larrosa and Federico Heras.