}} (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. ,

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. ,

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. ,

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

Solving (weighted) partial maxsat through satisfiability testing, Theory and Applications of Satisfiability Testing -SAT 2009, pp.427-440, 2009. ,

Resolution for max-sat, Artificial Intelligence, vol.171, issue.8, pp.606-618, 2007. ,

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

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

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

Resolution-based lower bounds in maxsat, Constraints, vol.15, pp.456-484, 2010. ,

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. ,

New inference rules for max-sat, Journal of Artificial Intelligence Research, vol.30, pp.321-359, 2007. ,

Open-wbo: A modular maxsat solver, Theory and Applications of Satisfiability Testing -SAT 2014, pp.438-445, 2014. ,

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

Grasp: A search algorithm for propositional satisfiability. Computers, IEEE Transactions on, vol.48, pp.506-521, 1999. ,