A Complete Resolution Calculus for Signed Max-SAT

We define a resolution-style rule for solving the Max-SAT problem of Signed CNF formulas (Signed Max-SAT) and prove that our rule provides a complete calculus for that problem. From the completeness proof we derive an original exact algorithm for solving Signed Max-SAT. Finally, we present some connections between our approach and the work done in the Weighted CSP community.

• Type: Conference
• Year: 2007
• Where: ISMVL
• Authors: Carlos Ansótegui, Maria Luisa Bonet, Jordi Levy, Felip Manyà
• Keywords: Artificial Intelligence, ISMVL 2007, Max-SAT Problem, Original Exact Algorithm, Weighted CSP Community