Resolution for Max-SAT

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. We also give a weighted Max-SAT resolution-like rule, and show how to adapt the soundness and completeness proofs of the Max-SAT rule to the weighted Max-SAT one. Finally we give several particular Max-SAT problems that require an exponential number of steps of our Max-SAT rule to obtain the minimal number of unsatisfied clauses of the combinatorial principle. These results are based on the corresponding Resolution lower bounds for those particular problems.