Collaborative Research: AF:Medium: Advancing the Lower Bound Frontier

The central problem in computational complexity theory is to develop the most efficient algorithms for important computational problems. To prove that an algorithm is the most efficient, the holy grail of complexity theory is to prove unconditional lower bounds, showing that any algorithm, however clever or sophisticated, will inherently require a certain amount of resources (hardware, or runtime) to solve. The goal of this research is to tackle the most basic challenge of proving circuit and runtime lower bounds for explicit problems, as well as similar challenges in proof and communication complexity lower bounds.In more detail, this project is focused on two approaches. The first approach involves exploiting the two-way connection between circuit lower bounds and meta-algorithms, algorithms whose inputs or outputs are circuits or other algorithm descriptions. Important examples of meta-algorithms are: circuit satisfiability, where the input is a circuit and the output is whether it is satisfiable; proof search, where the input is an unsatisfiable formula and the output is a small refutation of it in a proof system; and PAC learning, where the input consists of labelled examples of an unknown target function to be output. Often, paradoxically, efficient algorithms for meta-computational problems such as these lead to improved lower bounds and vice versa. The second approach is known as lifting, whereby lower bounds in a more complex model of computation are reduced to lower bounds in a simpler model. Through lifting and related ideas, circuit complexity has been related to proof complexity and communication complexity, and lower bounds have been improved for all three settings. The team of researchers will investigate a variety of ideas to extend and deepen these approaches to push past the current barriers in lower bounds. The research is also expected to develop improved algorithms for meta-algorithmic problems, which are of central importance for hardware and software verification, algorithmic learning, and a broad range of other applications.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.