On Improving the Backjump Level in PB Solvers
  Current PB solvers implement many techniques inspired by the CDCL
architecture of modern SAT solvers, so as to benefit from its practical
efficiency. However, they also need to deal with the fact that many of the
properties leveraged by this architecture are no longer true when considering
PB constraints. In this paper, we focus on one of these properties, namely the
optimality of the so-called first unique implication point (1-UIP). While it is
well known that learning the first assertive clause produced during conflict
analysis ensures to perform the highest possible backjump in a SAT solver, we
show that there is no such guarantee in the presence of PB constraints. We also
introduce and evaluate different approaches designed to improve the backjump
level identified during conflict analysis by allowing to continue the analysis
after reaching the 1-UIP. Our experiments show that sub-optimal backjumps are
fairly common in PB solvers, even though their impact on the solver is not
clear.
