Publications

A Complete Calculus for Max-SAT

Publication Type:

Conference Paper

Authors:

María Luisa Bonet; Jordi Levy; Felip Manyà

Source:

Lecture Notes in Computer Science, Springer-Verlag, Volume 4121, p.240-251 (2006)

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.

Projects: 
MULOG
»