Title | A Complete Calculus for Max-SAT |

Publication Type | Conference Paper |

Year of Publication | 2006 |

Authors | Bonet MLuisa [1], Levy J [2], Manyà F [3] |

Conference Name | Lecture Notes in Computer Science |

Volume | 4121 |

Publisher | Springer-Verlag |

Pagination | 240-251 |

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. |