Abstract
Pseudo-Boolean solving is the task of finding a solution to a collection of (linear) pseudo-Boolean constraints, also known as a 0-1 integer linear program, possibly optimizing some linear objective function. This problem can be approached using methods from conflict-driven clause learning (CDCL) SAT solving as in MaxSAT solvers, or "native" pseudo-Boolean reasoning based on variants of the cutting planes proof system, or (mixed) integer linear programming (MIP). The purpose of this tutorial is to provide a brief survey of pseudo-Boolean reasoning, MaxSAT solving, and integer linear programming, focusing on the potential for synergy between these different approaches and highlighting many open problems on both the applied and the theoretical side.