Meena Mahajan

SAT Conference 2025 Conference Paper

Semi-Algebraic Proof Systems for QBF

• Olaf Beyersdorff
• Ilario Bonacina
• Kaspar Kasche
• Meena Mahajan
• Luc Nicolas Spachmann

We introduce new semi-algebraic proof systems for Quantified Boolean Formulas (QBF) analogous to the propositional systems Nullstellensatz, Sherali-Adams and Sum-of-Squares. We transfer to this setting techniques both from the QBF literature (strategy extraction) and from propositional proof complexity (size-degree relations and pseudo-expectation). We obtain a number of strong QBF lower bounds and separations between these systems, even when disregarding propositional hardness.

SAT Conference 2024 Conference Paper

New Lower Bounds for Polynomial Calculus over Non-Boolean Bases

• Yogesh Dahiya
• Meena Mahajan
• Sasank Mouli

In this paper, we obtain new size lower bounds for proofs in the Polynomial Calculus (PC) proof system, in two different settings. - When the Boolean variables are encoded using ±1 (as opposed to 0, 1): We establish a lifting theorem using an asymmetric gadget G, showing that for an unsatisfiable formula F, the lifted formula F∘G requires PC size 2^{Ω(d)}, where d is the degree required to refute F. Our lower bound does not depend on the number of variables n, and holds over every field. The only previously known size lower bounds in this setting were established quite recently in [Sokolov, STOC 2020] using lifting with another (symmetric) gadget. The size lower bound there is 2^{Ω((d-d₀)²/n)} (where d₀ is the degree of the initial equations arising from the formula), and is shown to hold only over the reals. - When the PC refutation proceeds over a finite field 𝔽_p and is allowed to use extension variables: We show that there is an unsatisfiable AC⁰[p] formula with N variables for which any PC refutation using N^{1+ε(1-δ)} extension variables, each of arity at most N^{1-ε} and size at most N^c, must have size exp(Ω(N^{εδ}/polylog N)). Our proof achieves these bounds by an XOR-ification of the generalised PHP^{m, r}_n formulas from [Razborov, CC 1998]. The only previously known lower bounds for PC in this setting are those obtained in [Impagliazzo-Mouli-Pitassi, CCC 2023]; in those bounds the number of extension variables is required to be sub-quadratic, and their arity is restricted to logarithmic in the number of original variables. Our result generalises these, and demonstrates a tradeoff between the number and the arity of extension variables. Since our tautology is represented by a small AC⁰[p] formula, our results imply lower bounds for a reasonably strong fragment of AC⁰[p]-Frege.

AAAI Conference 2024 Conference Paper

Runtime vs. Extracted Proof Size: An Exponential Gap for CDCL on QBFs

• Olaf Beyersdorff
• Benjamin Böhm
• Meena Mahajan

Conflict-driven clause learning (CDCL) is the dominating algorithmic paradigm for SAT solving and hugely successful in practice. In its lifted version QCDCL, it is one of the main approaches for solving quantified Boolean formulas (QBF). In both SAT and QBF, proofs can be efficiently extracted from runs of (Q)CDCL solvers. While for CDCL, it is known that the proof size in the underlying proof system propositional resolution matches the CDCL runtime up to a polynomial factor, we show that in QBF there is an exponential gap between QCDCL runtime and the size of the extracted proofs in QBF resolution systems. We demonstrate that this is not just a gap between QCDCL runtime and the size of any QBF resolution proof, but even the extracted proofs are exponentially smaller for some instances. Hence searching for a small proof via QCDCL (even with non-deterministic decision policies) will provably incur an exponential overhead for some instances.

TCS Journal 2023 Journal Article

On (simple) decision tree rank

• Yogesh Dahiya
• Meena Mahajan

In the decision tree computation model for Boolean functions, the depth corresponds to query complexity, and the size corresponds to storage space. The depth measure is the most well-studied one, and is known to be polynomially related to several non-computational complexity measures of functions such as certificate complexity. The size measure is also studied, but to a lesser extent. Another decision tree measure that has received very little attention is the minimal rank of the decision tree, first introduced by Ehrenfeucht and Haussler in 1989. This measure is closely related to the logarithm of the size, but is not polynomially related to depth, and hence it can reveal additional information about the complexity of a function. It is characterised by the value of a Prover-Delayer game first proposed by Pudlák and Impagliazzo in the context of tree-like resolution proofs. In this paper we study this measure further. We obtain an upper bound on depth in terms of rank and Fourier sparsity. We obtain upper and lower bounds on rank in terms of (variants of) certificate complexity. We also obtain upper and lower bounds on the rank for composed functions in terms of the depth of the outer function and the rank of the inner function. This allows us to easily recover known asympotical lower bounds on logarithm of the size for Iterated AND-OR and Iterated 3-bit Majority. We compute the rank exactly for several natural functions and use them to show that all the bounds we have obtained are tight. We also show that rank in the simple decision tree model can be used to bound query complexity, or depth, in the more general conjunctive decision tree model. Finally, we improve upon the known size lower bound for the Tribes function and conclude that in the size-rank relationship for decision trees, obtained by Ehrenfeucht and Haussler, the upper bound for Tribes is asymptotically tight.

Highlights Conference 2023 Conference Abstract

Quantified Boolean Formulas and Proof Complexity

• Meena Mahajan

For several years, both proof complexity and practical solving focussed on propositional proof systems and detecting (un)satisfiability. In the last two decades, several proof systems for the more succinct Quantified Boolean Formulas QBFs have been proposed and studied, and several QBF solvers have been developed. This talk will give an overview of what has been achieved in QBF proof complexity, and how (if at all) it informs QBF solving.

MFCS Conference 2023 Conference Paper

Query Complexity of Search Problems

• Arkadev Chattopadhyay
• Yogesh Dahiya
• Meena Mahajan

We relate various complexity measures like sensitivity, block sensitivity, certificate complexity for multi-output functions to the query complexities of such functions. Using these relations, we provide the following improvements upon the known relationship between pseudo-deterministic and deterministic query complexity for total search problems: - We show that deterministic query complexity is at most the third power of its pseudo-deterministic query complexity. Previously, a fourth-power relation was shown by Goldreich, Goldwasser and Ron (ITCS'13). - We improve the known separation between pseudo-deterministic and randomized decision tree size for total search problems in two ways: (1) we exhibit an exp(Ω̃(n^{1/4})) separation for the SearchCNF relation for random k-CNFs. This seems to be the first exponential lower bound on the pseudo-deterministic size complexity of SearchCNF associated with random k-CNFs. (2) we exhibit an exp(Ω(n)) separation for the ApproxHamWt relation. The previous best known separation for any relation was exp(Ω(n^{1/2})). We also separate pseudo-determinism from randomness in And and (And, Or) decision trees, and determinism from pseudo-determinism in Parity decision trees. For a hypercube colouring problem, that was introduced by Goldwasswer, Impagliazzo, Pitassi and Santhanam (CCC'21) to analyze the pseudo-deterministic complexity of a complete problem in TFNP^{dt}, we prove that either the monotone block-sensitivity or the anti-monotone block sensitivity is Ω(n^{1/3}); Goldwasser et al. showed an Ω(n^{1/2}) bound for general block-sensitivity.

SAT Conference 2022 Conference Paper

QBF Merge Resolution Is Powerful but Unnatural

• Meena Mahajan
• Gaurav Sood 0001

The Merge Resolution proof system (M-Res) for QBFs, proposed by Beyersdorff et al. in 2019, explicitly builds partial strategies inside refutations. The original motivation for this approach was to overcome the limitations encountered in long-distance Q-Resolution proof system (LD-Q-Res), where the syntactic side-conditions, while prohibiting all unsound resolutions, also end up prohibiting some sound resolutions. However, while the advantage of M-Res over many other resolution-based QBF proof systems was already demonstrated, a comparison with LD-Q-Res itself had remained open. In this paper, we settle this question. We show that M-Res has an exponential advantage over not only LD-Q-Res, but even over LQU^+-Res and IRM, the most powerful among currently known resolution-based QBF proof systems. Combining this with results from Beyersdorff et al. 2020, we conclude that M-Res is incomparable with LQU-Res and LQU^+-Res. Our proof method reveals two additional and curious features about MRes: (i) M-Res is not closed under restrictions, and is hence not a natural proof system, and (ii) weakening axiom clauses with existential variables provably yields an exponential advantage over MRes without weakening. We further show that in the context of regular derivations, weakening axiom clauses with universal variables provably yields an exponential advantage over M-Res without weakening. These results suggest that M-Res is better used with weakening, though whether M-Res with weakening is closed under restrictions remains open. We note that even with weakening, M-Res continues to be simulated by eFrege+∀red (the simulation of ordinary M-Res was shown recently by Chew and Slivovsky).

SAT Conference 2020 Conference Paper

MaxSAT Resolution and Subcube Sums

• Yuval Filmus
• Meena Mahajan
• Gaurav Sood 0001
• Marc Vinyals

Abstract We study the MaxRes rule in the context of certifying unsatisfiability. We show that it can be exponentially more powerful than tree-like resolution, and when augmented with weakening (the system MaxResW), p -simulates tree-like resolution. In devising a lower bound technique specific to MaxRes (and not merely inheriting lower bounds from Res), we define a new semialgebraic proof system called the SubCubeSums proof system. This system, which p -simulates MaxResW, is a special case of the Sherali–Adams proof system. In expressivity, it is the integral restriction of conical juntas studied in the contexts of communication complexity and extension complexity. We show that it is not simulated by Res. Using a proof technique qualitatively different from the lower bounds that MaxResW inherits from Res, we show that Tseitin contradictions on expander graphs are hard to refute in SubCubeSums. We also establish a lower bound technique via lifting: for formulas requiring large degree in SubCubeSums, their XOR-ification requires large size in SubCubeSums.

SAT Conference 2019 Conference Paper

Short Proofs in QBF Expansion

• Olaf Beyersdorff
• Leroy Chew
• Judith Clymo
• Meena Mahajan

Abstract For quantified Boolean formulas (QBF) there are two main different approaches to solving: conflict-driven clause learning (QCDCL) and expansion solving. In this paper we compare the underlying proof systems and show that expansion systems admit strictly shorter proofs than QCDCL systems for formulas of bounded quantifier complexity, thus pointing towards potential advantages of expansion solving techniques over QCDCL solving. Our first result shows that tree-like expansion systems allow short proofs of QBFs that are a source of hardness for QCDCL, i. e. tree-like \(\forall \textsf {Exp{+}Res}\) is strictly stronger than tree-like Q-Resolution. In our second result we efficiently transform dag-like Q-Resolution proofs of QBFs with bounded quantifier complexity into \(\forall \textsf {Exp{+}Res}\) proofs. This is theoretical confirmation of experimental findings by Lonsing and Egly, who observed that expansion QBF solvers often outperform QCDCL solvers on instances with few quantifier alternations.

TCS Journal 2018 Journal Article

Sums of read-once formulas: How many summands are necessary?

• Meena Mahajan
• Anuj Tawari

An arithmetic read-once formula (ROF) is a formula (circuit of fan-out 1) over +, × where each variable labels at most one leaf. Every multilinear polynomial can be expressed as the sum of (possibly exponentially many) ROFs. In this work, we prove, for certain multilinear polynomials, a tight lower bound on the number of summands in such an expression.

I&C Journal 2018 Journal Article

Understanding cutting planes for QBFs

• Olaf Beyersdorff
• Leroy Chew
• Meena Mahajan
• Anil Shukla

We study the cutting planes system CP+∀red for quantified Boolean formulas (QBF), obtained by augmenting propositional Cutting Planes with a universal reduction rule, and analyse the proof-theoretic strength of this new calculus. While in the propositional case, Cutting Planes is of intermediate strength between resolution and Frege, our findings here show that the situation in QBF is slightly more complex: while CP+∀red is again weaker than QBF Frege and stronger than the CDCL-based QBF resolution systems Q-Res and QU-Res, it turns out to be incomparable to even the weakest expansion-based QBF resolution system ∀Exp+Res. A similar picture holds for a semantic version semCP+∀red. Technically, our results establish the effectiveness of two lower bound techniques for CP+∀red: via strategy extraction and via monotone feasible interpolation.

CSL Conference 2017 Conference Paper

Arithmetic Circuits: An Overview (Invited Talk)

• Meena Mahajan

This talk reviews recent developments in algebraic complexity theory. It outlines some major results concerning structure, completeness, closure, and lower bounds. It describes some techniques that have been central to obtaining these results, including extreme depth reduction, partial derivatives, and padding.

MFCS Conference 2017 Conference Paper

Computing the Maximum using (min, +) Formulas

• Meena Mahajan
• Prajakta Nimbhorkar
• Anuj Tawari

We study computation by formulas over (min, +). We consider the computation of max{x_1, .. ., x_n} over N as a difference of (min, +) formulas, and show that size n + n \log n is sufficient and necessary. Our proof also shows that any (min, +) formula computing the minimum of all sums of n-1 out of n variables must have n \log n leaves; this too is tight. Our proofs use a complexity measure for (min, +) functions based on minterm-like behaviour and on the entropy of an associated graph.

TCS Journal 2014 Journal Article

Monomials, multilinearity and identity testing in simple read-restricted circuits

• Meena Mahajan
• B.V. Raghavendra Rao
• Karteek Sreenivasaiah

We study the problem of testing if the polynomial computed by an arithmetic circuit is identically zero. We give a deterministic polynomial time algorithm for this problem when the inputs are read-twice or read-thrice formulas. In the process, these algorithms also test if the input circuit is computing a multilinear polynomial. We further study three related computational problems on arithmetic circuits. Given an arithmetic circuit C, (1) ZMC: test if a given monomial in C has zero coefficient or not, (2) MonCount: compute the number of monomials in C, and (3) MLIN: test if C computes a multilinear polynomial or not. These problems were introduced by Fournier, Malod and Mengel (2012) [11], and shown to characterise various levels of the counting hierarchy ( CH ). We address the above problems on read-restricted arithmetic circuits and branching programs. We prove several complexity characterisations for the above problems on these restricted classes of arithmetic circuits.

MFCS Conference 2013 Conference Paper

Small Depth Proof Systems

• Andreas Krebs
• Nutan Limaye
• Meena Mahajan
• Karteek Sreenivasaiah

Abstract A proof system for a language L is a function f such that Range( f ) is exactly L. In this paper, we look at proof systems from a circuit complexity point of view and study proof systems that are computationally very restricted. The restriction we study is: they can be computed by bounded fanin circuits of constant depth (NC 0 ), or of O (loglog n ) depth but with O (1) alternations (poly log AC 0 ). Each output bit depends on very few input bits; thus such proof systems correspond to a kind of local error-correction on a theorem-proof pair. We identify exactly how much power we need for proof systems to capture all regular languages. We show that all regular language have poly log AC 0 proof systems, and from a previous result (Beyersdorff et al, MFCS 2011, where NC 0 proof systems were first introduced), this is tight. Our technique also shows that Maj has poly log AC 0 proof system. We explore the question of whether Taut has NC 0 proof systems. Addressing this question about 2TAUT, and since 2TAUT is closely related to reachability in graphs, we ask the same question about Reachability. We show that both Undirected Reachability and Directed UnReachability have NC 0 proof systems, but Directed Reachability is still open. In the context of how much power is needed for proof systems for languages in NP, we observe that proof systems for a good fraction of languages in NP do not need the full power of AC 0; they have SAC 0 or coSAC 0 proof systems.

TCS Journal 2012 Journal Article

Counting classes and the fine structure between N C 1 and L

• Samir Datta
• Meena Mahajan
• B.V. Raghavendra Rao
• Michael Thomas
• Heribert Vollmer

The class N C 1 of problems solvable by bounded fan-in circuit families of logarithmic depth is known to be contained in logarithmic space L, but not much about the converse is known. In this paper we examine the structure of classes in between N C 1 and L based on counting functions or, equivalently, based on arithmetic circuits. The classes P NC 1 and C = NC 1, defined by a test for positivity and a test for zero, respectively, of arithmetic circuit families of logarithmic depth, sit in this complexity interval. We study the landscape of Boolean hierarchies, constant-depth oracle hierarchies, and logarithmic-depth oracle hierarchies over P NC 1 and C = NC 1. We provide complete problems, obtain the upper bound L for all these hierarchies, and prove partial hierarchy collapses. In particular, the constant-depth oracle hierarchy over P NC 1 collapses to its first level P NC 1, and the constant-depth oracle hierarchy over C = NC 1 collapses to its second level.

MFCS Conference 2012 Conference Paper

Identity Testing, Multilinearity Testing, and Monomials in Read-Once/Twice Formulas and Branching Programs

• Meena Mahajan
• B. V. Raghavendra Rao
• Karteek Sreenivasaiah

Abstract We study the problem of testing if the polynomial computed by an arithmetic circuit is identically zero ( ACIT ). We give a deterministic polynomial time algorithm for this problem when the inputs are read-twice formulas. This algorithm also computes the MLIN predicate, testing if the input circuit computes a multilinear polynomial. We further study two related computational problems on arithmetic circuits. Given an arithmetic circuit C, 1) ZMC: test if a given monomial in C has zero coefficient or not, and 2) MonCount: compute the number of monomials in C. These problems were introduced by Fournier, Malod and Mengel [STACS 2012], and shown to characterize various levels of the counting hierarchy ( CH ). We address the above problems on read-restricted arithmetic circuits and branching programs. We prove several complexity characterizations for the above problems on these restricted classes of arithmetic circuits.

TCS Journal 2012 Journal Article

The planar k -means problem is NP-hard

• Meena Mahajan
• Prajakta Nimbhorkar
• Kasturi Varadarajan

In the k -means problem, we are given a finite set S of points in ℜ m, and integer k ≥ 1, and we want to find k points (centers) so as to minimize the sum of the square of the Euclidean distance of each point in S to its nearest center. We show that this well-known problem is NP-hard even for instances in the plane, answering an open question posed by Dasgupta (2007) [7].

MFCS Conference 2011 Conference Paper

Verifying Proofs in Constant Depth

• Olaf Beyersdorff
• Samir Datta
• Meena Mahajan
• Gido Scharfenberger-Fabian
• Karteek Sreenivasaiah
• Michael Thomas 0001
• Heribert Vollmer

Abstract In this paper we initiate the study of proof systems where verification of proofs proceeds by \(\protect{\ensuremath{\mathsf{NC}}}^{0}\) circuits. We investigate the question which languages admit proof systems in this very restricted model. Formulated alternatively, we ask which languages can be enumerated by \(\protect{\ensuremath{\mathsf{NC}}}^{0}\) functions. Our results show that the answer to this problem is not determined by the complexity of the language. On the one hand, we construct \(\protect{\ensuremath{\mathsf{NC}}}^{0}\) proof systems for a variety of languages ranging from regular to \(\protect{\ensuremath{\mathsf{NP}}}\) -complete. On the other hand, we show by combinatorial methods that even easy regular languages such as Exact-OR do not admit \(\protect{\ensuremath{\mathsf{NC}}}^{0}\) proof systems. We also present a general construction of \(\protect{\ensuremath{\mathsf{NC}}}^{0}\) proof systems for regular languages with strongly connected NFA’s.

MFCS Conference 2010 Conference Paper

Counting Classes and the Fine Structure between NC 1 and L

• Samir Datta
• Meena Mahajan
• B. V. Raghavendra Rao
• Michael Thomas 0001
• Heribert Vollmer

Abstract The class NC 1 of problems solvable by bounded fan-in circuit families of logarithmic depth is known to be contained in logarithmic space L, but not much about the converse is known. In this paper we examine the structure of classes in between NC 1 and L based on counting functions or, equivalently, based on arithmetic circuits. The classes PNC 1 and C = NC 1, defined by a test for positivity and a test for zero, respectively, of arithmetic circuit families of logarithmic depth, sit in this complexity interval. We study the landscape of Boolean hierarchies, constant-depth oracle hierarchies, and logarithmic-depth oracle hierarchies over PNC 1 and C = NC 1. We provide complete problems, obtain the upper bound L for all these hierarchies, and prove partial hierarchy collapses—in particular, the constant-depth oracle hierarchy over PNC 1 collapses to its first level PNC 1, and the constant-depth oracle hierarchy over C = NC 1 collapses to its second level.

MFCS Conference 2008 Conference Paper

Arithmetic Circuits, Syntactic Multilinearity, and the Limitations of Skew Formulae

• Meena Mahajan
• B. V. Raghavendra Rao

Abstract Functions in arithmetic NC 1 are known to have equivalent constant width polynomial degree circuits, but the converse containment is unknown. In a partial answer to this question, we show that syntactic multilinear circuits of constant width and polynomial degree can be depth-reduced, though the resulting circuits need not be syntactic multilinear. We then focus specifically on polynomial-size syntactic multilinear circuits, and study relationships between classes of functions obtained by imposing various resource (width, depth, degree) restrictions on these circuits. Along the way, we obtain a characterisation of NC 1 (and its arithmetic counterparts) in terms of log width restricted planar branching programs. We also study the power of skew formulae, and show that even exponential sums of these are unlikely to suffice to express the determinant function.

I&C Journal 2004 Journal Article

The complexity of planarity testing

• Eric Allender
• Meena Mahajan

We clarify the computational complexity of planarity testing, by showing that planarity testing is hard for L, and lies in SL. This nearly settles the question, since it is widely conjectured that L=SL. The upper bound of SL matches the lower bound of L in the context of (nonuniform) circuit complexity, since L /poly is equal to SL /poly. Similarly, we show that a planar embedding, when one exists, can be found in FL SL. Previously, these problems were known to reside in the complexity class AC 1, via the O(logn) time CRCW PRAM algorithm of Ramachandran and Reif, although planarity checking for degree-three graphs had been shown to be in SL [Chicago J. Theoret. Comput. Sci. (1995); J. ACM 31 (2) (1984) 401].

STOC Conference 2000 Conference Paper

A new NC-algorithm for finding a perfect matching in bipartite planar and small genus graphs (extended abstract)

• Meena Mahajan
• Kasturi R. Varadarajan

TCS Journal 1998 Journal Article

Non-commutative arithmetic circuits: depth reduction and size lower bounds

• Eric Allender
• Jia Jiao
• Meena Mahajan
• V. Vinay

We investigate the phenomenon of depth-reduction in commutative and non-commutative arithmetic circuits. We prove that in the commutative setting, uniform semi-unbounded arithmetic circuits of logarithmic depth are as powerful as uniform arithmetic circuits of polynomial degree (and unrestricted depth); earlier proofs did not work in the uniform setting. This also provides a unified proof of the circuit characterizations of the class LOGCFL and its counting variant #LOGCFL. We show that AC1 has no more power than arithmetic circuits of polynomial size and degree n O(log log n) (improving the trivial bound of n O(log n)). Connections are drawn between TC1 and arithmetic circuits of polynomial size and degree. Then we consider non-commutative computation. We show that over the algebra (∑∗, max, concat), arithmetic circuits of polynomial size and polynomial degree can be reduced to O(log 2 n) depth (and even to O(log n) depth if unbounded-fanin gates are allowed). This establishes that OptLOGCFL is in AC1. This is the first depth-reduction result for arithmetic circuits over a non-commutative semiring, and it complements the lower bounds of Kosaraju and Nisan showing that depth reduction cannot be done in the general non-commutative setting. We define new notions called “short-left-paths” and “short-right-paths” and we show that these notions provide a characterization of the classes of arithmetic circuits for which optimal depth reduction is possible. This class also can be characterized using the AuxPDA model. Finally, we characterize the languages generated by efficient circuits over the semiring (2∑∗, union, concat) in terms of simple one-way machines, and we investigate and extend earlier lower bounds on non-commutative circuits.

SODA Conference 1997 Conference Paper

A Combinatorial Algorithm for the Determinant

• Meena Mahajan
• V. Vinay

TCS Journal 1995 Journal Article

Nondeterministic, probabilistic and alternating computations on cellular array models

• Kamala Krithivasan
• Meena Mahajan

A new mechanism for introducing nondeterminism on the cellular automaton model is introduced. It is shown that this form of nondeterminism corresponds to the traditional notion in the unbounded-time case, but there appear to be differences when real-time or linear-time cellular automata are considered. The notion is then generalised to include probabilistic and alternating computations. Restricted nondeterminism classes are also defined and studied, in an attempt to refine the power of nondeterminism.