We compare the strength of the algebraic proof systems Sherali-Adams (SA) and Nullstellensatz (NS) with Frege-style proof systems. Unlike bounded-depth Frege, SA has polynomial-size proofs of the pigeonhole principle (PHP). A natural question is whether adding PHP to bounded-depth Frege is enough to simulate SA. We show that SA, with unary integer coefficients, lies strictly between tree-like depth-1 Frege + PHP and tree-like Resolution. We introduce a levelled version of PHP (L PHP) and we show that SA with integer coefficients lies strictly between tree-like depth-1 Frege + L PHP and Resolution. Analogous results are shown for NS using the bijective (i.e. onto and functional) pigeonhole principle and a leveled version of it.

MaxSAT is the problem of finding an assignment satisfying the maximum number of clauses in a CNF formula. We consider a natural generalization of this problem to generic sets of polynomials and propose a weighted version of Polynomial Calculus to address this problem. Weighted Polynomial Calculus is a natural generalization of the systems MaxSAT-Resolution and weighted Resolution. Unlike such systems, weighted Polynomial Calculus manipulates polynomials with coefficients in a finite field and either weights in N or Z. We show the soundness and completeness of weighted Polynomial Calculus via an algorithmic procedure. Weighted Polynomial Calculus, with weights in N and coefficients in F2, is able to prove efficiently that Tseitin formulas on a connected graph are minimally unsatisfiable. Using weights in Z, it also proves efficiently that the Pigeonhole Principle is minimally unsatisfiable.

In recent years there has been an increasing interest in studying proof systems stronger than Resolution, with the aim of building more efficient SAT solvers based on them. In defining these proof systems, we try to find a balance between the power of the proof system (the size of the proofs required to refute a formula) and the difficulty of finding the proofs. In this paper we consider the proof systems circular Resolution, Sherali-Adams, Nullstellensatz and Weighted Resolution and we study their relative power from a theoretical perspective. We prove that circular Resolution, Sherali-Adams and Weighted Resolution are polynomially equivalent proof systems. We also prove that Nullstellensatz is polynomially equivalent to a restricted version of Weighted Resolution. The equivalences carry on also for versions of the systems where the coefficients/weights are expressed in unary. The practical interest in these systems comes from the fact that they admit efficient algorithms to find proofs in case these have small width/degree.

Abstract We introduce a novel take on sum-of-squares that is able to reason with complex numbers and still make use of polynomial inequalities. This proof system might be of independent interest since it allows to represent multivalued domains both with Boolean and Fourier encoding. We show degree and size lower bounds in this system for a natural generalization of knapsack: the vanishing sums of roots of unity. These lower bounds naturally apply to polynomial calculus as-well.

We characterize the strength of the algebraic proof systems Sherali-Adams () and Nullstellensatz () in terms of Frege-style proof systems. Unlike bounded-depth Frege, has polynomial-size proofs of the pigeonhole principle (). A natural question is whether adding to bounded-depth Frege is enough to simulate .

We prove that for k ≪ 4√ n regular resolution requires length n Ω( k ) to establish that an Erdős–Rényi graph with appropriately chosen edge density does not contain a k -clique. This lower bound is optimal up to the multiplicative constant in the exponent and also implies unconditional n Ω( k ) lower bounds on running time for several state-of-the-art algorithms for finding maximum cliques in graphs.

We define and investigate Frege systems for quantified Boolean formulas (QBF). For these new proof systems, we develop a lower bound technique that directly lifts circuit lower bounds for a circuit class C to the QBF Frege system operating with lines from C . Such a direct transfer from circuit to proof complexity lower bounds has often been postulated for propositional systems but had not been formally established in such generality for any proof systems prior to this work. This leads to strong lower bounds for restricted versions of QBF Frege, in particular an exponential lower bound for QBF Frege systems operating with AC 0 [ p ] circuits. In contrast, any non-trivial lower bound for propositional AC 0 [ p ]-Frege constitutes a major open problem. Improving these lower bounds to unrestricted QBF Frege tightly corresponds to the major problems in circuit complexity and propositional proof complexity. In particular, proving a lower bound for QBF Frege systems operating with arbitrary P/poly circuits is equivalent to either showing a lower bound for P/poly or for propositional extended Frege (which operates with P/poly circuits). We also compare our new QBF Frege systems to standard sequent calculi for QBF and establish a correspondence to intuitionistic bounded arithmetic.

We prove that for k ≪ n1/4 regular resolution requires length nΩ(k) to establish that an Erdos-Renyi graph with appropriately chosen edge density does not contain a k-clique. This lower bound is optimal up to the multiplicative constant in the exponent, and also implies unconditional nΩ(k) lower bounds on running time for several state-of-the-art algorithms for finding maximum cliques in graphs.

Given an unsatisfiable k-CNF formula phi we consider two complexity measures in Resolution: width and total space. The width is the minimal W such that there exists a Resolution refutation of phi with clauses of at most W literals. The total space is the minimal size T of a memory used to write down a Resolution refutation of phi where the size of the memory is measured as the total number of literals it can contain. We prove that T = Omega((W - k)^2).

A general and long-standing belief in the proof complexity community asserts that there is a close connection between progress in lower bounds for Boolean circuits and progress in proof size lower bounds for strong propositional proof systems. Although there are famous examples where a transfer from ideas and techniques from circuit complexity to proof complexity has been effective, a formal connection between the two areas has never been established so far. Here we provide such a formal relation between lower bounds for circuit classes and lower bounds for Frege systems for quantified Boolean formulas (QBF).

We show quadratic lower bounds on the total space used in resolution refutations of random $k$-CNFs over $n$ variables and of the graph pigeonhole principle and the bit pigeonhole principle for $n$ holes. This answers the open problem of whether there are families of $k$-CNF formulas of polynomial size that require quadratic total space in resolution. The results follow from a more general theorem showing that, for formulas satisfying certain conditions, in every resolution refutation there is a memory configuration containing many clauses of large width.

We consider a restriction of the Resolution proof system in which at most a fixed number of variables can be resolved more than once along each refutation path. This system lies between regular Resolution, in which no variable can be resolved more than once along any path, and general Resolution where there is no restriction on the number of such variables. We show that when the number of re-resolved variables is not too large, this proof system is consistent with the Strong Exponential Time Hypothesis (SETH). More precisely for large n and k we show that there are unsatisfiable k-CNF formulas which require Resolution refutations of size 2^{(1 - epsilon_k)n}, where n is the number of variables and epsilon_k=~O(k^{-1/5}), whenever in each refutation path we only allow at most ~O(k^{-1/5})n variables to be resolved multiple times. However, these re-resolved variables along different paths do not need to be the same. Prior to this work, the strongest proof system shown to be consistent with SETH was regular Resolution [Beck and Impagliazzo, STOC'13]. This work strengthens that result and gives a different and conceptually simpler game-theoretic proof for the case of regular Resolution.

Algebraic proof systems, such as Polynomial Calculus (PC) and Polynomial Calculus with Resolution (PCR), refute contradictions using polynomials. Space complexity for such systems measures the number of distinct monomials to be kept in memory while verifying a proof. We introduce a new combinatorial framework for proving space lower bounds in algebraic proof systems. As an immediate application, we obtain the space lower bounds previously provided for PC/PCR [Alekhnovich et al. 2002; Filmus et al. 2012]. More importantly, using our approach in its full potential, we prove Ω( n ) space lower bounds in PC/PCR for random k -CNFs ( k ≥ 4) in n variables, thus solving an open problem posed in Alekhnovich et al. [2002] and Filmus et al. [2012]. Our method also applies to the Graph Pigeonhole Principle, which is a variant of the Pigeonhole Principle defined over a constant (left) degree expander graph.

We show quadratic lower bounds on the total space used in resolution refutations of random k-CNFs over n variables, and of the graph pigeonhole principle and the bit pigeonhole principle for n holes. This answers the long-standing open problem of whether there are families of k-CNF formulas of polynomial size which require quadratic total space in resolution. The results follow from a more general theorem showing that, for formulas satisfying certain conditions, in every resolution refutation there is a memory configuration containing many clauses of large width.

We devise a new combinatorial framework for proving space lower bounds in algebraic proof systems like Polynomial Calculus (Pc) and Polynomial Calculus with Resolution (Pcr). Our method can be thought as a Spoiler-Duplicator game, which is capturing boolean reasoning on polynomials instead that clauses as in the case of Resolution. Hence, for the first time, we move the problem of studying the space complexity for algebraic proof systems in the range of 2-players games, as is the case for Resolution.