Skip to content



A complete resolution-like calculus for Maxsat

Bonet, ML (Barcelona)
Thursday 13 April 2006, 10:00-10:30

Seminar Room 1, Newton Institute


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. Joint work with Jordi Levy and Felip Manya.


MP3MP3 Real AudioReal Audio

Back to top ∧