The Stabbing Planes proof system [8] was introduced to model the reasoning carried out in practical mixed integer programming solvers. As a proof system, it is powerful enough to simulate Cutting Planes and to refute the Tseitin formulas - certain unsatisfiable systems of linear equations mod2 - which are canonical hard examples for many algebraic proof systems. In a recent (and surprising) result, Dadush and Tiwari [25] showed that these short refutations of the Tseitin formulas could be translated into quasi-polynomial size and depth Cutting Planes proofs, refuting a long-standing conjecture. This translation raises several interesting questions. First, whether all Stabbing Planes proofs can be efficiently simulated by Cutting Planes. This would allow for the substantial analysis done on the Cutting Planes system to be lifted to practical mixed integer programming solvers. Second, whether the quasi-polynomial depth of these proofs is inherent to Cutting Planes. In this paper we make progress towards answering both of these questions. First, we show that any Stabbing Planes proof with bounded coefficients (SP*) can be translated into Cutting Planes. As a consequence of the known lower bounds for Cutting Planes, this establishes the first exponential lower bounds on SP*. Using this translation, we extend the result of Dadush and Tiwari to show that Cutting Planes has short refutations of any unsatisfiable system of linear equations over a finite field. Like the Cutting Planes proofs of Dadush and Tiwari, our refutations also incur a quasi-polynomial blow-up in depth, and we conjecture that this is inherent. As a step towards this conjecture, we develop a new geometric technique for proving lower bounds on the depth of Cutting Planes proofs. This allows us to establish the first lower bounds on the depth of Semantic Cutting Planes proofs of the Tseitin formulas.
We introduce a new family of propositional proof systems, denoted , for an arbitrary TFNP search problem R. Informally, a refutation of a CNF formula F in is given by a polynomial-time reduction from the false-clause search problem Search_F to R, combined with an Extended Frege proof that the reduction is correct. These are motivated in two ways: 1. They are the propositional translations of witnessing theorems in bounded arithmetic, by which proofs of ∀ Σ^b_1 formulas ϕ in a theory T imply algorithms solving the search problem for ϕ in a TFNP class corresponding to T. 2. They are a white-box analogue of the characterizations of proof systems using decision tree reductions to black-box TFNP problems. We consider the proof system , where Iter is a complete problem for PLS. We prove that is polynomially equivalent to the sequent calculus G_1, and also to the implicit Resolution proof system [EF, Resolution]. Hence G_1 and [EF, Resolution] are equivalent, which is the first characterization of an implicit proof system by a classical proof system beyond the work of Wang. We also consider for general TFNP relations R. We observe that if EF can prove that a search problem R is in FP, then is polynomially equivalent to EF. This contrasts to our above result, which shows that Extended-Frege provable reductions to Iter, a problem widely believed not to be in FP, yields a proof system (G_1) that is believed to be stronger than Extended Frege. Finally, we show that for any proof system P which is sufficiently strong, there is a polynomial-time computable search problem R_P ∈ FP such that is polynomially equivalent to P. Letting P = [EF, Resolution] and combining our two results shows that is polynomially equivalent to .
We prove new upper and lower bounds on ε-approximate sign-rank, a relaxation of sign-rank introduced by Chornomaz, Moran, and Waknine (STOC 2025). We show that every m × n sign matrix with approximate sign-rank d contains a monochromatic rectangle of size d^-O(d)m × d^-O(d^2)n, paralleling classical results for exact sign-rank. As an application, we establish a lower bound of Ω(√(d/log d)) on the ε-approximate sign-rank of large-margin d-dimensional half-spaces. Prior to our work, the only general lower bound technique known for approximate sign-rank yielded bounds of strength ε^-1 - 1, which are constant for fixed ε. A key ingredient is a new geometric theorem on hyperplane avoidance: for any set of n points in general position in ℝ^d, there exist d subsets, each of size d^-O(d) n, such that no hyperplane simultaneously splits all of them. The proof combines the Forster-Barthe isotropic position theorem with the Bourgain-Tzafriri restricted invertibility principle. We also study the relationship between approximate sign-rank and VC dimension. We prove a lower bound on approximate sign-rank in terms of VC dimension, and exhibit concept classes of VC dimension 2 with large approximate sign-rank. Finally, we study the approximate sign-rank of the 2^m × 2^m Hadamard matrix H_m. The sign-rank of H_m is known to be Ω(√(2^m)) by Forster's classic theorem. Contrasting this, we adapt an argument of Alman and Williams to show that the approximate sign-rank of H_m is at most m^O(√(m)log(1/ε)), and hence the Hadamard matrix does not witness polynomial-strength lower bounds for approximate sign-rank. Using our VC dimension bound, we prove that the approximate sign-rank of H_m is at least Ω_ε(m).
The complexity class PPP contains all total search problems many-one reducible to the Pigeon problem, where we are given a succinct encoding of a function mapping n+1 pigeons to n holes, and must output two pigeons that collide in a hole. PPP is one of the “original five” syntactically-defined subclasses of TFNP, and has been extensively studied due to the strong connections between its defining problem — the pigeonhole principle — and problems in cryptography, extremal combinatorics, proof complexity, and other fields. However, despite its importance, PPP appears to be less robust than the other important TFNP subclasses. In particular, unlike all other major TFNP subclasses, it was conjectured by Buss and Johnson that PPP is not closed under Turing reductions, and they called for a black-box separation in order to provide evidence for this conjecture. The question of whether PPP contains its Turing closure was further highlighted by Daskalakis in his recent IMU Abacus Medal Lecture. In this work we prove that PPP is indeed not Turing-closed in the black-box setting, affirmatively resolving the above conjecture and providing strong evidence that PPP is not Turing-closed. In fact, we are able to separate PPP from its non-adaptive Turing closure, in which all calls to the Pigeon oracle must be made in parallel. This differentiates PPP from all other important TFNP subclasses, and especially from its closely-related subclass PWPP — defined by reducibility to the weak pigeonhole principle — which is known to be non-adaptively Turing-closed. Our proof requires developing new tools for PPP lower bounds, and creates new connections between PPP and the theory of pseudoexpectation operators used for Sherali-Adams and Sum-of-Squares lower bounds. In particular, we introduce a new type of pseudoexpectation operator that is precisely tailored for lower bounds against black-box PPP, which may be of independent interest.
Abstract. We show [Formula: see text]. Here the class [Formula: see text] consists of all total search problems that reduce to the End-of-Potential-Line problem, which was introduced in the works by Hubáček and Yogev (SICOMP 2020) and Fearnley et al. (JCSS 2020). In particular, our result yields a new simpler proof of the breakthrough collapse [Formula: see text] by Fearnley et al. (STOC 2021). We also prove a companion result [Formula: see text], where [Formula: see text] is the class associated with the Sink-of-Potential-Line problem.
We show that the TFNP problem Ramsey is not black-box reducible to Pigeon, refuting a conjecture of Goldberg and Papadimitriou in the black-box setting. We prove this by giving reductions to Ramsey from a new family of TFNP problems that correspond to generalized versions of the pigeonhole principle, and then proving that these generalized versions cannot be reduced to Pigeon. Formally, we define $t$ -PPP as the class of total NP-search problems reducible to finding a $t$ -collision in a mapping from $(t-1) N + 1$ pigeons to $N$ holes. These classes are closely related to multi-collision resistant hash functions in cryptography. We show that the generalized pigeonhole classes form a hierarchy as $t$ increases, and also give a natural condition on the parameters $t_{1}, t_{2}$ that captures exactly when $t_{1}$ -PPP and $t_2$ -PPP collapse in the black-box setting. Finally, we prove other inclusion and separation results between these generalized Pigeon problems and other previously studied TFNP subclasses, such as PLS, PPA, and PLC. Our separation results rely on new lower bounds in propositional proof complexity based on pseudoexpectation operators, which may be of independent interest.
One of the major open problems in complexity theory is proving super-logarithmic lower bounds on the depth of circuits (i.e., P\nsubseteq NC 1 ). Karchmer, Raz, and Wigderson [13] suggested to approach this problem by proving that depth complexity behaves “as expected” with respect to the composition of functions f◇g. They showed that the validity of this conjecture would imply that P\nsubseteq NC 1 . Several works have made progress toward resolving this conjecture by proving special cases. In particular, these works proved the KRW conjecture for every outer function, but only for few inner functions. Thus, it is an important challenge to prove the KRW conjecture for a wider range of inner functions. In this work, we extend significantly the range of inner functions that can be handled. First, we consider the monotone version of the KRW conjecture. We prove it for every monotone inner function whose depth complexity can be lower bounded via a query-to-communication lifting theorem. This allows us to handle several new and well-studied functions such as the s-t-connectivity, clique, and generation functions. In order to carry this progress back to the non-monotone setting, we introduce a new notion of semi-monotone composition, which combines the non-monotone complexity of the outer function with the monotone complexity of the inner function. In this setting, we prove the KRW conjecture for a similar selection of inner functions, but only for a specific choice of the outer function f.
We show EOPL = PLS \cap PsansP \sansP AD. Here the class EOPL consists of all total search problems that reduce to the END -OF -POTENTIAL -LINE problem, which was introduced in the works by Hub\'acv \ek and Yogev (SICOMP 2020) and Fearnley et al. (JCSS 2020). In particular, our result yields a new simpler proof of the breakthrough collapse CLS = PLS \cap PsansP \sansP AD by Fearnley et al. (STOC 2021). We also prove a companion result SOPL = PLS \cap PsansP \sansP ADS, where SOPL is the class associated with the SINK -OF -POTENTIAL -LINE problem.
It is well-known that Resolution proofs can be efficiently simulated by Sherali-Adams (SA) proofs. We show 1 , however, that any such simulation needs to exploit huge coefficients: Resolution cannot be efficiently simulated by SA when the coefficients are written in unary. We also show that Reversible Resolution (a variant of MaxSAT Resolution) cannot be efficiently simulated by Nullstellensatz (NS). These results have consequences for total NP search problems. First, we characterise the classes PPADS, PPAD, SOPL by unary-SA, unary-NS, and Reversible Resolution, respectively. Second, we show that, relative to an oracle, PLS $\nsubseteq$ PPP, SOPL $\nsubseteq$ PPA, and EOPL $\nsubseteq$ UEOPL. In particular, together with prior work, this gives a complete picture of the black-box relationships between all classical TFNP classes introduced in the 1990s. 1 This is an extended abstract. For the full version of this article, please refer to [GHJ+22b].
Recent work has shown that many of the standard TFNP classes – such as PLS , PPADS , PPAD , SOPL , and EOPL – have corresponding proof systems in propositional proof complexity, in the sense that a total search problem is in the class if and only if the totality of the problem can be efficiently proved by the corresponding proof system. We build on this line of work by studying coloured variants of these TFNP classes: C - PLS , C - PPADS , C - PPAD , C - SOPL , and C - EOPL . While C - PLS has been studied in the literature before, the coloured variants of the other classes are introduced here for the first time. We give a family of results showing that these coloured TFNP classes are natural objects of study, and that the correspondence between TFNP and natural propositional proof systems is not an exceptional phenomenon isolated to weak TFNP classes. Namely, we show that: Each of the classes C - PLS , C - PPADS , and C - SOPL have corresponding proof systems characterizing them. Specifically, the proof systems for these classes are obtained by adding depth to the formulas in the corresponding proof system for the uncoloured class. For instance, while it was previously known that PLS is characterized by bounded-width Resolution (i.e. depth 0.5 Frege), we prove that C - PLS is characterized by depth-1.5 Frege (Res( polylog ( n ))). The classes C - PPAD and C - EOPL coincide exactly with the uncoloured classes PPADS and SOPL , respectively. Thus, both of these classes also have corresponding proof systems: unary Sherali-Adams and Reversible Resolution, respectively. Finally, we prove a coloured intersection theorem for the coloured sink classes, showing C - PLS ∩ C - PPADS = C - SOPL , generalizing the intersection theorem PLS ∩ PPADS = SOPL . However, while it is known in the uncoloured world that PLS ∩ PPAD = EOPL = CLS , we prove that this equality fails in the coloured world in the black-box setting. More precisely, we show that there is an oracle O such that C - PLS O ∩ C - PPAD O ⊋ C - EOPL O . To prove our results, we introduce an abstract multivalued proof system – the Blockwise Calculus – which may be of independent interest.
Most recent works on cryptographic obfuscation focus on the high-end regime of obfuscating general circuits while guaranteeing computational indistinguishability between functionally equivalent circuits. Motivated by the goals of simplicity and efficiency, we initiate a systematic study of “low-end” obfuscation, focusing on simpler representation models and information-theoretic notions of security. We obtain the following results. Positive results via “white-box” learning. We present a general technique for obtaining perfect indistinguishability obfuscation from exact learning algorithms that are given restricted access to the representation of the input function. We demonstrate the usefulness of this approach by obtaining simple obfuscation for decision trees and multilinear read-k arithmetic formulas. Negative results via PAC learning. A proper obfuscation scheme obfuscates programs from a class C by programs from the same class. Assuming the existence of one-way functions, we show that there is no proper indistinguishability obfuscation scheme for k -CNF formulas for any constant k ≥ 3; in fact, even obfuscating 3-CNF by k -CNF is impossible. This result applies even to computationally secure obfuscation, and makes an unexpected use of PAC learning in the context of negative results for obfuscation. Separations. We study the relations between different information-theoretic notions of indistin-guishability obfuscation, giving cryptographic evidence for separations between them.
11 A language L is random-self-reducible if deciding membership in L can be reduced (in polynomial 12 time) to deciding membership in L for uniformly random instances. It is known that several “number 13 theoretic” languages (such as computing the permanent of a matrix) admit random self-reductions. 14 Feigenbaum and Fortnow showed that NP-complete languages are not non-adaptively random-self15 reducible unless the polynomial-time hierarchy collapses, giving suggestive evidence that NP may 16 not admit random self-reductions. Hirahara and Santhanam introduced a weakening of random 17 self-reductions that they called pseudorandom self-reductions, in which a language L is reduced to 18 a distribution that is computationally indistinguishable from the uniform distribution. They then 19 showed that the Minimum Circuit Size Problem (MCSP) admits a non-adaptive pseudorandom 20 self-reduction, and suggested that this gave further evidence that distinguished MCSP from standard 21 NP-Complete problems. 22 We show that, in fact, the Clique problem admits a non-adaptive pseudorandom self-reduction, 23 assuming the planted clique conjecture. More generally we show the following. Call a property of 24 graphs π hereditary if G ∈ π implies H ∈ π for every induced subgraph of G. We show that for any 25 infinite hereditary property π, the problem of finding a maximum induced subgraph H ∈ π of a 26 given graph G admits a non-adaptive pseudorandom self-reduction. 27 2012 ACM Subject Classification Theory of computation → Problems, reductions and completeness 28
We study the amortized circuit complexity of boolean functions. Given a circuit model $\mathcal{F}$ and a boolean function $f:\{0,1\}^{n}\rightarrow\{0,1\}$, the $\mathcal{F}$-amortized circuit complexity is defined to be the size of the smallest circuit that outputs $m$ copies of $f$ (evaluated on the same input), divided by $m$, as $m\rightarrow\infty$. We prove a general duality theorem that characterizes the amortized circuit complexity in terms of “formal complexity measures”. More precisely, we prove that the amortized circuit complexity in any circuit model composed out of gates from a finite set is equal to the pointwise maximum of the family of “formal complexity measures” associated with $\mathcal{F}$. Our duality theorem captures many of the formal complexity measures that have been previously studied in the literature for proving lower bounds (such as formula complexity measures, submodular complexity measures, and branching program complexity measures), and thus gives a characterization of formal complexity measures in terms of circuit complexity. We also introduce and investigate a related notion of catalytic circuit complexity, which we show is “intermediate” between amortized circuit complexity and standard circuit complexity, and which we also characterize (now, as the best integer solution to a linear program). Finally, using our new duality theorem as a guide, we strengthen the known upper bounds for non-uniform catalytic space, introduced by Buhrman et. al [1] (this is related to, but not the same as, our notion of catalytic circuit size). Potechin [2] proved that for any boolean function $f:\{0,1\}^{n}\rightarrow\{0,1\}$, there is a catalytic branching program computing $m=2^{2^{n}-1}$ copies of $f$ with total size $O(mn)$-that is, linear size per copy — refuting a conjecture of Girard, Koucký and McKenzie [3]. Potechin then asked if the number of copies $m$ can be reduced while retaining the amortized upper bound. We make progress on this question by showing that if $f$ has degree $d$ when represented as polynomial over $\mathbb{F}_{2}$, then there is a catalytic branching program computing $m=2^{\begin{pmatrix}n\\ \leq d\end{pmatrix}}$ copies of $f$ with total size $O(mn)$.
We give a new characterization of the Sherali-Adams proof system, showing that there is a degree- d Sherali-Adams refutation of an unsatisfiable CNF formula C if and only if there is an ε > 0 and a degree- d conical junta J such that viol C ( x ) − ε = J , where viol C ( x ) counts the number of falsified clauses of C on an input x . Using this result we show that the linear separation complexity , a complexity measure recently studied by Hrubeˇs (and independently by de Oliveira Oliveira and Pudl´ak under the name of weak monotone linear programming gates ), monotone feasibly interpolates Sherali-Adams proofs. We then investigate separation results for viol C ( x ) − ε . In particular, we give a family of unsatisfiable CNF formulas C which have polynomial-size and small-width resolution proofs, but for which any representation of viol C ( x ) − 1 by a conical junta requires degree Ω( n ) ; this resolves an open question of Filmus, Mahajan, Sood, and Vinyals. Since Sherali-Adams can simulate resolution, this separates the non-negative degree of viol C ( x ) − 1 and viol C ( x ) − ε for arbitrarily small ε > 0 . Finally, by applying lifting theorems, we translate this lower bound into new separation results between extension complexity and monotone circuit complexity.
We survey lower-bound results in complexity theory that have been obtained via newfound interconnections between propositional proof complexity, boolean circuit complexity, and query/communication complexity. We advocate for the theory of total search problems (TFNP) as a unifying language for these connections and discuss how this perspective suggests a whole programme for further research.
We survey lower-bound results in complexity theory that have been obtained via newfound interconnections between propositional proof complexity, boolean circuit complexity, and query/communication complexity. We advocate for the theory of total search problems (TFNP) as a unifying language for these connections and discuss how this perspective suggests a whole programme for further research.
We survey lower-bound results in complexity theory that have been obtained via newfound interconnections between propositional proof complexity, boolean circuit complexity, and query/communication complexity. We advocate for the theory of total search problems (TFNP) as a unifying language for these connections and discuss how this perspective suggests a whole programme for further research.
The random k -SAT model is one of the most important and well-studied distributions over k -SAT instances. It is closely connected to statistical physics and is a benchmark for satisfiability algorithms. We show that when \( k = \Theta (\log n) \), any Cutting Planes refutation for random k -SAT requires exponential length in the regime where the number of clauses guarantees that the formula is unsatisfiable with high probability.
We establish an exactly tight relation between reversible pebblings of graphs and Nullstellensatz refutations of pebbling formulas, showing that a graph G can be reversibly pebbled in time t and space s if and only if there is a Nullstellensatz refutation of the pebbling formula over G in size t + 1 and degree s (independently of the field in which the Nullstellensatz refutation is made). We use this correspondence to prove a number of strong size-degree trade-offs for Nullstellensatz, which to the best of our knowledge are the first such results for this proof system.
We show that algebraic proofs are hard to find: Given an unsatisfiable CNF formula F , it is NP -hard to find a refutation of F in the Nullstellensatz, Polynomial Calculus, or Sherali–Adams proof systems in time polynomial in the size of the shortest such refutation. Our work extends, and gives a simplified proof of, the recent breakthrough of Atserias and Müller (JACM 2020) that established an analogous result for Resolution.