Linear matroid intersection is an important problem in combinatorial optimization. Given two linear matroids over the same ground set, the linear matroid intersection problem asks you to find a common independent set of maximum size. The deep interest in linear matroid intersection is due to the fact that it generalises many classical problems in theoretical computer science, such as bipartite matching, edge disjoint spanning trees, rainbow spanning tree, and many more. We study this problem in the model of catalytic computation: space-bounded machines are granted access to \textit{catalytic space}, which is additional working memory that is full with arbitrary data that must be preserved at the end of its computation. Although linear matroid intersection has had a polynomial time algorithm for over 50 years, it remains an important open problem to show that linear matroid intersection belongs to any well studied subclass of $\mathsf{P}$. We address this problem for the class catalytic logspace ($\mathsf{CL}$) with a polynomial time bound ($\mathsf{CLP}$). Recently, Agarwala and Mertz (2025) showed that bipartite maximum matching can be computed in the class $\mathsf{CLP}\subseteq \mathsf{P}$. This was the first subclass of $\mathsf{P}$ shown to contain bipartite matching, and additionally the first problem outside $\mathsf{TC}^1$ shown to be contained in $\mathsf{CL}$. We significantly improve the result of Agarwala and Mertz by showing that linear matroid intersection can be computed in $\mathsf{CLP}$.

Recently, Göös et al. [Göös et al., 2024] showed that Res ⋏ uSA = RevRes in the following sense: if a formula φ has refutations of size at most s and width/degree at most w in both Res and uSA, then there is a refutation for φ of size at most poly(s ⋅ 2^w) in RevRes. Their proof relies on the TFNP characterization of the aforementioned proof systems. In our work, we give a direct and simplified proof of this result, simultaneously achieving better bounds: we show that if for a formula φ there are refutations of size at most s in both Res and uSA, then there is a refutation of φ of size at most poly(s) in RevRes. This potentially allows us to "lift" size lower bounds from RevRes to Res for the formulas for which there are upper bounds in uSA. This kind of lifting was not possible before because of the exponential blow-up in size from the width. Similarly, we improve the bounds in another intersection theorem from [Göös et al., 2024] by giving a direct proof of Res ⋏ uNS = RevResT. Finally, we generalize those intersection theorems to some proof systems for which we currently do not have a TFNP characterization. For example, we show that Res(⊕) ⋏ u-wRes(⊕) = RevRes(⊕), which effectively allows us to reduce the problem of proving Pigeonhole Principle lower bounds in Res(⊕) to proving Pigeonhole Principle lower bounds in RevRes(⊕), a potentially weaker proof system.

Suppose we are given an infinite sequence of input cells, each initialized with a uniform random symbol from [n]. How hard is it to output a sequence in [n]n that is close to a uniform random permutation? Viola (SICOMP 2020) conjectured that if each output cell is computed by making d probes to input cells, then d≥ω(1). Our main result shows that, in fact, d≥ (logn)Ω(1), which is tight up to the constant in the exponent. Our techniques also show that if the probes are nonadaptive, then d≥ nΩ(1), which is an exponential improvement over the previous nonadaptive lower bound due to Yu and Zhan (ITCS 2024). Our results also imply lower bounds against succinct data structures for storing permutations.

Aaronson (STOC 2010) conjectured that almost k-wise independence fools constant-depth circuits; he called this the generalised Linial-Nisan conjecture. Aaronson himself later found a counterexample for depth-3 circuits. We give here an improved counterexample for depth-2 circuits (DNFs). This shows, for instance, that Bazzi’s celebrated result (k-wise independence fools DNFs) cannot be generalised in a natural way. We also propose a way to circumvent our counterexample: We define a new notion of pseudorandomness called local couplings and show that it fools DNFs and even decision lists.

In a seminal work, Buhrman et al. (STOC 2014) defined the class CSPACE(s,c) of problems solvable in space s with an additional catalytic tape of size c, which is a tape whose initial content must be restored at the end of the computation. They showed that uniform TC¹ circuits are computable in catalytic logspace, i.e., CL = CSPACE(O(log{n}), 2^{O(log{n})}), thus giving strong evidence that catalytic space gives L strict additional power. Their study focuses on an arithmetic model called register programs, which has been a focal point in development since then. Understanding CL remains a major open problem, as TC¹ remains the most powerful containment to date. In this work, we study the power of catalytic space and register programs to compute circuits of larger depth. Using register programs, we show that for every ε > 0, SAC² ⊆ CSPACE (O((log²n)/(log log n)), 2^{O(log^{1+ε} n)}) . On the other hand, we know that SAC² ⊆ TC² ⊆ CSPACE(O(log²{n}) , 2^{O(log{n})}). Our result thus shows an O(log log n) factor improvement on the free space needed to compute SAC², at the expense of a nearly-polynomial-sized catalytic tape. We also exhibit non-trivial register programs for matrix powering, which is a further step towards showing NC² ⊆ CL.

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 Lifting theorems are used to transfer lower bounds between Boolean function complexity measures. Given a lower bound on a complexity measure $$A$$ A for some function $$f$$ f , we compose $$f$$ f with a carefully chosen gadget function $$g$$ g and get essentially the same lower bound on a complexity measure $$B$$ B for the lifted function $$f \diamond g$$ f ⋄ g . Lifting theorems have applications in many different areas, such as circuit complexity, communication complexity, proof complexity, etc. One of the main questions in the context of lifting is how to choose a suitable gadget $$g$$ g . Generally, to get better results, i.e., to minimize the losses when transferring lower bounds, we need the gadget to be of a constant size (number of inputs). Unfortunately, in many settings we know lifting results only for gadgets of size that grows with the size of $$f$$ f , and it is unclear whether they can be improved to constant-size gadgets. This motivates us to identify the properties of gadgets that make lifting possible. In this paper, we systematically study the question: ‘For which gadgets does the lifting result hold?’ in the following four settings: lifting from decision tree depth to decision tree size, lifting from conjunction DAG width to conjunction DAG size, lifting from decision tree depth to parity decision tree depth and size, and lifting from block sensitivity to deterministic and randomized communication complexities. In all the cases, we prove the complete classification of gadgets by exposing the properties of gadgets that make lifting results hold. The structure of the results shows that there are no intermediate cases—for every gadget, there is either a polynomial lifting or no lifting at all. As a byproduct of our studies, we prove the log-rank conjecture for the class of functions that can be represented as $$f\diamond OR \diamond XOR$$ f ⋄ O R ⋄ X O R for some function $$f$$ f .

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].

Abstract Software projects grow larger every year, which, in turn, makes the testing process harder. One of the most useful methods for testing large projects is unit‐test generation. However, some tests can repeatedly cover the same parts of the code, making it difficult to maintain a growing test codebase. In software testing, test suite minimization plays a crucial role in reducing the cost of testing and improving the efficiency of the testing process. In this paper, we provide an extensible minimization engine that detects redundant tests using one of the supported minimization algorithms without changing the coverage metrics. We also performed a comprehensive analysis of existing approaches and techniques, developed an engine structure, and implemented multiple algorithms of different kinds. Finally, we evaluated our tool on various open‐source projects to demonstrate its effectiveness and efficiency.

A major proof complexity problem is to prove a superpolynomial lower bound on the length of Frege proofs of arbitrary depth. A more general question is to prove an Extended Frege lower bound. Surprisingly, proving such bounds turns out to be much easier in the algebraic setting. In this paper, we study a proof system that can simulate Extended Frege: an extension of the Polynomial Calculus proof system where we can take a square root and introduce new variables that are equivalent to arbitrary depth algebraic circuits. We prove that an instance of the subset-sum principle, the binary value principle 1 + x₁ + 2 x₂ + … + 2^{n-1} x_n = 0 (BVP_n), requires refutations of exponential bit size over ℚ in this system. Part and Tzameret [Fedor Part and Iddo Tzameret, 2020] proved an exponential lower bound on the size of Res-Lin (Resolution over linear equations [Ran Raz and Iddo Tzameret, 2008]) refutations of BVP_n. We show that our system p-simulates Res-Lin and thus we get an alternative exponential lower bound for the size of Res-Lin refutations of BVP_n.

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: