Schedule for: 20w5144 - Proof Complexity

A buffet dinner is served daily between 5:30pm and 7:30pm in the Vistas Dining Room, the top floor of the Sally Borden Building.

Breakfast is served daily between 7 and 9am in the Vistas Dining Room, the top floor of the Sally Borden Building.

A brief introduction to BIRS with important logistical information, technology instruction, and opportunity for participants to ask questions.

A biased, incomplete high-level survey of progress in proof complexity over the last two decades. The start of a conversation about where to go next.

Over the past several decades, an exciting interplay between proof systems and algorithms has emerged. Several prominent algorithms can be viewed as direct translations of proofs that a solution exists into an algorithm for finding that solution. Perhaps nowhere is this connection more prominent than in the context of semi-algebraic proof systems and large classes linear and semi-definite programs. The proof system perspective, in this context, has provided fundamentally new tools for both algorithm design and analysis. These news tools have helped in both designing better algorithms for well-studied problems and proving tight lower bounds on such techniques. This talk will focus on this connection for the Sum-of-Squares proof system. In the first half, I will develop Sum-of-Squares both as a proof system and as a meta-algorithm. In doing so, I will discuss issues such as the duality between these two perspectives, and under what conditions Sum-of-Squares can be assumed to be automatizable. The second half of the talk will survey the landscape of Sum-of-Squares. This will include how Sum-of-Squares relates to other proof systems and to other semi-definite programs. As well, I will survey some of the applications of the connection between these two perspectives of Sum-of-Squares to the design of efficient algorithms for a variety of optimization problems.

Hardness condensation (or compression) is a technique that allows to drastically reduce the number of variables in a contradictory formula while preserving its hardness for a proof system. It is based on substituting variables with more complicated formulas in such a way that the dependence relation between old and new variables makes a good expander. In this talk we will review several applications of this technique; a significant part of it will be devoted to actual proofs of one or, time permitting, even two results.

Lunch is served daily between 11:30am and 1:30pm in the Vistas Dining Room, the top floor of the Sally Borden Building.

Meet in the Corbett Hall Lounge for a guided tour of The Banff Centre campus.

Meet in foyer of TCPL to participate in the BIRS group photo. The photograph will be taken outdoors, so dress appropriately for the weather. Please don't be late, or you might not be in the official group photo!

I will talk about recent joint work with Nicola Galesi and Neil Thapen. Our main result is that if a $k$-CNF can be refuted in polynomial calculus (or, in fact, PCR) in space $s$, then it has a resolution refutation of width $O(s^2)$.

We present a size-degree trade-off for Sums-of-Squares proofs that is analogous to the previous size-width and size-degree trade-offs for resolution and polynomial calculus. We discuss a strong duality theorem between provable lower bounds and pseudoexpectation values that is key to our proof method, and ways to extend the result to Positivstellensatz proof system. Joint work with Albert Atserias.

One of the major open problem in proof complexity is to prove lower bounds on $AC_0[p]$-Frege proof systems. As a step toward this goal Impagliazzo, Mouli and Pitassi in a recent paper suggested to prove lower bounds on the size for Polynomial Calculus over the $\{\pm 1\}$ basis. In this talk we show a technique for proving such lower bounds and moreover we also give lower bounds on the size for Sum-of-Squares over the $\{\pm 1\}$ basis. We show lower bounds on random $\Delta$-CNF formulas and formulas composed with a gadget. As a byproduct, we establish a separation between Polynomial Calculus and Sum-of-Squares over the $\{\pm 1\}$ basis by proving a lower bound on the Pigeonhole Principle.

A buffet dinner is served daily between 5:30pm and 7:30pm in the Vistas Dining Room, the top floor of the Sally Borden Building.

Combinatorial characterizations of canonical and interpolation pairs have been found for Frege system for every constant depth. The most interesting case is the canonical pair of Resolution which is equivalent to the interpolation pair of depth 1 Frege system. The first (formulation) is connected with weak automatibility of Resolution, the second with interpolation for the weakest fragment of Frege systems for which we do not have feasible interpolation. We will show several ways how these pairs can be presented and connections with monotone interpolation.

We introduce the binary value principle which is a simple subset-sum instance expressing that a natural number written in binary cannot be negative, relating it to central problems in proof and algebraic complexity. We prove conditional superpolynomial lower bounds on the Ideal Proof System (IPS) refutation size of this instance, based on a well-known hypothesis by Shub and Smale about the hardness of computing factorials, where IPS is the strong algebraic proof system introduced by Grochow and Pitassi (2018). Conversely, we show that short IPS refutations of this instance bridge the gap between sufficiently strong algebraic and semi-algebraic proof systems. Our results extend to full-fledged IPS the paradigm introduced in Forbes et al. (2016), whereby lower bounds against subsystems of IPS were obtained using restricted algebraic circuit lower bounds, and demonstrate that the binary value principle captures the advantage of semi-algebraic over algebraic reasoning, for sufficiently strong systems. Specifically, we show the following: *Conditional IPS lower bounds:* The Shub-Smale hypothesis (1995) implies a superpolynomial lower bound on the size of IPS refutations of the binary value principle over the rationals defined as the unsatisfiable linear equation $\sum_{i=1}^{n} 2^{i-1}x_i = -1$, for boolean $x_i$'s. Further, the related $\tau$-conjecture (1995) implies a superpolynomial lower bound on the size of IPS refutations of a variant of the binary value principle over the ring of rational functions. No prior conditional lower bounds were known for IPS or for apparently much weaker propositional proof systems such as Frege. *Algebraic vs. semi-algebraic proofs:* Admitting short refutations of the binary value principle is necessary for any algebraic proof system to fully simulate any known semi-algebraic proof system, and for strong enough algebraic proof systems it is also sufficient. In particular, we introduce a very strong proof system that simulates all known semi-algebraic proof systems (and most other known concrete propositional proof systems), under the name Cone Proof System (CPS), as a semi-algebraic analogue of the ideal proof system: CPS establishes the unsatisfiability of collections of polynomial equalities and inequalities over the reals, by representing sum-of-squares proofs (and extensions) as algebraic circuits. We prove that IPS is polynomially equivalent to CPS iff IPS admits polynomial-size refutations of the binary value principle (for the language of systems of equations that have no 0/1-solutions), over both $\mathbb{Z}$ and $\mathbb{Q}$. Joint work with Yaroslav Alekseev and Dima Grigoriev.

Proving that there are problems in $P^{NP}$ that require boolean circuits of super-linear size is a major frontier in complexity theory. While such lower bounds are known for larger complexity classes, existing results only show that the corresponding problems are hard on infinitely many input lengths. For instance, proving almost-everywhere circuit lower bounds is open even for problems in MAEXP. Giving the notorious difficulty of proving lower bounds that hold for all large input lengths, we ask the following question: Can we show that a large set of techniques cannot prove that NP is easy infinitely often? Motivated by this and related questions about the interaction between mathematical proofs and computations, we investigate circuit complexity from the perspective of logic. Among other results, we prove that for any parameter $k > 1$ it is consistent with theory T that computational class $C \not\subseteq i.o.SIZE(n^k)$, where $(T,C)$ is one of the pairs: $T=T12$ and $C=P^{NP}$, $T=S12$ and $C=NP$, $T=PV$ and $C=P$. In other words, these theories cannot establish infinitely often circuit upper bounds for the corresponding problems. This is of interest because the weaker theory PV already formalizes sophisticated arguments, such as a proof of the PCP Theorem (Pich, 2015). These consistency statements are unconditional and improve on earlier theorems of Krajicek and Oliveira (2017) and Bydzovsky and Muller (2018) on the consistency of lower bounds with PV. https://arxiv.org/abs/1905.12935

We formalize and study the question of whether there are inherent difficulties to showing lower bounds on propositional proof complexity. We establish the following unconditional result: Propositional proof systems cannot efficiently show that truth tables of random Boolean functions lack polynomial size nonuniform proofs of hardness. Assuming a conjecture of Rudich, propositional proof systems also cannot efficiently show that random k-CNFs of linear density lack polynomial size non-uniform proofs of unsatisfiability. Since the statements in question assert the average-case hardness of standard NP problems (MCSP and 3-SAT respectively) against co-nondeterministic circuits for natural distributions, one interpretation of our result is that propositional proof systems are inherently incapable of efficiently proving strong complexity lower bounds in our formalization. Another interpretation is that an analogue of the Razborov-Rudich ‘natural proofs’ barrier holds in proof complexity: under reasonable hardness assumptions, there are natural distributions on hard tautologies for which it is infeasible to show proof complexity lower bounds for strong enough proof systems. For the specific case of the Extended Frege (EF) propositional proof system, we show that at least one of the following cases holds: (1) EF has no efficient proofs of superpolynomial circuit lower bound tautologies for any Boolean function or (2) There is an explicit family of tautologies of each length such that under reasonable hardness assumptions, most tautologies are hard but no propositional proof system can efficiently establish hardness for most tautologies in the family. Thus, under reasonable hardness assumptions, either the Circuit Lower Bounds program toward complexity separations cannot be implemented in EF, or there are inherent obstacles to implementing the Cook-Reckhow program for EF. This is a joint work with Rahul Santhanam.

This talk will start with an overview of the relatively young field of QBF proof complexity, explaining QBF proof systems (including QBF resolution) and an assessment of which lower bound techniques are available for QBF proof systems. In the main part of the talk, I will explain hardness characterisations for QBF proof systems in terms of circuit complexity, yielding very direct connections between circuit lower bounds and QBF proof system lower bounds.

The ordering principle, which says that if there is an ordering on n elements then one of them must be less than all of the others, is an important example in proof complexity. The ordering principle is important because while it has a short resolution proof, any resolution proof must have width $\Omega(n)$ and any polynomial calculus proof must have degree $\Omega(n)$. Thus, with some adjustments, the ordering principle gives a tight example for the size/width tradeoffs of Ben-Sasson and Wigderson for resolution and the size/degree tradeoffs of Impagliazzo, Pudlak, and Sgall for polynomial calculus (as it requires $n^2$ variables to express the ordering principle). A natural question is whether the sum of squares hierarchy also requires degree $\Omega(n)$ to prove the ordering principle or if sum of squares can do better. As it turns out, sum of squares can do better. In this talk, I will describe how the sum of squares hierarchy can prove the ordering principle using degree roughly $n^(1/2)$. Time permitting, I will also describe ideas for a sum of squares lower bound.

We compare the complexity of refuting the binary and unary versions of large classes of combinatorial principles in Resolution and its extension Res(s) to s-DNFs. In particular we prove size lower bonds in Res(s) for the binary versions of the weak pigeonhole principle and the k-clique principle. The talk is based on a joint work with Stefan Dantchev and Barnaby Martin.

A major open problem in proof complexity is to prove super-polynomial lower bounds for $AC^0[p]$-Frege proofs. This system is the analog of $AC^0[p]$, the class of bounded depth circuits with prime modular counting gates. Despite strong lower bounds for this class dating back thirty years (Razborov, '86 and Smolensky, '87), there are no significant lower bounds for $AC^0[p]$-Frege. Significant and extensive *degree* lower bounds have been obtained for a variety of subsystems of $AC^0[p]$-Frege, including Nullstellensatz (Beame et. al. '94), Polynomial Calculus (Clegg et. al. '96), and SOS (Griegoriev and Vorobjov, '01). However to date there has been no progress on $AC^0[p]$-Frege lower bounds. In this paper we study constant-depth extensions of the Polynomial Calculus introduced by Griegoriev and Hirsch, '03. We show that these extensions are much more powerful than was previously known. Our main result is that small depth Polynomial Calculus (over a sufficiently large field) can polynomially simulate all of the well-studied semialgebraic proof systems: Cutting Planes, Sherali-Adams and Sum-of-Squares, and they can also quasi-polynomially simulate $AC^0[p]$-Frege as well as $TC^0$-Frege. Thus, proving strong lower bounds for $AC^0[p]$-Frege would seem to require proving lower bounds for systems as strong as $TC^0$-Frege.

A growing number of results in proof complexity rely on so-called "lifting" techniques (also called "hardness escalation"), which are inspired from communication complexity. In the context of proof complexity, the basic idea of lifting is simple: in order to prove lower bounds in a proof system that is "complex", start with a formula F that is hard for a "simple" proof system, and make the formula F harder by replacing each variable in F with some inner function that is hard to represent in the "complex" system. Often, we are able to show that the best proof for the composed formula in the complex proof system is to simulate the proof in the simple system --- thus, this reduces the lower bound problem from the complex proof system to proving lower bounds in the simple system, which is often much easier. In this survey talk, we will give an introduction to these techniques, survey some of the applications, and delineate when the techniques can be applied. No prior background in lifting techniques or communication complexity will be necessary.

We show that it is NP-hard to distinguish formulas that have Resolution refutations of almost linear length from formulas that do not even have weakly exponentially long ones. It follows from this that Resolution is not automatable in polynomial time unless P = NP, or in weakly exponential time unless ETH fails. In the talk I will try to explain the process of discovery that led us to the result.

In a breathtaking breakthrough, Atserias and Muller (FOCS'19, Best Paper) settled the complexity of finding short proofs in Resolution, the most basic propositional proof system. Namely, given an unsatisfiable CNF formula F, they showed it is NP-hard to find a Resolution refutation of F in time polynomial in the length of the shortest such refutation. In this talk, we present a simple proof of the Atserias--Muller theorem. The new proof generalises better: We obtain analogous hardness results for Nullstellensatz, Polynomial Calculus, Sherali--Adams, and (with more work) Cutting Planes. An open problem is to include Sum-of-Squares in this list. Based on joint works with Sajin Koroth, Ian Mertz, Jakob Nordström, Toniann Pitassi, Susanna de Rezende, Robert Robere, Dmitry Sokolov.

A refutation statement for a proof system $P$, a CNF $F$, and an integer $s$, is a statement that $F$ has a $P$-refutation of length $s$. We discuss why resolution requires exponential size to refute resolution refutation statements for any unsatisfiable $F$ (and for any $s$ greater than a small polynomial in the size of $F$). We look at some consequences.

There are unsatisfiable $k$-CNF formulas in n variables such that each regular resolution refutation of those has size at least $2^{n(1 - c_k)}$ where where $c_k$ goes to 0 as $k$ goes to infinity. The problem of finding $k$-CNF formulas for which we can prove such strong size lower bounds in resolution (or stronger systems) is open. A lower bound of this form for resolution would imply that CDCL solvers cannot disprove the Strong Exponential Time Hypothesis. In this talk we give a simple proof of the result for regular resolution with the idea in mind to attack the problem for general resolution (or stronger systems). (Talk based on joint works with Navid Talebanfard)

We show a new connection between the space measure in tree-like resolution and the reversible pebble game in graphs. Using this connection we provide several formula classes for which there is a logarithmic factor separation between the space complexity measure in tree-like and general resolution. We show that these separations are almost optimal by proving upper bounds for tree-like resolution space in terms of general resolution clause and variable space. In particular we show that for any formula $F$, its tree-like resolution is upper bounded by space$(\pi)\big(\hbox{\rm time}(\pi)\big)$ where $\pi$ is any general resolution refutation of $F$. This holds considering as space$(\pi)$ the clause space of the refutation as well as considering its variable space. For the concrete case of Tseitin formulas we are able to improve this bound to the optimal bound space$(\pi)\log n$, where $n$ is the number of vertices of the corresponding graph.

We show that the size of any regular resolution refutation of Tseitin formula $T(G,c)$ based on a graph $G$ is at least $2^{\Omega(tw(G))/log n}$, where $n$ is the number of vertices in $G$ and $tw(G)$ is the treewidth of $G$. For constant degree graphs there is known upper bound $2^{O(tw(G))}$ [Alekhnovich, Razborov, FOCS-2002], so our lower bound is tight up to a logarithmic factor in the exponent. In order to prove this result we show that any regular resolution proof of Tseitin formula $T(G,c)$ of size $S$ can be transformed to a read-once branching program of size $S^{log n}$ computing a satisfiable Tseitin formula $T(G,c')$. Then we show that any read-once branching program computing satisfiable Tseitin formula $T(G,c')$ has size at least $2^{\Omega(tw(G))}$; the latter improves the result of [Glinskih, Itsykson, CSR-2019] and together with the transformation implies the main result. Talk is based on joint work with Artur Riazanov, Danil Sagunov and Petr Smirnov.

For the average hardness of $k$-clique CNF, we have the $2^k$-type lower bound for general resolution, and the ideal $n^k$-type for regular resolution. What's difficult in getting the ideal lbd for general resolution? Is regularity really important here? We examine known separations of general vs. regular, and show that they actually all separate a middle model (called ``a-irregular'') from regular. It also turns out, $k$-Clique goes past (ie., is hard for) this model. Thus the difficulty comes from, not surprisingly, those ``very irregular'' proofs.

Despite the fact that the resolution proof system has been extensively studied for decades, a full understanding of even some quite basic formulas has remained out of reach. One example of this are the so-called weak pigeonhole principle (PHP) formulas claiming that m pigeons can be mapped one-to-one to n holes for $m >> n$. In a breakthrough result, Raz (2001) established exponential lower bounds for such formulas, which Razborov further strengthened and generalized by developing his so-called pseudo-width method. In this work, we show how to extend the pseudo-witdth method further to obtain lower bounds for graph PHP formulas, where pigeons can only fly to holes as specified by sparse bipartite graphs, thus answering an open question by Razborov. This seminar is based on joint work with Susanna F. de Rezende, Jakob Nordström and Dmitry Sokolov.

Lifting theorems in complexity theory are a method of transferring lower bounds in a weak computational model into lower bounds for a more powerful computational model, via function composition. There has been an explosion of lifting theorems in the last ten years, essentially reducing communication lower bounds to query complexity lower bounds. These theorems only hold for composition with very specific ``gadgets'' such as indexing and inner product. In this talk, we will present a generalization of the theorem lifting Nullstellensatz degree to monotone span program size by Pitassi and Robere (2018) so that it works for any gadget with high enough rank, in particular, for useful gadgets such as equality and greater-than. We will then explain how to apply our generalized theorem to solve two open problems: *We present the first result that demonstrates a separation in proof power for cutting planes with unbounded versus polynomially bounded coefficients. Specifically, we exhibit CNF formulas that can be refuted in quadratic length and constant line space in cutting planes with unbounded coefficients, but for which there are no refutations in subexponential length and subpolynomial line space if coefficients are restricted to be of polynomial magnitude. * We give the first explicit separation between monotone Boolean formulas and monotone real formulas. Namely, we give an explicit family of functions that can be computed with monotone real formulas of nearly linear size but require monotone Boolean formulas of exponential size. Previously only a non-explicit separation was known. This talk is based on joint work with Or Meir, Jakob Nordström, Toniann Pitassi, Robert Robere, and Marc Vinyals.

We prove that Tseitin formulas $Ts(G)$ for an undirected graph $G$, requires proofs of size $2^{tw(G)^{\Omega(1/d)}}$ in depth d-Frege systems for $d<{K \log n}/{\log \log n}$, where $tw(G)$ is the treewidth of $G$ and $K$ a constant. This extends H\r{a}stad recent lower bound for the grid graph to any graph. Furthermore, we prove tightness of our bound up to a multiplicative constant in the top exponent. The talk is based on a joint work with Dmitry Itsykson, Artur Ryazonov, Anastasia Sofronova.

This paper studies propositional proof systems in which lines are sequents of decision trees or branching programs - deterministic and nondeterministic. The systems LDT and LNDT are propositional proof systems in which lines represent deterministic or non-deterministic decision trees. Branching programs are modeled as decision dags. Adding extension to LDT and LNDT gives systems eLDT and eLNDT in which lines represent deterministic and non-deterministic branching programs, respectively. Deterministic and non-deterministic branching programs correspond to log-space (L) and nondeterministic log-space (NL). Thus the systems eLDT and eLNDT are propositional proof systems that reason with (nonuniform) L and NL properties. The main results of the paper are simulation and non-simulation results for tree-like and dag-like proofs in the systems LDT, LNDT, eLDT, and eLNDT. These systems are also compared with Frege systems, constantdepth Frege systems and extended Frege systems. This talk is based on work published in the proceedings of CSL 2020.

Motivated by interpolation theorem for Lovasz-Shrijver proof system, I discuss a model of monotone computation based on linear programming. To prove super polynomial lower bound for this model is an open problem; I give at least some equivalent formulations via non-negative matrix rank.

The CDCL algorithm, which is nowadays the top-performing algorithm to solve SAT in practice, is polynomially equivalent to resolution when we view it as a proof system, that is we replace some of its heuristics by nondeterministic choices. In this talk we show that this is no longer true if we leave the heuristics in place; more precisely we build a family of formulas that have resolution proofs of polynomial size but require exponential time to decide in CDCL with a class of variable decision heuristics that includes the most common heuristics such as VSIDS.

5-day workshop participants are welcome to use BIRS facilities (BIRS Coffee Lounge, TCPL and Reading Room) until 3 pm on Friday, although participants are still required to checkout of the guest rooms by 12 noon.