On Dedicated CDCL Strategies for PB Solvers
  Current implementations of pseudo-Boolean (PB) solvers working on native PB
constraints are based on the CDCL architecture which empowers highly efficient
modern SAT solvers. In particular, such PB solvers not only implement a
(cutting-planes-based) conflict analysis procedure, but also complementary
strategies for components that are crucial for the efficiency of CDCL, namely
branching heuristics, learned constraint deletion and restarts. However, these
strategies are mostly reused by PB solvers without considering the particular
form of the PB constraints they deal with. In this paper, we present and
evaluate different ways of adapting CDCL strategies to take the specificities
of PB constraints into account while preserving the behavior they have in the
clausal setting. We implemented these strategies in two different solvers,
namely Sat4j (for which we consider three configurations) and RoundingSat. Our
experiments show that these dedicated strategies allow to improve, sometimes
significantly, the performance of these solvers, both on decision and
optimization problems.
