A. Abramé and D. Habet, }} (we name the tertiary clause c) detected by the first implication graph represented on the left in Fig.8 after the respective propagation of literals l 1 , l 2 , l 3 and l 4 . In the second graph on the left in the same figure, we represent another possible propagation sequence which outlines the possible neighborhood of l 4 , neigh(l 4 ) = {l 1 , l 3 } not containing the empty clause. Clearly, the subset ? = ? \ {{l}} is a 5-UCS recognized by the FUIP l such that c participates in the conflict and |succ(l)| = |c| = 3. The max-resolution transformation of ? with respect to RPO which corresponds to the variable sequence S = var(l 4 ), var(l 3 ), var(l 2 ), var(l 1 ) is represented on the right in Fig.8. Clearly, the References 1, Principles and Practice of Constraint Programming, vol.3, pp.92-107, 2014.

A. Abramé and D. Habet, On the extension of learning for Max-SAT, Proceedings of the 7th European Starting AI Researcher Symposium (STAIRS 2014), vol.241, pp.1-10, 2014.

A. Abramé and D. Habet, ahmaxsat: Description and Evaluation of a Branch and Bound Max-SAT Solver, Journal on Satisfiability, Boolean Modeling and Computation, vol.9, pp.89-128, 2015.

A. Abramé and D. Habet, On the resiliency of unit propagation to max-resolution, Proceedings of the 24th International Joint Conference on Artificial Intelligence, pp.268-274, 2015.

C. Ansótegui, M. L. Bonet, and J. Levy, Solving (weighted) partial maxsat through satisfiability testing, Theory and Applications of Satisfiability Testing -SAT 2009, pp.427-440, 2009.

M. L. Bonet, J. Levy, and F. Manyà, Resolution for max-sat, Artificial Intelligence, vol.171, issue.8, pp.606-618, 2007.

J. Davies and F. Bacchus, Solving maxsat by solving a sequence of simpler sat instances, International conference on principles and practice of constraint programming, pp.225-239, 2011.

F. Heras and J. Larrosa, New inference rules for efficient Max-SAT solving, Proceedings of the 21st National Conference on Artificial Intelligence, pp.68-73, 2006.

A. Küegel, Improved exact solver for the weighted max-sat problem, POS-10. Pragmatics of SAT, vol.8, pp.15-27, 2012.

C. M. Li, F. Manyà, N. O. Mohamedou, and J. Planes, Resolution-based lower bounds in maxsat, Constraints, vol.15, pp.456-484, 2010.

C. M. Li, F. Manyà, and J. Planes, Detecting Disjoint Inconsistent Subformulas for Computing Lower Bounds for Max-SAT, Proceedings of the 21st National Conference on Artificial Intelligence (AAAI-06), vol.1, pp.86-91, 2006.

C. M. Li, F. Manyà, and J. Planes, New inference rules for max-sat, Journal of Artificial Intelligence Research, vol.30, pp.321-359, 2007.

R. Martins, V. Manquinho, and I. Lynce, Open-wbo: A modular maxsat solver, Theory and Applications of Satisfiability Testing -SAT 2014, pp.438-445, 2014.

N. Narodytska and F. Bacchus, Maximum satisfiability using core-guided maxsat resolution, Proceedings of the Twenty-Eighth Conference on Artificial Intelligence (AAAI-14), pp.2717-2723, 2014.

P. Marques-silva, J. , A. Sakallah, and K. , Grasp: A search algorithm for propositional satisfiability. Computers, IEEE Transactions on, vol.48, pp.506-521, 1999.