Daniel Dadush and Samarth Tiwari from CWI's Networks and Optimization research group receive the Best Paper Award at CCC'20, the Computational Complexity Conference, for their work 'On the Complexity of Branching Proofs'. This year, the conference takes place online instead of Saarbruecken, from 28-30 July.
Tiwari explains the topic of the award winning paper: "Designing fast algorithms to solve various computational problems is the central goal of computer science. Proof complexity theorists study the related problem of proving that a solution is indeed correct: for some hard problems, devising proofs (or 'certificates') is difficult in itself. Modern optimization software and bug-detecting software routinely produce and work with such proofs."
The PhD student continues: "A proof of correctness, like a solution to a high school math problem, consists of step-by-step logical deductions. In fact, the number of steps in a proof is one measure of its complexity. Another is its total size, say, in kilobytes. The size of a proof depends not only on the number of logical deductions, but also on the size of each step. Daniel and I both analyzed different kinds of such certificates from a geometric perspective. We related the size of a proof directly to the number of steps needed by bounding the complexity of a single step in a proof."
A long-standing conjecture in the field asserted that certificates for the correctness of so-called Tseitin formulas must be long. Dadush and Tiwari now refuted this conjecture, demonstrating that Tseitin formulas admit shorter certificates than previously thought. They attribute their results to reinterpreting well-known techniques from proof complexity in the language of integer programming. Through extended collaboration between these two disciplines, they hope to build bridges and enrich understanding of fundamental questions in theoretical computer science.
The talk of Samarth Tiwari and Daniel Dadush for CCC'20 can be seen online.
More information
- CCC'20 conference
- CWI's Networks and Optimization research group
- the online talk of Samarth Tiwari and Daniel Dadush for CCC'20
- the award winning paper, On the Complexity of Branching Proofs