English   español  
Por favor, use este identificador para citar o enlazar a este item: http://hdl.handle.net/10261/133776
Compartir / Impacto:
Add this article to your Mendeley library MendeleyBASE
Visualizar otros formatos: MARC | Dublin Core | RDF | ORE | MODS | METS | DIDL

Resolution procedures for multiple-valued optimization

AutorAnsotegui, Carlos; Bonet, María L.; Levy, Jordi ; Manya, Felip
Palabras claveMultiple-valued logics
Maximum satisfiability
Signed logic
Fecha de publicación2013
CitaciónInformation Sciences 227: 43- 59 (2013)
ResumenSigned clausal forms offer a suitable logical framework for automated reasoning in multiple-valued logics. It turns out that the satisfiability problem of any finitely-valued propositional logic, as well as of certain infinitely-valued logics, can be easily reduced, in polynomial time, to the satisfiability problem of signed clausal forms. On the other hand, signed clausal forms are a powerful knowledge representation language for constraint programming, and have shown to be a practical and competitive approach to solving combinatorial decision problems. Motivated by the existing theoretical and practical results for the satisfiability problem of signed clausal forms, as well as by the recent logical and algorithmic results on the Boolean maximum satisfiability problem, in this paper we investigate the maximum satisfiability problem of propositional signed clausal forms from the logical and practical points of view. From the logical perspective, our aim is to define complete inference systems taking as a starting point the resolution-style calculi defined for the Boolean CNF case. The result is the definition of two sound and complete resolution-style rules, called signed binary resolution and signed parallel resolution for maximum satisfiability. From the practical perspective, our main motivation is to use the language of signed clausal forms along with the newly defined inference systems as a generic approach to solve combinatorial optimization problems, and not just for solving decision problems as so far. The result is the establishment of a link between signed logic and constraint programming that provides a concise and elegant logical framework for weighted constraint programming. © 2012 Elsevier Inc. All rights reserved.
Identificadoresdoi: 10.1016/j.ins.2012.12.004
issn: 0020-0255
Aparece en las colecciones: (IIIA) Artículos
Ficheros en este ítem:
Fichero Descripción Tamaño Formato  
accesoRestringido.pdf15,38 kBAdobe PDFVista previa
Mostrar el registro completo

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