Adapting CDCL Strategies for PB Solvers

by Romain Wallon for the 11th Pragmatics of SAT International workshop (http://www.pragmaticsofsat.org/2020/)

Current implementations of pseudo-Boolean (PB) solvers are based on the CDCL architecture, which is the central component of modern SAT solvers. In addition to clause learning, this architecture comes with many strategies that help the solver find its way through the search space, either to a solution or to an unsatisfiability proof. Particularly important are the decision heuristic, but also other features like learned clause deletion or restarts. Currently, these strategies are mostly used "as is" in PB solvers, without considering the particular form of the PB constraints they deal with. In this paper, we introduce new ways of adapting these strategies to better take into account the specificities of such constraints, especially regarding their weights and propagation properties. In particular, our experiments show that carefully considering these criteria may have a significant impact on the performance of the solver.