|Título||Resolution for Max-SAT|
|Publication Type||Journal Article|
|Year of Publication||2007|
|Authors||Bonet MLuisa, Levy J, Manyà F|
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.
- Acerca del IIIA
- 25 aniversario