Proofs and Practical Algorithm Analysis

Tuesday, July 20, 2-3 p.m.

Online

Noah Fleming

Faculty candidate

Abstract:

Despite being an NP-hard problem, there has been extraordinary success in designing algorithms which are able to routinely solve instances of SAT that occur in practice. An analogous situation has occurred for integer programming, where researchers have been able to design blazingly fast practical integer programming solvers. This makes explaining the efficacy of these algorithms an exciting open problem. However, these algorithms are finely-tuned and interlinked heuristics, which makes analyzing them directly a daunting task. An effective method for overcoming this is to formalize the techniques used by a class of algorithms as a formal proof system — a set of rules for making logical inferences — and then analyze the proof system instead. This allows us to hide many of the practical details of the implementations of the algorithms, without limiting the capabilities of the algorithms. The analysis of these proof systems falls under the purview of Proof Complexity — an exciting area of research aimed at ultimately resolving the P versus NP question by studying the complexity of proof systems.

In this talk, we will analyze modern SAT and integer programming algorithms through the perspective of proof complexity. We will show that modern integer programming solvers can be formalized by the powerful Stabbing Planes proof system. Then, by establishing the first lower bounds on the complexity of Stabbing Planes proofs, we will exhibit a natural family of inputs which require exponential runtime for modern integer programming algorithms. Similarly, we will use the fact that modern algorithms for SAT are formalized by Resolution proofs in order to gain a deeper understanding of these algorithms. We will explore questions such as whether these algorithms can be parallelized, and to what extent each subroutine of these algorithms contributes to its efficiency.

Join: https://mun.webex.com/mun/j.php?MTID=m7f2e1dff531ee4cb3d9ac5e1f2befea3

Presented by Department of Computer Science

Event Listing 2021-07-20 14:00:00 2021-07-20 15:00:00 America/St_Johns Proofs and Practical Algorithm Analysis Noah Fleming Faculty candidate Abstract: Despite being an NP-hard problem, there has been extraordinary success in designing algorithms which are able to routinely solve instances of SAT that occur in practice. An analogous situation has occurred for integer programming, where researchers have been able to design blazingly fast practical integer programming solvers. This makes explaining the efficacy of these algorithms an exciting open problem. However, these algorithms are finely-tuned and interlinked heuristics, which makes analyzing them directly a daunting task. An effective method for overcoming this is to formalize the techniques used by a class of algorithms as a formal proof system — a set of rules for making logical inferences — and then analyze the proof system instead. This allows us to hide many of the practical details of the implementations of the algorithms, without limiting the capabilities of the algorithms. The analysis of these proof systems falls under the purview of Proof Complexity — an exciting area of research aimed at ultimately resolving the P versus NP question by studying the complexity of proof systems. In this talk, we will analyze modern SAT and integer programming algorithms through the perspective of proof complexity. We will show that modern integer programming solvers can be formalized by the powerful Stabbing Planes proof system. Then, by establishing the first lower bounds on the complexity of Stabbing Planes proofs, we will exhibit a natural family of inputs which require exponential runtime for modern integer programming algorithms. Similarly, we will use the fact that modern algorithms for SAT are formalized by Resolution proofs in order to gain a deeper understanding of these algorithms. We will explore questions such as whether these algorithms can be parallelized, and to what extent each subroutine of these algorithms contributes to its efficiency. Join: https://mun.webex.com/mun/j.php?MTID=m7f2e1dff531ee4cb3d9ac5e1f2befea3 Online Department of Computer Science