Abstract
The last couple of decades has witnessed a revolution in combinatorial optimization, with modern algorithms being used routinely to solve large-scale real-world problems, but the scientific understanding how these so-called combinatorial solvers can perform so well is quite poor. More importantly, even mature commercial solvers are known to sometimes produce wrong answers, which can be fatal for some types of applications.
We will discuss how proof complexity can be leveraged to design so-called certifying solvers, which output not only an answer but also a machine-verifiable proof that this answer is correct. Quite surprisingly, it turns out that cutting planes, if suitably extended, seems to hit a sweet spot between simplicity and expressivity, making it a suitable proof system for not only advanced Boolean satisfiability (SAT) solving but also MaxSAT solving, pseudo-Boolean optimization, and constraint programming.