@article{Larrosa_Rollon_2020, title={Augmenting the Power of (Partial) MaxSat Resolution with Extension}, volume={34}, url={https://ojs.aaai.org/index.php/AAAI/article/view/5516}, DOI={10.1609/aaai.v34i02.5516}, abstractNote={<p>The refutation power of SAT and MaxSAT resolution is challenged by problems like the <em>soft</em> and <em>hard</em> <em>Pigeon Hole Problem</em> PHP for which short refutations do not exist. In this paper we augment the MaxSAT resolution proof system with an <em>extension</em> rule. The new proof system MaxResE is sound and complete, and more powerful than plain MaxSAT resolution, since it can refute the soft and hard PHP in polynomial time. We show that MaxResE refutations actually subtract lower bounds from the objective function encoded by the formulas. The resulting formula is the <em>residual</em> after the lower bound extraction. We experimentally show that the residual of the soft PHP (once its necessary cost of 1 has been efficiently subtracted with MaxResE) is a concise, easy to solve, satisfiable problem.</p>}, number={02}, journal={Proceedings of the AAAI Conference on Artificial Intelligence}, author={Larrosa, Javier and Rollon, Emma}, year={2020}, month={Apr.}, pages={1561-1568} }