Cargando…

On Weakening Strategies for PB Solvers

Current pseudo-Boolean solvers implement different variants of the cutting planes proof system to infer new constraints during conflict analysis. One of these variants is generalized resolution, which allows to infer strong constraints, but suffers from the growth of coefficients it generates while...

Descripción completa

Detalles Bibliográficos
Autores principales: Le Berre, Daniel, Marquis, Pierre, Wallon, Romain
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2020
Materias:
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7326540/
http://dx.doi.org/10.1007/978-3-030-51825-7_23
_version_ 1783552366541275136
author Le Berre, Daniel
Marquis, Pierre
Wallon, Romain
author_facet Le Berre, Daniel
Marquis, Pierre
Wallon, Romain
author_sort Le Berre, Daniel
collection PubMed
description Current pseudo-Boolean solvers implement different variants of the cutting planes proof system to infer new constraints during conflict analysis. One of these variants is generalized resolution, which allows to infer strong constraints, but suffers from the growth of coefficients it generates while combining pseudo-Boolean constraints. Another variant consists in using weakening and division, which is more efficient in practice but may infer weaker constraints. In both cases, weakening is mandatory to derive conflicting constraints. However, its impact on the performance of pseudo-Boolean solvers has not been assessed so far. In this paper, new application strategies for this rule are studied, aiming to infer strong constraints with small coefficients. We implemented them in Sat4j and observed that each of them improves the runtime of the solver. While none of them performs better than the others on all benchmarks, applying weakening on the conflict side has surprising good performance, whereas applying partial weakening and division on both the conflict and the reason sides provides the best results overall.
format Online
Article
Text
id pubmed-7326540
institution National Center for Biotechnology Information
language English
publishDate 2020
record_format MEDLINE/PubMed
spelling pubmed-73265402020-07-01 On Weakening Strategies for PB Solvers Le Berre, Daniel Marquis, Pierre Wallon, Romain Theory and Applications of Satisfiability Testing – SAT 2020 Article Current pseudo-Boolean solvers implement different variants of the cutting planes proof system to infer new constraints during conflict analysis. One of these variants is generalized resolution, which allows to infer strong constraints, but suffers from the growth of coefficients it generates while combining pseudo-Boolean constraints. Another variant consists in using weakening and division, which is more efficient in practice but may infer weaker constraints. In both cases, weakening is mandatory to derive conflicting constraints. However, its impact on the performance of pseudo-Boolean solvers has not been assessed so far. In this paper, new application strategies for this rule are studied, aiming to infer strong constraints with small coefficients. We implemented them in Sat4j and observed that each of them improves the runtime of the solver. While none of them performs better than the others on all benchmarks, applying weakening on the conflict side has surprising good performance, whereas applying partial weakening and division on both the conflict and the reason sides provides the best results overall. 2020-06-26 /pmc/articles/PMC7326540/ http://dx.doi.org/10.1007/978-3-030-51825-7_23 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
Le Berre, Daniel
Marquis, Pierre
Wallon, Romain
On Weakening Strategies for PB Solvers
title On Weakening Strategies for PB Solvers
title_full On Weakening Strategies for PB Solvers
title_fullStr On Weakening Strategies for PB Solvers
title_full_unstemmed On Weakening Strategies for PB Solvers
title_short On Weakening Strategies for PB Solvers
title_sort on weakening strategies for pb solvers
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7326540/
http://dx.doi.org/10.1007/978-3-030-51825-7_23
work_keys_str_mv AT leberredaniel onweakeningstrategiesforpbsolvers
AT marquispierre onweakeningstrategiesforpbsolvers
AT wallonromain onweakeningstrategiesforpbsolvers