Pueblo: A Modern Pseudo-Boolean SAT Solver

The paper introduces a new SAT (satisfiability) solver that integrates logic-based 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.