Korten and Pitassi (FOCS, 2024) defined a new complexity class L₂^P as the polynomial-time Turing closure of the Linear Ordering Principle (a total function extending finding the minimum of an order [M. Chiari and J. Krajíček, 1998] to the case where the order is not linear). They put it between MA (Merlin-Arthur protocols) and S₂^P (the second symmetric level of the polynomial hierarchy). In this paper we sandwich L₂^P between P^prMA and P^prSBP. (The oracles here are promise problems, and SBP is the only known class between MA and AM.) The containment in P^prSBP is proved via an iterative process that uses a prSBP oracle to estimate the average order rank of a subset and find the minimum of a linear order. Another containment result of this paper is P^prO₂^P ⊆ O₂^P (where O₂^P is the input-oblivious version of S₂^P). These containment results altogether have several byproducts: - We give an affirmative answer to an open question posed by Chakaravarthy and Roy (Computational Complexity, 2011) whether P^prMA ⊆ S₂^P, thereby settling the relative standing of the existing (non-oblivious) Karp–Lipton–style collapse results of [V. T. Chakaravarthy and S. Roy, 2011] and [J.-Y. Cai, 2007], - We give an affirmative answer to an open question of Korten and Pitassi whether a Karp-Lipton-style collapse can be proven for L₂^P, - We show that the Karp-Lipton-style collapse to P^prOMA is actually better than both known collapses to P^prMA due to Chakaravarthy and Roy (Computational Complexity, 2011) and to O₂^P also due to Chakaravarthy and Roy (STACS, 2006). Thus we resolve the controversy between previously incomparable Karp-Lipton collapses stemming from these two lines of research.

The (extended) Binary Value Principle ( eBVP , the equation ∑ i = 1 n x i 2 i − 1 = − k for k > 0 and Boolean variables x i ) has received a lot of attention recently, several lower bounds have been proved for it [1] , [2] , [11] . Also it has been shown [1] that the probabilistically verifiable Ideal Proof System ( IPS ) [8] together with eBVP polynomially simulates a similar semialgebraic proof system. In this paper we consider Polynomial Calculus with an algebraic version of Tseitin's extension rule ( Ext - PC ) that introduces a new variable for any polynomial. Contrary to IPS , this is a Cook–Reckhow proof system. We show that in this context eBVP still allows to simulate similar semialgebraic systems. We also prove that it allows to simulate the Square Root Rule [6] , which is in sharp contrast with the result of [2] that shows an exponential lower bound on the size of Ext - PC derivations of the Binary Value Principle from its square. On the other hand, we demonstrate that eBVP probably does not help in proving exponential lower bounds for Boolean formulas: we show that an Ext - PC (even with the Square Root Rule) derivation of any unsatisfiable Boolean formula in CNF from eBVP must be of exponential size.

Abstract. 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 [ J. ACM, 65 (2018), 37]. Conversely, we show that short IPS refutations of this instance bridge the gap between sufficiently strong algebraic and semialgebraic proof systems. Our results extend to unrestricted IPS the paradigm introduced by Forbes, Shpilka, Tzameret, and Wigderson [ Theory Comput., 17 (2021), pp. 1–88], 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 semialgebraic over algebraic reasoning, for sufficiently strong systems. Specifically, we show the following. (1) Conditional IPS lower bounds: The Shub–Smale hypothesis [ Duke Math. J., 81 (1995), pp. 47–54] 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 [Formula: see text] for Boolean [Formula: see text]’s. Further, the related and more widely known [Formula: see text]-conjecture [ Duke Math. J., 81 (1995), pp. 47–54] 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 apparently weaker propositional proof systems such as Frege systems (though our lower bounds do not translate to Frege lower bounds since the hard instances are not Boolean formulas). (2) Algebraic versus semialgebraic proofs: Admitting short refutations of the binary value principle is necessary for any algebraic proof system to fully simulate any known semialgebraic 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 semialgebraic proof systems (and most other known concrete propositional proof systems), under the name Cone Proof System (CPS), as a semialgebraic analogue of the IPS: 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 polynomially simulates 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 [Formula: see text] and [Formula: see text].

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:

We consider Boolean circuits over the full binary basis. We prove a (3+1/86)n-o(n) lower bound on the size of such a circuit for an explicitly defined predicate, namely an affine disperser for sublinear dimension. This improves the 3n-o(n) bound of Norbert Blum (1984).The proof is based on the gate elimination technique extended with the following three ideas. We generalize the computational model by allowing circuits to contain cycles, this in turn allows us to perform affine substitutions. We use a carefully chosen circuit complexity measure to track the progress of the gate elimination process. Finally, we use quadratic substitutions that may be viewed as delayed affine substitutions.

Although a simple counting argument shows the existence of Boolean functions of exponential circuit complexity, proving superlinear circuit lower bounds for explicit functions seems to be out of reach of the current techniques. There has been a (very slow) progress in proving linear lower bounds with the latest record of 3 1/86*n-o(n). All known lower bounds are based on the so-called gate elimination technique. A typical gate elimination argument shows that it is possible to eliminate several gates from an optimal circuit by making one or several substitutions to the input variables and repeats this inductively. In this note we prove that this method cannot achieve linear bounds of cn beyond a certain constant c, where c depends only on the number of substitutions made at a single step of the induction.

The existence of a ($p$-)optimal propositional proof system is a major open question in (proof) complexity; many people conjecture that such systems do not exist. Kraj\'{\i}\v{c}ek and Pudl\'{a}k \cite{KP} show that this question is equivalent to the existence of an algorithm that is optimal\footnote{Recent papers \cite{Monroe} call such algorithms \emph{$p$-optimal} while traditionally Levin's algorithm was called \emph{optimal}. We follow the older tradition. Also there is some mess in terminology here, thus please see formal definitions in Sect.~\ref{sec:prelim} below.} on all propositional tautologies. Monroe \cite{Monroe} recently gave a conjecture implying that such algorithm does not exist. We show that in the presence of errors such optimal algorithms \emph{do} exist. The concept is motivated by the notion of heuristic algorithms. Namely, we allow the algorithm to claim a small number of false ``theorems'' (according to any polynomial-time samplable distribution on non-tautologies) and err with bounded probability on other inputs. Our result can also be viewed as the existence of an optimal proof system in a class of proof systems obtained by generalizing automatizable proof systems.

We assume the existence of a function f that is computable in polynomial time but its inverse function is not computable in randomized average-case polynomial time. The cryptographic setting is, however, different: even for a weak one-way function, every possible adversary should fail on a polynomial fraction of inputs. Nevertheless, we show how to construct an infinitely-often one-way function based on f . These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Proof systems for polynomial inequalities in 0-1 variables include the well-studied Cutting Planes proof system (CP) and the Lovász- Schrijver calculi (LS) utilizing linear, respectively, quadratic, inequalities. We introduce generalizations LS d of LS involving polynomial inequalities of degree at most d . Surprisingly, the systems LS d turn out to be very strong. We construct polynomial-size bounded degree LS d proofs of the clique-coloring tautologies (which have no polynomial-size CP proofs), the symmetric knapsack problem (which has no bounded degree Positivstellensatz Calculus (PC) proofs), and Tseitin’s tautologies (hard for many known proof systems). Extending our systems with a division rule yields a polynomial simulation of CP with polynomially bounded coefficients , while other extra rules further reduce the proof degrees for the aforementioned examples. Finally, we prove lower bounds on Lovász-Schrijver ranks , demonstrating, in particular, their rather limited applicability for proof complexity.