English   español  
Please use this identifier to cite or link to this item: http://hdl.handle.net/10261/134458
Share/Impact:
Statistics
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:

Title

Efficient Encodings from CSP into SAT, and from MaxCSP into MaxSAT

AuthorsArgelich, Josep; Cabiscol, Alba; Lynce, Ines; Manyà, Felip CSIC ORCID
KeywordsSAT
MaxSAT
MaxCSP
Encoding
CSP
Issue Date2012
PublisherOld City Publishing
CitationJournal of Multiple-Valued Logic and Soft Computing 19 (1): 3- 23 (2012)
AbstractWe first survey existing encondings from CSP intoSAT, and define two new encodings: the minimal support encoding and the interval-based support encoding. Then, we study how the existing and new encodings from CSP into SAT can be extended for encoding MaxCSP into Partial MaxSAT. Finally, we report on the empirical investigation. The obtained results provide empirical evidence of the good performance profile of the new encodings on SAT solvers such as MiniSat and PrecoSAT that incorporate conflict-clause learning, as well as when they are used to encode MaxCSP into Partial MaxSAT and are solved with MaxSAT solvers such as MSUnCore, SAT4J-Maxsat and WMaxSatz. © 2012 Old City Publishing, Inc.
URIhttp://hdl.handle.net/10261/134458
Identifiersissn: 1542-3980
Appears in Collections:(IIIA) Artículos
Files in This Item:
File Description SizeFormat 
accesoRestringido.pdf15,38 kBAdobe PDFThumbnail
View/Open
Show full item record
Review this work
 


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