# On Dedicated CDCL Strategies for PB Solvers

arXiv: https://arxiv.org/abs/2109.01013 · HTML: https://mlsanity.com/paper/2109.01013/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 3 of its 38 references that are in the map.
- First posted on arXiv 2 Sep 2021.

## Builds on (most cited first, 3 of 3)

- [Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution](https://mlsanity.com/paper/1401.3868/) (2014)
- [On Weakening Strategies for PB Solvers](https://mlsanity.com/paper/2005.04466/) (2020)
- [On Irrelevant Literals in Pseudo-Boolean Constraint Learning](https://mlsanity.com/paper/2012.04424/) (2020)

## Built on by (most cited first, 1 of 1)

- [Which algorithm to select in sports timetabling?](https://mlsanity.com/paper/2309.03229/) (2023)

## Abstract (arXiv)

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.