English   español  
Please use this identifier to cite or link to this item: http://hdl.handle.net/10261/133776
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 | DATACITE
Exportar a otros formatos:


Resolution procedures for multiple-valued optimization

AuthorsAnsotegui, Carlos; Bonet, Maria Luisa; Levy, Jordi CSIC ORCID ; Manyà, Felip CSIC ORCID
KeywordsMultiple-valued logics
Maximum satisfiability
Signed logic
Issue Date2013
CitationInformation Sciences 227: 43- 59 (2013)
AbstractSigned 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.
Identifiersdoi: 10.1016/j.ins.2012.12.004
issn: 0020-0255
Appears in Collections:(IIIA) Artículos
Files in This Item:
File Description SizeFormat 
accesoRestringido.pdf15,38 kBAdobe PDFThumbnail
Show full item record
Review this work

Related articles:

WARNING: Items in Digital.CSIC are protected by copyright, with all rights reserved, unless otherwise indicated.