Reflections on Propositional Proofs in Algorithms and Complexity

Overview

The area of proof complexity was introduced by Cook and Reckhow in 1979 as a way to tackle the NP vs coNP problem. The overarching goal of the field is to understand how difficult it is to prove certain mathematical facts. Traditionally, the complexity of a theorem is measured as the length of the shortest proof of the theorem in a given formal system. Since the early years of the field many techniques have been developed to analyze concrete proof systems, including establishing relations to other areas of complexity.

In recent years, many exciting results and new connections to proof complexity were discovered or further developed in areas such as, for example, automated proof search, combinatorial optimization, total NP search problems (TFNP), minimum circuit size problem (MCSP), cryptography, learning, approximation algorithms and sum-of-squares, extension complexity, algebraic complexity and witnessing theorems. The goal of this workshop is to present some of the classical theory in proof complexity, as well as survey some of the recent exciting connections. The talks will be tutorial in style and we especially encourage attendance from people working in related areas who are not familiar with proof complexity.

The workshop is virtual and will take place over Zoom. FOCS registration is required for all participants. The Zoom link will be made available to registered participants.

Speakers

Sam Buss, Joshua Grochow, Pravesh K. Kothari, Jan Krajíček, Toni Pitassi, Susanna de Rezende, Robert Robere, Rahul Santhanam, Neil Thapen

Program

All times are in Eastern Standard Time (US East Coast/New York time, UTC-5).

Videos of all talks are now available here (see also individual links below).

Abstracts

This session is aimed at introducing researchers in other areas of theory to algebraic (and semi-algebraic) proof complexity, and to the wealth of open problems and connections with algebraic circuit complexity, polynomial identity testing, and inapproximability.

Part I: Motivation, history, and introduction to algebraic proof complexity (Toniann Pitassi)

This first talk will give a quick primer on proof complexity, especially as it relates to algebraic proof systems. It will cover some of the history and motivation that led to the study of algebraic proof systems, as well as introduce some well-studied algebraic proof systems and the relations between them.

Part II: Circuit complexity, ideals and proof systems: connections and recent results (Joshua A. Grochow)

The second talk will cover connections between the Ideal Proof System (IPS), circuit complexity, and more generally complexity in ideals. In particular, it will cover the relation between IPS and VP vs VNP, as well as the recent result of Andrews & Forbes that extends the constant-depth algebraic circuit lower bound of Limaye-Srinivasan-Tavenas to a lower bound on refuting certain polynomial equations in IPS. The talk will highlight the connection between algebraic circuit complexity, algebraic proof complexity, and even Boolean circuit complexity to the complexity not of individual (families of) polynomials, but of arbitrary (families of) polynomials inside an ideal or coset of an ideal.

TFNP search problems have the form: find a witness to an NP property of some object, when a witness is always known to exist. For example, given a hash function from n+1 bits to n bits, find a collision.

Subclasses of TFNP are usually defined by specifying a problem and including all problems reducible to it. It turns out that this is essentially the same as specifying a logical theory and including all problems which the theory proves have a solution. I will talk about what TFNP looks like from this point of view.

Essentially any theory can be used. Some useful ones come from bounded arithmetic, where questions about the provability of some relevant combinatorial principles have been well studied. I will say what the corresponding subclasses of TFNP look like; in particular we get subclasses capturing the strength of some standard models of computation. I will use this approach to study the place of the RAMSEY search problem in TFNP, via a theory that captures reasoning using approximate counting.

This talk discusses Total NP Search (TFNP) problems, including Polynomial Local Search (PLS), polylog width Resolution refutations, connections with Bounded Arithmetic, and the Wrong-Proof Search problem. The last part of the talk discusses similar results for Colored Polynomial Local Search (CPLS), Resolution, and the Res(polylog) refutation system.

The recent discovery and rapid development of query-to-communication lifting theorems has led to the resolution of a number of long-standing open problems in communication, circuit, and proof complexity. These results include the resolution of the Alon-Saks-Seymour problem, explicit strongly exponential lower bounds on monotone formula complexity, exponential lower bounds on the size of Cutting Planes proofs for random CNF formulas, and many others. One of the key viewpoints enabling the application of these techniques is a deeper understanding of both proof complexity and circuit complexity through the use of certain total search problems. These characterizations greatly expand on several classical results in complexity theory, such as the characterization of circuit depth by Karchmer-Wigderson games and the equivalence between tree-like Resolution and decision trees.

In this talk, we outline a systematic research program that classifies propositional proof systems and circuit classes using the theory of total search problems. The complexity classes in the theory of TFNP, in particular, turn out to provide a natural organizing principle for many proof and circuit classes, and many lower bound results in circuit and proof complexity can be naturally cast into this framework. Future directions and concrete open problems will be discussed.

A recently discovered new proof complexity measure based on algorithmic information seems to play as a fundamental role for proof search as the size measure plays for classical proof complexity centered around lengths-of-proofs notions and problems.

One cannot hope to separate unconditionally, for any proof system, the information measure from (the log of) the size measure as that would imply that P differs from NP.

But is it possible to prove non-trivial lower bounds for information in some cases where we failed so far to prove size lower bounds?

This problem seems to be quite inspiring and possibly runs rather deep. I shall explain the necessary background and discuss several facets of the problem.

Super-polynomial proof size lower bounds for strong propositional proof systems such as Frege and EF have remained out of reach, despite intensive efforts. Are there mathematical reasons why strong proof complexity lower bounds are hard to show? I will discuss recent work that sheds light on this question.

Based on joint work with Jan Pich and Iddo Tzameret.

A 3-SAT formula with randomly generated m clauses over n variables for m ≫ 5n is unsatisfiable with high probability. For what range of m do such formulas admit short refutations, i.e., efficiently verifiable proofs of unsatisfiability? And when can we find such proofs efficiently?

These questions have a three-decade-long history beginning with the beautiful 1988 paper of Chvátal and Szemerédi. Over time, they have served as a testbed for developing new techniques in proof complexity and average-case algorithm design in addition to yielding canonical hardness assumptions with applications to cryptography, learning theory, and complexity of statistical inference.

In this talk, I'll present a taste of three techniques developed over the past two decades that yield the strongest results for refuting CSPs: 1) combinatorial techniques based on even covers, 2) spectral methods based on eigenvalues of appropriate matrices, and 3) semidefinite programming/sum-of-squares method. My focus will be on recent works that yield significantly simpler arguments that generalize to more general semi-random models of CSPs. In addition, these new analyses reveal a surprising new relationship between combinatorial and spectral/SDP-based techniques and lead to a proof Feige's 2008 conjecture on girth-density trade-offs for worst-case hypergraphs.

Based on joint works with Venkatesan Guruswami, Peter Manohar, and Jackson Abascal.

Organizers: Toni Pitassi, Robert Robere, Susanna de Rezende

Workshop co-chairs: Alexander Sherstov, Vincent Cohen-Addad