English   español  
Por favor, use este identificador para citar o enlazar a este item: http://hdl.handle.net/10261/162447
COMPARTIR / IMPACTO:
Estadísticas
logo share SHARE logo core CORE   Add this article to your Mendeley library MendeleyBASE

Visualizar otros formatos: MARC | Dublin Core | RDF | ORE | MODS | METS | DIDL
Exportar a otros formatos:
Título

Resolution for Max-SAT

AutorBonet, M. Luisa; Levy, Jordi ; Manyà, Felip
Palabras claveSaturation
Weighted Max-SAT
Max-SAT
Completeness
Resolution
Satisfiability
Fecha de publicación2007
EditorElsevier
CitaciónArtificial Intelligence 171: 606- 618 (2007)
ResumenMax-SAT is the problem of finding an assignment minimizing the number of unsatisfied clauses in a 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. We also define a weighted Max-SAT resolution-like rule, and show how to adapt the soundness and completeness proofs of the Max-SAT rule to the weighted Max-SAT rule. Finally, we give several particular Max-SAT problems that require an exponential number of steps of our Max-SAT rule to obtain the minimal number of unsatisfied clauses of the combinatorial principle. These results are based on the corresponding resolution lower bounds for those particular problems. © 2007 Elsevier B.V. All rights reserved.
URIhttp://hdl.handle.net/10261/162447
Identificadoresdoi: 10.1016/j.artint.2007.03.001
issn: 0004-3702
Aparece en las colecciones: (IIIA) Artículos
Ficheros en este ítem:
Fichero Descripción Tamaño Formato  
accesoRestringido.pdf15,38 kBAdobe PDFVista previa
Visualizar/Abrir
Mostrar el registro completo
 

Artículos relacionados:


NOTA: Los ítems de Digital.CSIC están protegidos por copyright, con todos los derechos reservados, a menos que se indique lo contrario.