Cargando…

Towards a Better Understanding of (Partial Weighted) MaxSAT Proof Systems

MaxSAT is a very popular language for discrete optimization with many domains of application. While there has been a lot of progress in MaxSAT solvers during the last decade, the theoretical analysis of MaxSAT inference has not followed the pace. Aiming at compensating that lack of balance, in this...

Descripción completa

Detalles Bibliográficos
Autores principales: Larrosa, Javier, Rollon, Emma
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2020
Materias:
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7326545/
http://dx.doi.org/10.1007/978-3-030-51825-7_16
_version_ 1783552367701000192
author Larrosa, Javier
Rollon, Emma
author_facet Larrosa, Javier
Rollon, Emma
author_sort Larrosa, Javier
collection PubMed
description MaxSAT is a very popular language for discrete optimization with many domains of application. While there has been a lot of progress in MaxSAT solvers during the last decade, the theoretical analysis of MaxSAT inference has not followed the pace. Aiming at compensating that lack of balance, in this paper we do a proof complexity approach to MaxSAT resolution-based proof systems. First, we give some basic definitions on completeness and show that refutational completeness makes compleness redundant, as it happens in SAT. Then we take three inference rules such that adding them sequentially allows us to navigate from the weakest to the strongest resolution-based MaxSAT system available (i.e., from standalone MaxSAT resolution to the recently proposed ResE), each rule making the system stronger. Finally, we show that the strongest system captures the recently proposed concept of Circular Proof while being conceptually simpler, since weights, which are intrinsic in MaxSAT, naturally guarantee the flow condition required for the SAT case.
format Online
Article
Text
id pubmed-7326545
institution National Center for Biotechnology Information
language English
publishDate 2020
record_format MEDLINE/PubMed
spelling pubmed-73265452020-07-01 Towards a Better Understanding of (Partial Weighted) MaxSAT Proof Systems Larrosa, Javier Rollon, Emma Theory and Applications of Satisfiability Testing – SAT 2020 Article MaxSAT is a very popular language for discrete optimization with many domains of application. While there has been a lot of progress in MaxSAT solvers during the last decade, the theoretical analysis of MaxSAT inference has not followed the pace. Aiming at compensating that lack of balance, in this paper we do a proof complexity approach to MaxSAT resolution-based proof systems. First, we give some basic definitions on completeness and show that refutational completeness makes compleness redundant, as it happens in SAT. Then we take three inference rules such that adding them sequentially allows us to navigate from the weakest to the strongest resolution-based MaxSAT system available (i.e., from standalone MaxSAT resolution to the recently proposed ResE), each rule making the system stronger. Finally, we show that the strongest system captures the recently proposed concept of Circular Proof while being conceptually simpler, since weights, which are intrinsic in MaxSAT, naturally guarantee the flow condition required for the SAT case. 2020-06-26 /pmc/articles/PMC7326545/ http://dx.doi.org/10.1007/978-3-030-51825-7_16 Text en © Springer Nature Switzerland AG 2020 This article is made available via the PMC Open Access Subset for unrestricted research re-use and secondary analysis in any form or by any means with acknowledgement of the original source. These permissions are granted for the duration of the World Health Organization (WHO) declaration of COVID-19 as a global pandemic.
spellingShingle Article
Larrosa, Javier
Rollon, Emma
Towards a Better Understanding of (Partial Weighted) MaxSAT Proof Systems
title Towards a Better Understanding of (Partial Weighted) MaxSAT Proof Systems
title_full Towards a Better Understanding of (Partial Weighted) MaxSAT Proof Systems
title_fullStr Towards a Better Understanding of (Partial Weighted) MaxSAT Proof Systems
title_full_unstemmed Towards a Better Understanding of (Partial Weighted) MaxSAT Proof Systems
title_short Towards a Better Understanding of (Partial Weighted) MaxSAT Proof Systems
title_sort towards a better understanding of (partial weighted) maxsat proof systems
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7326545/
http://dx.doi.org/10.1007/978-3-030-51825-7_16
work_keys_str_mv AT larrosajavier towardsabetterunderstandingofpartialweightedmaxsatproofsystems
AT rollonemma towardsabetterunderstandingofpartialweightedmaxsatproofsystems