Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

New Hybrid Heuristics for Pseudo-Boolean Propagation

Mia Müßig, Jan Johannsen

TL;DR

The paper tackles the efficiency of unit propagation in pseudo-Boolean solving by refining the hybrid counting-watched-literal method. It introduces two heuristics, Absolute Hybrid and Additive Hybrid, that decide when to use counting versus watching based on coefficient magnitudes, and demonstrates substantial runtime improvements on PB competition datasets, especially for knapsack-like instances. The changes require minimal code modifications, suggesting easy integration and potential automatic tuning based on instance characteristics. Overall, the work advances practical performance of PB solvers by targeted heuristic tuning of the propagation mechanism.

Abstract

In pseudo-boolean solving the currently most successful unit propagation strategy is a hybrid mode combining the watched literal scheme with the counting method. This short paper introduces new heuristics for this hybrid decision, which are able to drastically outperform the current method in the RoundingSAT solver.

New Hybrid Heuristics for Pseudo-Boolean Propagation

TL;DR

The paper tackles the efficiency of unit propagation in pseudo-Boolean solving by refining the hybrid counting-watched-literal method. It introduces two heuristics, Absolute Hybrid and Additive Hybrid, that decide when to use counting versus watching based on coefficient magnitudes, and demonstrates substantial runtime improvements on PB competition datasets, especially for knapsack-like instances. The changes require minimal code modifications, suggesting easy integration and potential automatic tuning based on instance characteristics. Overall, the work advances practical performance of PB solvers by targeted heuristic tuning of the propagation mechanism.

Abstract

In pseudo-boolean solving the currently most successful unit propagation strategy is a hybrid mode combining the watched literal scheme with the counting method. This short paper introduces new heuristics for this hybrid decision, which are able to drastically outperform the current method in the RoundingSAT solver.

Paper Structure

This paper contains 5 sections, 3 equations, 3 figures, 1 algorithm.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. New Hybrid Heuristics
  4. Conclusion
  5. Appendix

Figures (3)

  • Figure 1: Runtime comparison on the 206 instances of the OPT-LIN and DEC-LIN track from the Pseudo Boolean Competition 2025, where at least one constraint contains a coefficient $\geq 100$.
  • Figure 2: Runtime comparison on the 783 knapsack instances from the Pseudo Boolean Competition dataset.
  • Figure 3: Runtime comparison with more $c$ values on the 206 instances of the OPT-LIN and DEC-LIN track from the Pseudo Boolean Competition 2025, where at least one constraint contains a coefficient $\geq 100$.