Semi-algebraic proof systems such as sum-of-squares (SoS) have attracted a lot of attention recently 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.

It was recently shown by Atserias, Buss and Mueller that the standard complexity-theoretic conjecture NEXP not in P / poly is consistent with the relatively strong bounded arithmetic theory V^0_2, which can prove a substantial part of complexity theory. We observe that their approach can be extended to show that the stronger conjectures NEXP not in EXP / poly and NEXP not in coNEXP are consistent with a stronger theory, which includes every true universal number-sort sentence.

It has become standard that, when a SAT solver decides that a CNF $Γ$ is unsatisfiable, it produces a certificate of unsatisfiability in the form of a refutation of $Γ$ in some proof system. The system typically used is DRAT, which is equivalent to extended resolution (ER) -- for example, until this year DRAT refutations were required in the annual SAT competition. Recently [Bogaerts et al.~2023] introduced a new proof system, associated with the tool VeriPB, which is at least as strong as DRAT and is further able to handle certain symmetry-breaking techniques. We show that this system simulates the proof system $G_1$, which allows limited reasoning with QBFs and forms the first level above ER in a natural hierarchy of proof systems. This hierarchy is not known to be strict, but nevertheless this is evidence that the system of [Bogaerts et al. 2023] is plausibly strictly stronger than ER and DRAT. In the other direction, we show that symmetry-breaking for a single symmetry can be handled inside ER.

Semi-algebraic proof systems such as sum-of-squares (SoS) have attracted a lot of attention recently due to their relation to approximation algorithms [3]: constant degree semi-algebraic proofs lead to conjecturally optimal polynomial-time approximation algorithms for important NP-hard optimization problems (cf. [4]). 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 [7] dynamic-by-static simulation of polynomial calculus (PC) by SoS to PC with the radical rule.

We show that if a k-CNF requires width w to refute in resolution, then it requires space square root of √ω to refute in polynomial calculus, where the space of a polynomial calculus refutation is the number of monomials that must be kept in memory when working through the proof. This is the first analogue, in polynomial calculus, of Atserias and Dalmau's result lower-bounding clause space in resolution by resolution width. As a by-product of our new approach to space lower bounds we give a simple proof of Bonacina's recent result that total space in resolution (the total number of variable occurrences that must be kept in memory) is lower-bounded by the width squared. As corollaries of the main result we obtain some new lower bounds on the PCR space needed to refute specific formulas, as well as partial answers to some open problems about relations between space, size, and degree for polynomial calculus.

We study the random resolution refutation system definedin [Buss et al. 2014]. This attempts to capture the notion of a resolution refutation that may make mistakes but is correct most of the time. By proving the equivalence of several different definitions, we show that this concept is robust. On the other hand, if P does not equal NP, then random resolution cannot be polynomially simulated by any proof system in which correctness of proofs is checkable in polynomial time. We prove several upper and lower bounds on the width and size of random resolution refutations of explicit and random unsatisfiable CNF formulas. Our main result is a separation between polylogarithmic width random resolution and quasipolynomial size resolution, which solves the problem stated in [Buss et al. 2014]. We also prove exponential size lower bounds on random resolution refutations of the pigeonhole principle CNFs, and of a family of CNFs which have polynomial size refutations in constant depth Frege.

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 study the space complexity of the cutting planes proof system, in which the lines in a proof are integral linear inequalities. We measure the space used by a refutation as the number of linear inequalities that need to be kept on a blackboard while verifying it. We show that any unsatisfiable set of linear inequalities has a cutting planes refutation in space five. This is in contrast to the weaker resolution proof system, for which the analogous space measure has been well-studied and many optimal linear lower bounds are known. Motivated by this result we consider a natural restriction of cutting planes, in which all coefficients have size bounded by a constant. We show that there is a CNF which requires super-constant space to refute in this system. The system nevertheless already has an exponential speed-up over resolution with respect to size, and we additionally show that it is stronger than resolution with respect to space, by constructing constant-space cutting planes proofs, with coefficients bounded by two, of the pigeonhole principle. We also consider variable instance space for cutting planes, where we count the number of instances of variables on the blackboard, and total space, where we count the total number of symbols.

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 $\omega(n)$ space lower bound in PC for the canonical 3-CNF version of the pigeonhole principle formulas $PHP_{m}^{n}$ with $m$ pigeons and $n$ holes, and show that this is tight. (2) For PCR, we prove an $\omega(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 $\omega(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.

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.

Abstract We study the long-standing open problem of giving $\forall {\rm{\Sigma }}_1^b$ separations for fragments of bounded arithmetic in the relativized setting. Rather than considering the usual fragments defined by the amount of induction they allow, we study Jeřábek’s theories for approximate counting and their subtheories. We show that the $\forall {\rm{\Sigma }}_1^b$ Herbrandized ordering principle is unprovable in a fragment of bounded arithmetic that includes the injective weak pigeonhole principle for polynomial time functions, and also in a fragment that includes the surjective weak pigeonhole principle for FPNPfunctions. We further give new propositional translations, in terms of random resolution refutations, for the consequences of $T_2^1$ augmented with the surjective weak pigeonhole principle for polynomial time functions.

The ordering principle states that every finite linear order has a least element. We show that, in the relativized setting, the surjective weak pigeonhole principle for polynomial time functions does not prove a Herbrandized version of the ordering principle over T 1 2 . This answers an open question raised in Buss et al. [2012] and completes their program to compare the strength of Jeřábek's bounded arithmetic theory for approximate counting with weakened versions of it.

A propositional proof system is weakly automatizable if there is a polynomial time algorithm that separates satisfiable formulas from formulas that have a short refutation in the system, with respect to a given length bound. We show that if the resolution proof system is weakly automatizable, then parity games can be decided in polynomial time. We give simple proofs that the same holds for depth-1 propositional calculus (where resolution has depth 0) with respect to mean payoff and simple stochastic games. We define a new type of combinatorial game and prove that resolution is weakly automatizable if and only if one can separate, by a set decidable in polynomial time, the games in which the first player has a positional winning strategy from the games in which the second player has a positional winning strategy. Our main technique is to show that a suitable weak bounded arithmetic theory proves that both players in a game cannot simultaneously have a winning strategy, and then to translate this proof into propositional form.

During the last decade, 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 issue in SAT solving. For the polynomial calculus proof system, the only previously known space lower bound is for CNF formulas of unbounded width in [Alekhnovich et al. '02], where the 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 refute any k-CNF formula in constant space. We prove several new results on space in polynomial calculus (PC) and in the extended proof system polynomial calculus resolution (PCR) studied in [Alekhnovich et al. '02]. (1) For PCR, we prove an Ω(n) space lower bound for a bitwise encoding of the functional pigeonhole principle with m pigeons and n holes. These formulas have width O(log n), and hence this is an exponential improvement over [Alekhnovich et al. '02] measured in the width of the formulas. (2) 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. (3) We prove an Ω(n) space lower bound in PC for the canonical 3-CNF version of the pigeonhole principle formulas PHPmnwith m pigeons and n holes, and show that this is tight. (4) 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 known to be 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.

Abstract We show, under the assumption that factoring is hard, that a model of PV exists in which the polynomial hierarchy does not collapse to the linear hierarchy; that a model of exists in which NP is not in the second level of the linear hierarchy; and that a model of exists in which the polynomial hierarchy collapses to the linear hierarchy. Our methods are model-theoretic. We use the assumption about factoring to get a model in which the weak pigeonhole principle fails in a certain way, and then work with this failure to obtain our results. As a corollary of one of the proofs, we also show that in the failure of WPHP (for definable relations) implies that the strict version of PH does not collapse to a finite level.

Abstract We give combinatorial and computational characterizations of the NP search problems definable in the bounded arithmetic theories and .

Thereplacement(orcollectionorchoice) axiom scheme BB(Γ) asserts bounded quantifier exchange as follows: ∀i< |a| ∃x<aϕ(i,x) → ∃w∀i< |a|ϕ(i,[w]i), for ϕ in the class Γ of formulas. The theoryS12proves the scheme BB(Σb1), and thus inS12every Σb1formula is equivalent to a strict Σb1formula (in which all non-sharply-bounded quantifiers are in front). Here we prove (sometimes subject to an assumption) that certain theories weaker thanS12do not prove either BB(Σb1) or BB(Σb0). We show (unconditionally) thatV0does not prove BB(Σb0), where V0(essentially IΣ1,b0) is the two-sorted theory associated with the complexity class AC0. We show that PV does not prove BB(Σb0), assuming that integer factoring is not possible in probabilistic polynomial time. Johannsen and Pollett introduced the theoryC02associated with the complexity class TC0, and later introduced an apparently weaker theory Δb1− CR for the same class. We use our methods to show that Δb1− CR is indeed weaker thanC02, assuming that RSA is secure against probabilistic polynomial time attack.Our main tool is the KPT witnessing theorem.

We describe a system LK(c[/spl lambda/]) for refuting CNF formulae, as a restriction of the sequent calculus in which every formula in a sequent is defined over at most /spl lambda/ variables. This further generalizes the system Res(k), a generalization of Resolution to k-DNF introduced in (Krajicek, 2001). We adapt the Pudlak-Impagliazzo game (Pudlak and Impagliazzo, 2000) to prove lower bounds for treelike LK(c[/spl lambda/]). We show that dynamic satisfiability, which was introduced in (Esteban et al., 2002) to study resolution space complexity, is a sufficient "but not necessary" condition to obtain exponential lower bounds.

The replacement (or collection or choice,) axiom scheme BB(/spl Gamma/) asserts bounded quantifier exchange as follows: /spl forall/I < |a| /spl exist/x < ao(i, x) /spl rarr/ /spl exist/w /spl forall/i < |a| o (i, [w]/sub i/) where o is in the class /spl Gamma/ of formulas. The theory S/sub 2//sup 1/ proves the scheme BB(/spl Sigma//sub 1//sup b/), and thus in S/sub 2//sup 1/ every /spl Sigma//sub 1//sup b/ formula is equivalent to a strict /spl Sigma//sub 1//sup b/ formula (in which all non-sharply-bounded quantifiers are in front). Here we prove (sometimes subject to an assumption) that certain theories weaker than S/sub 2//sup 1/ do not prove either BB(/spl Sigma//sub 1//sup b/) or BB(/spl Sigma//sub 0//sup b/). We show (unconditionally) that V/sup 0/ does not prove BB(/spl Sigma//sub 1//sup B/), where V/sup 0/ (essentially I/spl Sigma//sub 0//sup 1,b/) is the two-sorted theory associated with the complexity class AC/sup 0/. We show that PV does not prove BB(/spl Sigma//sub 0//sup b/), assuming that integer factoring is not possible in probabilistic polynomial time. Johannsen and Pollet introduced the theory C/sub 2//sup 0/ associated with the complexity class TC/sup 0/, and later introduced an apparently weaker theory /spl Delta//sub 1//sup b/ - CR for the same class. We use our methods to show that /spl Delta//sub 1//sup b/ - CR is indeed weaker than C/sub 2//sup 0/, assuming that RSA is secure against probabilistic polynomial time attack. Our main tool is the KPT witnessing theorem.