2024-03-28T21:27:20Zhttp://digital.csic.es/dspace-oai/requestoai:digital.csic.es:10261/1976942020-01-14T02:46:02Zcom_10261_60com_10261_4col_10261_1195
Clause Branching in MaxSAT and MinSAT
Argelich, Josep
Li, Chu Min
Manyà, Felip
Zhu, Zhu
European Commission
Trabajo 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
We 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.
2020-01-13T12:08:08Z
2020-01-13T12:08:08Z
2018
comunicación de congreso
Frontiers in Artificial Intelligence and Applications: 17-26 (2018)
978-1-61499-917-1
http://hdl.handle.net/10261/197694
10.3233/978-1-61499-918-8-17
http://dx.doi.org/10.13039/501100000780
eng
http://dx.doi.org/10.3233/978-1-61499-918-8-17
Sí
info:eu-repo/grantAgreement/EC/H2020/769142
info:eu-repo/grantAgreement/MINECO/Plan Estatal de Investigación Científica y Técnica y de Innovación 2013-2016/TIN2015-71799-C2-1-P
info:eu-repo/grantAgreement/MINECO/Plan Estatal de Investigación Científica y Técnica y de Innovación 2013-2016/TIN2015-71799-C2-2-P
closedAccess
IOS Press