This paper introduces a new SAT solver that integrates logicbased reasoning and integer programming methods to systems of CNF and PB constraints. Its novel features include an efficient PB literal watching strategy and several PB learning methods that take advantage of the pruning power of PB constraints while minimizing their overhead.
Hossein M. Sheini, Karem A. Sakallah