DocumentCode
2671653
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
fYear
2007
fDate
13-16 May 2007
Firstpage
22
Lastpage
22
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;
fLanguage
English
Publisher
ieee
Conference_Titel
Multiple-Valued Logic, 2007. ISMVL 2007. 37th International Symposium on
Conference_Location
Oslo
ISSN
0195-623X
Print_ISBN
0-7695-2831-7
Type
conf
DOI
10.1109/ISMVL.2007.2
Filename
4215945
Link To Document