On Weakening Strategies for PB Solvers
This work addresses a specific bottleneck in pseudo-Boolean solving for constraint satisfaction problems, offering incremental improvements to solver efficiency.
The paper tackles the problem of weakening strategies in pseudo-Boolean solvers, which are essential for conflict analysis but previously unassessed for performance impact, and finds that new strategies, such as applying weakening on the conflict side or partial weakening and division on both sides, improve solver runtime in implementations like Sat4j.
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.