skip to content

A complete resolution-like calculus for Maxsat

Thursday 13th April 2006 - 10:00 to 10:30
INI Seminar Room 1

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.

Presentation Material: 
University of Cambridge Research Councils UK
    Clay Mathematics Institute London Mathematical Society NM Rothschild and Sons