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
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.
