Search

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. [ABSTRACT FROM AUTHOR]

We introduce a new and natural algebraic proof system, whose complexity measure is essentially the algebraic circuit size of Nullstellensatz certificates. This enables us to exhibit close connections between effective Nullstellensatzë, proof complexity, and (algebraic) circuit complexity. In particular, we show that any super-polynomial lower bound on any Boolean tautology in our proof system implies that the permanent does not have polynomial-size algebraic circuits (VNP ≠ VP). We also show that super-polynomial lower bounds on the number of lines in Polynomial Calculus proofs imply the Permanent versus Determinant Conjecture. Note that there was no proof system prior to ours for which lower bounds on an arbitrary tautology implied any complexity class lower bound. Our proof system helps clarify the relationships between previous algebraic proof systems. In doing so, we highlight the importance of polynomial identity testing (PIT) in proof complexity. In particular, we use PIT to illuminate AC0[p]-Frege lower bounds, which have been open for nearly 30 years, with no satisfactory explanation as to their apparent difficulty. Finally, we explain the obstacles that must be overcome in any attempt to extend techniques from algebraic circuit complexity to prove lower bounds in proof complexity. Using the algebraic structure of our proof system, we propose a novel route to such lower bounds. Although such lower bounds remain elusive, this proposal should be contrasted with the difficulty of extending AC0[p] circuit lower bounds to AC0[p]-Frege lower bounds. [ABSTRACT FROM AUTHOR]

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 &#954:-CNFs (κ ≥ 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. [ABSTRACT FROM AUTHOR]

Resolution over linear equations is a natural extension of the popular resolution refutation system, augmented with the ability to carry out basic counting. Denoted Res (lin R) , this refutation system operates with disjunctions of linear equations with Boolean variables over a ring R, to refute unsatisfiable sets of such disjunctions. Beginning in the work of Raz & Tzameret (2008), through the work of Itsykson & Sokolov (2020) which focused on tree-like lower bounds, this refutation system was shown to be fairly strong. Subsequent work (cf. Garlik & Kołodziejczyk 2018; Itsykson & Sokolov 2020; Krajícek 2017; Krajícek & Oliveira 2018) made it evident that establishing lower bounds against general Res (lin R) refutations is a challenging and interesting task since the system captures a ``minimal'' extension of resolution with counting gates for which no super-polynomial lower bounds are known to date. We provide the first super-polynomial size lower bounds against general (dag-like) resolution over linear equations refutations in the large characteristic regime. In particular, we prove that the subset-sum principle 1 + ∑ i = 1 n 2 i x i = 0 requires refutations of exponential size over Q . We use a novel lower bound technique: We show that under certain conditions every refutation of a subset-sum instance f = 0 must pass through a fat clause consisting of the equation f = α for every α in the image of f under Boolean assignments, or can be efficiently reduced to a proof containing such a clause. We then modify this approach to prove exponential lower bounds against tree-like refutations of any subset-sum instance that depends on n variables, hence also separating tree-like from dag-like refutations over the rationals. We then turn to the finite fields regime, showing that the work of Itsykson & Sokolov (2020), where tree-like lower bounds over F 2 were obtained, can be carried over and extended to every finite field. We establish new lower bounds and separations as follows: (i) For every pair of distinct primes p , q , there exist CNF formulas with short tree-like refutations in Res (lin F p) that require exponential-size tree-like Res (lin F q) refutations; (ii) random k-CNF formulas require exponential-size tree-like Res (lin F p) refutations, for every prime p and constant k; and (iii) exponential-size lower bounds for tree-like Res (lin F) refutations of the pigeonhole principle, for every field F . [ABSTRACT FROM AUTHOR]

Polynomial complexity is an algebraic proof system inspired by Gröbner bases which was introduced by Clegg, Edmonds and Impagliazzo. Alekhnovich and Razborov devised a method for proving degree lower bounds for polynomial calculus. We present an alternative account of their method, which also encompasses a generalization due to Galesi and Lauria. [ABSTRACT FROM AUTHOR]

Semi-algebraic proof systems such as sum-of-squares (SoS) have attracted a lot of attention due to their relation to approximation algorithms: constant degree semi-algebraic proofs lead to conjecturally optimal polynomial-time approximation algorithms for important NP -hard optimization problems. Motivated by the need to allow a more streamlined and uniform framework for working with SoS proofs than the restrictive propositional level, we initiate a systematic first-order logical investigation into the kinds of reasoning possible in algebraic and semi-algebraic proof systems. Specifically, we develop first-order theories that capture in a precise manner constant degree algebraic and semi-algebraic proof systems: every statement of a certain form that is provable in our theories translates into a family of constant degree polynomial calculus or SoS refutations, respectively; and using a reflection principle, the converse also holds. This places algebraic and semi-algebraic proof systems in the established framework of bounded arithmetic, while providing theories corresponding to systems that vary quite substantially from the usual propositional-logic ones. We give examples of how our semi-algebraic theory proves statements such as the pigeonhole principle, we provide a separation between algebraic and semi-algebraic theories, and we describe initial attempts to go beyond these theories by introducing extensions that use the inequality symbol, identifying along the way which extensions lead outside the scope of constant degree SoS. Moreover, we prove new results for propositional proofs, and specifically extend Berkholz's dynamic-by-static simulation of polynomial calculus (PC) by SoS to PC with the radical rule. [ABSTRACT FROM AUTHOR]

We investigate the space complexity of refuting 3-CNFs in Resolution and algebraic systems. We prove that every Polynomial Calculus with Resolution refutation of a random 3-CNF φ in n variables requires, with high probability, Ω ( n ) distinct monomials to be kept simultaneously in memory. The same construction also proves that every Resolution refutation of φ requires, with high probability, Ω ( n ) clauses each of width Ω ( n ) to be kept at the same time in memory. This gives a Ω ( n 2 ) lower bound for the total space needed in Resolution to refute φ . These results are best possible (up to a constant factor) and answer questions about space complexity of 3-CNFs. The main technical innovation is a variant of Hall's Lemma . We show that in bipartite graphs with bipartition ( L , R ) and left-degree at most 3, L can be covered by certain families of disjoint paths, called VW - matchings , provided that L expands in R by a factor of ( 2 − ϵ ) , for ϵ < 1 5 . [ABSTRACT FROM AUTHOR]

We prove that there are 3-CNF formulas over n variables that can be refuted in resolution in width ω but require resolution proofs of size nΩ(ω). This shows that the simple counting argument that any formula refutable in width ω must have a proof in size nΩ(ω) is essentially tight. Moreover, our lower bound generalizes to polynomial calculus resolution and Sherali-Adams, implying that the corresponding size upper bounds in terms of degree and rank are tight as well. The lower bound does not extend all the way to Lasserre, however, since we show that there the formulas we study have proofs of constant rank and size polynomial in both n and ω. [ABSTRACT FROM AUTHOR]

During the last 10 to 15 years, an active line of research in proof complexity has been to study space complexity and time-space trade-offs for proofs. Besides being a natural complexity measure of intrinsic interest, space is also an important concern in SAT solving, and so research has mostly focused on weak systems that are used by SAT solvers. There has been a relatively long sequence of papers on space in resolution, which is now reasonably well-understood from this point of view. For other proof systems of interest, however, such as polynomial calculus or cutting planes, progress has been more limited. Essentially nothing has been known about space complexity in cutting planes, and for polynomial calculus the only lower bound has been for conjunctive normal form (CNF) formulas of unbounded width in [Alekhnovich et al., SIAM J. Comput., 31 (2002), pp. 1184-1211], where the space lower bound is smaller than the initial width of the clauses in the formulas. Thus, in particular, it has been consistent with current knowledge that polynomial calculus could be able to refute any k-CNF formula in constant space. In this paper, we prove several new results on space in polynomial calculus (PC) and in the extended proof system polynomial calculus resolution (PCR) studied by Alekhnovich et al.: (1) We prove an ω(n) space lower bound in PC for the canonical 3-CNF version of the pigeonhole principle formulas PHPnm with m pigeons and n holes, and show that this is tight. (2) For PCR, we prove an ω(n) space lower bound for a bitwise encoding of the functional pigeonhole principle. These formulas have width O(log n), and hence this is an exponential improvement over Alekhnovich et al. measured in the width of the formulas. (3) We then present another encoding of the pigeonhole principle that has constant width, and prove an ω(n) space lower bound in PCR for these formulas as well. (4) Finally, we prove that any k-CNF formula can be refuted in PC in simultaneous exponential size and linear space (which holds for resolution and thus for PCR, but was not obviously the case for PC). We also characterize a natural class of CNF formulas for which the space complexity in resolution and PCR does not change when the formula is transformed into 3-CNF in the canonical way, something that we believe can be useful when proving PCR space lower bounds for other well-studied formula families in proof complexity. [ABSTRACT FROM AUTHOR]

In 2003, Atserias and Dalmau resolved a major open question about the resolution proof system by establishing that the space complexity of a Conjunctive Normal Form (CNF) formula is always an upper bound on the width needed to refute the formula. Their proof is beautiful but uses a nonconstructive argument based on Ehrenfeucht-Frös sè games. We give an alternative, more explicit, proof that works by simple syntactic manipulations of resolution refutations. As a by-product, we develop a "black-box" technique for proving space lower bounds via a "static" complexitymeasure that works against any resolution refutation--previous techniques have been inherently adaptive. We conclude by showing that the related question for polynomial calculus (i.e., whether space is an upper bound on degree) seems unlikely to be resolvable by similarmethods. [ABSTRACT FROM AUTHOR]

Pebble games were extensively studied in the 1970s and 1980s in a number of different contexts. The last decade has seen a revival of interest in pebble games coming from the field of proof complexity. Pebbling has proven to be a useful tool for studying resolution-based proof systems when comparing the strength of different subsystems, showing bounds on proof space, and establishing size-space trade-offs. This is a survey of research in proof complexity drawing on results and tools from pebbling, with a focus on proof space lower bounds and trade-offs between proof size and proof space. [ABSTRACT FROM AUTHOR]

Abstract: We study possible formulations of algebraic propositional proof systems operating with noncommutative formulas. We observe that a simple formulation gives rise to systems at least as strong as Frege, yielding a semantic way to define a Cook–Reckhow (i.e., polynomially verifiable) algebraic analog of Frege proofs, different from that given in Buss et al. (1997) and Grigoriev and Hirsch (2003). We then turn to an apparently weaker system, namely, polynomial calculus (PC) where polynomials are written as ordered formulas (PC over ordered formulas, for short). Given some fixed linear order on variables, an arithmetic formula is ordered if for each of its product gates the left subformula contains only variables that are less-than or equal, according to the linear order, than the variables in the right subformula of the gate. We show that PC over ordered formulas (when the base field is of zero characteristic) is strictly stronger than resolution, polynomial calculus and polynomial calculus with resolution (PCR), and admits polynomial-size refutations for the pigeonhole principle and Tseitinʼs formulas. We conclude by proposing an approach for establishing lower bounds on PC over ordered formulas proofs, and related systems, based on properties of lower bounds on noncommutative formulas (Nisan, 1991). The motivation behind this work is developing techniques incorporating rank arguments (similar to those used in arithmetic circuit complexity) for establishing lower bounds on propositional proofs. [Copyright &y& Elsevier]

We prove linear lower bounds on the Polynomial Calculus (PC) refutation-degree of random CNF whenever the underlying field has characteristic greater than 2. Our proof follows by showing the PC refutation-degree of a unsatisfiable system of linear equations modulo 2 is equivalent to its Gaussian width, a concept defined by the late Mikhail Alekhnovich. The equivalence of refutation-degree and Gaussian width which is the main contribution of this paper, allows us to also simplify the refutation-degree lower bounds of Buss et al. (2001) and additionally prove non-trivial upper bounds on the resolution and PC complexity of refuting unsatisfiable systems of linear equations. [ABSTRACT FROM AUTHOR]

We prove that Polynomial Calculus and Polynomial Calculus with Resolution are not automatizable, unless W[ P]-hard problems are fixed parameter tractable by one-side error randomized algorithms. This extends to Polynomial Calculus the analogous result obtained for Resolution by Alekhnovich and Razborov (SIAM J. Comput. 38(4):1347–1363, ). [ABSTRACT FROM AUTHOR]

We call a pseudorandom generator Gn (0, 1)n → (0, 1)m hard for a Propositional proof system P if P cannot efficiently prove the (properly encoded) statement Gn(x1, · , xn) ≠ b for any string b &epsiv; (0, 1)n We consider a variety of "combinatorial" pseudorandom generators inspired by the Nisan-Wigderson generator on the one hand, and by the construction of Tseitin tautologies on the other. We prove that under certain circumstances these generators are hard for such proof systems as resolution, polynomial calculus, and polynomial calculus with resolution (PCR). [ABSTRACT FROM AUTHOR]

Over a fixed finite field ${\bf F}_p$, families of polynomial equations $f_i(x_1, \dots, x_{n_N}) = 0$ for $i = 1, \dots, k_N$, that are uniformly determined by a parameter $N$, are considered. The notion of a uniform family is defined in terms of first-order logic. A notion of an abstract Euler characteristic is used to give sense to a statement that the system has a solution for infinite $N$, and a statement linking the solvability of a linear system for infinite $N$ with its solvability for finite $N$ is proved. This characterisation is used to formulate a criterion yielding degree lower bounds for various ideal membership proof systems (for example, Nullstellensatz and the polynomial calculus). Further, several results about Euler structures (structures with an abstract Euler characteristic) are proved, and the case of fields, in particular, is investigated more closely. 1991 Mathematics Subject Classification: primary 03F20, 12L12, 15A06; secondary 03C99, 12E12, 68Q15, 13L05. [ABSTRACT FROM AUTHOR]

We show that polynomial calculus proofs (sometimes also called Groebner proofs) of the pigeonhole principle $ P H P^m_n $ must have degree at least $ (n/2)+1 $ over any field. This is the first non-trivial lower bound on the degree of polynomial calculus proofs obtained without using unproved complexity assumptions. We also show that for some modifications of $ P H P^m_n $ , expressible by polynomials of at most logarithmic degree, our bound can be improved to linear in the number of variables. Finally, we show that for any Boolean function $ f_n $ in n variables, every polynomial calculus proof of the statement “ $ f_n $ cannot be computed by any circuit of size t,” must have degree $ \Omega(t/n) $ . Loosely speaking, this means that low degree polynomial calculus proofs do not prove $ {\bf NP}\not\subseteq {\bf P}/poly $ . [ABSTRACT FROM AUTHOR]