@conference {IIIA-2006-1247, title = {A Complete Calculus for Max-SAT}, booktitle = {Lecture Notes in Computer Science}, volume = {4121}, year = {2006}, pages = {240-251}, publisher = {Springer-Verlag}, organization = {Springer-Verlag}, abstract = {Max-SAT is the problem of finding an assignment minimizing the number of unsatisfied clauses of a given CNF formula. We propose a resolution-like calculus for Max-SAT and prove its soundness and completeness. We also prove the completeness of some refinements of this calculus. From the completeness proof we derive an exact algorithm for Max-SAT and a time upper bound.}, author = {Mar{\'\i}a Luisa Bonet and Jordi Levy and Felip Many{\`a}} }