|Title||A Complete Calculus for Max-SAT|
|Publication Type||Conference Paper|
|Year of Publication||2006|
|Authors||Bonet MLuisa, Levy J, Manyà F|
|Conference Name||Lecture Notes in Computer Science|
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.
- About IIIA
- Current news