English   español  
Please use this identifier to cite or link to this item: http://hdl.handle.net/10261/197694
logo share SHARE   Add this article to your Mendeley library MendeleyBASE

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


Clause Branching in MaxSAT and MinSAT

AuthorsArgelich, Josep; Li, Chu Min; Manyà, Felip ; Zhu, Zhu
Issue Date2018
PublisherIOS Press
CitationFrontiers in Artificial Intelligence and Applications: 17-26 (2018)
AbstractWe describe a new exact procedure, inspired on recent works on tableaux, for simultaneously solving MaxSAT and MinSAT. The main novelty of our procedure is that it implements a clause branching rule that preserves both the minimum and the maximum number of clauses than can be unsatisfied. Moreover, we prove the correctness of the procedure, and provide a review of the different types of branchings which are available for MaxSAT and MinSAT. We also give some preliminary experimental results that show that the new branching rule, when implemented into an existing branch-and-bound MaxSAT solver, produces substantial gains on industrial instances of the MaxSAT Evaluation.
DescriptionTrabajo presentado en el 21st International Conference of the Catalan Association for Artificial Intelligence (CCIA 2018), celebrada en Roses (España) del 8 al 10 de Octubre de 2018
Publisher version (URL)http://dx.doi.org/10.3233/978-1-61499-918-8-17
Appears in Collections:(IIIA) Libros y partes de libros
Files in This Item:
File Description SizeFormat 
accesoRestringido.pdf15,35 kBAdobe PDFThumbnail
Show full item record
Review this work

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