Title :
A Complete Resolution Calculus for Signed Max-SAT
Author :
Ansótegui, Carlos ; Bonet, María L. ; Levy, Jordi ; Manyà, Felip
Author_Institution :
DIEI, UdL Lleida, Lleida
Abstract :
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.
Keywords :
Boolean functions; computability; process algebra; Boolean Max-SAT problem; complete resolution calculus; original exact algorithm; signed CNF formulas; signed Max-SAT; weighted CSP community; Acoustic testing; Calculus; Constraint theory; Encoding; Inference algorithms; Large scale integration; Logic; Performance evaluation;
Conference_Titel :
Multiple-Valued Logic, 2007. ISMVL 2007. 37th International Symposium on
Conference_Location :
Oslo
Print_ISBN :
0-7695-2831-7
DOI :
10.1109/ISMVL.2007.2