arXiv subjects

Meena Mahajan

Publications and source records attributed to Meena Mahajan.

15 recordsLinked to original sources

arXiv2025

Semi-Algebraic Proof Systems for QBF

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.

cs.LO↗

arXiv2025

On the Interplay of Cube Learning and Dependency Schemes in QCDCL Proof Systems

Quantified Conflict Driven Clause Leaning (QCDCL) is one of the main approaches to solving Quantified Boolean Formulas (QBF). Cube-learning is employed in this approach to ensure that true formulas can be verified. Dependency Schemes help to detect spurious dependencies that are implied by the variable ordering in the quantifier prefix of QBFs but are not essential for constructing (counter)models. This detection can provably shorten refutations in specific proof systems, and is expected to speed up runs of QBF solvers. The simplest underlying proof system [BeyersdorffB\"ohm-LMCS2023], formalises the reasoning in the QCDCL approach on false formulas, when neither cube learning nor dependency schemes is used. The work of [B\"ohmPeitlBeyersdorff-AI2024] further incorporates cube-learning. The work of [ChoudhuryMahajan-JAR2024] incorporates a limited use of dependency schemes, but without cube-learning. In this work, proof systems underlying the reasoning of QCDCL solvers which use cube learning, and which use dependency schemes at all stages, are formalised. Sufficient conditions for soundness and completeness are presented, and it is shown that using the standard and reflexive resolution path dependency schemes ($D^{std}$ and $D^{rrs}$) to relax the decision order provably shortens refutations. When the decisions are restricted to follow quantification order, but dependency schemes are used in propagation and learning, in conjunction with cube-learning, the resulting proof systems using the dependency schemes $D^{std}$ and $D^{rrs}$ are investigated in detail and their relative strengths are analysed.

cs.LO↗

arXiv2024

QBF Merge Resolution is powerful but unnatural

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 M-Res: (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 M-Res 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 $+$ $\forall$red (the simulation of ordinary M-Res was shown recently by Chew and Slivovsky).

cs.CC↗

arXiv2024

Hard QBFs for Merge Resolution

We prove the first genuine QBF proof size lower bounds for the proof system Merge Resolution (MRes [Olaf Beyersdorff et al., 2020]), a refutational proof system for prenex quantified Boolean formulas (QBF) with a CNF matrix. Unlike most QBF resolution systems in the literature, proofs in MRes consist of resolution steps together with information on countermodels, which are syntactically stored in the proofs as merge maps. As demonstrated in [Olaf Beyersdorff et al., 2020], this makes MRes quite powerful: it has strategy extraction by design and allows short proofs for formulas which are hard for classical QBF resolution systems. Here we show the first genuine QBF exponential lower bounds for MRes, thereby uncovering limitations of MRes. Technically, the results are either transferred from bounds from circuit complexity (for restricted versions of MRes) or directly obtained by combinatorial arguments (for full MRes). Our results imply that the MRes approach is largely orthogonal to other QBF resolution models such as the QCDCL resolution systems QRes and QURes and the expansion systems $\forall$Exp+Res and IR.

cs.CC↗

arXiv2022

MaxSAT Resolution and Subcube Sums

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 proof system called the SubCubeSums proof system. This system, which p-simulates MaxResW, can be viewed as a special case of the semialgebraic 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.

cs.CC↗

arXiv2022

On (Simple) Decision Tree Rank

In the decision tree computation model for Boolean functions, the depth corresponds to query complexity, and 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 allow 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.

cs.CC↗

arXiv2020

Algebraic Branching Programs, Border Complexity, and Tangent Spaces

Nisan showed in 1991 that the width of a smallest noncommutative single-(source,sink) algebraic branching program (ABP) to compute a noncommutative polynomial is given by the ranks of specific matrices. This means that the set of noncommutative polynomials with ABP width complexity at most $k$ is Zariski-closed, an important property in geometric complexity theory. It follows that approximations cannot help to reduce the required ABP width. It was mentioned by Forbes that this result would probably break when going from single-(source,sink) ABPs to trace ABPs. We prove that this is correct. Moreover, we study the commutative monotone setting and prove a result similar to Nisan, but concerning the analytic closure. We observe the same behavior here: The set of polynomials with ABP width complexity at most $k$ is closed for single-(source,sink) ABPs and not closed for trace ABPs. The proofs reveal an intriguing connection between tangent spaces and the vector space of flows on the ABP. We close with additional observations on VQP and the closure of VNP which allows us to establish a separation between the two classes.

cs.CC↗

arXiv2019

Lower Bounds for Linear Decision Lists

We demonstrate a lower bound technique for linear decision lists, which are decision lists where the queries are arbitrary linear threshold functions. We use this technique to prove an explicit lower bound by showing that any linear decision list computing the function $MAJ \circ XOR$ requires size $2^{0.18 n}$. This completely answers an open question of Tur{á}n and Vatan [FoCM'97]. We also show that the spectral classes $PL_1, PL_\infty$, and the polynomial threshold function classes $\widehat{PT}_1, PT_1$, are incomparable to linear decision lists.

cs.CC↗

arXiv2017

Feasible Interpolation for QBF Resolution Calculi

In sharp contrast to classical proof complexity we are currently short of lower bound techniques for QBF proof systems. In this paper we establish the feasible interpolation technique for all resolution-based QBF systems, whether modelling CDCL or expansion-based solving. This both provides the first general lower bound method for QBF proof systems as well as largely extends the scope of classical feasible interpolation. We apply our technique to obtain new exponential lower bounds to all resolution-based QBF systems for a new class of QBF formulas based on the clique problem. Finally, we show how feasible interpolation relates to the recently established lower bound method based on strategy extraction.

cs.CC↗

arXiv2016

Some Complete and Intermediate Polynomials in Algebraic Complexity Theory

We provide a list of new natural $\mathsf{VNP}$-intermediate polynomial families, based on basic (combinatorial) $\mathsf{NP}$-complete problems that are complete under parsimonious reductions. Over finite fields, these families are in $\mathsf{VNP}$, and under the plausible hypothesis $\mathsf{Mod}_p\mathsf{P} \not\subseteq \mathsf{P/poly}$, are neither $\mathsf{VNP}$-hard (even under oracle-circuit reductions) nor in $\mathsf{VP}$. Prior to this, only the Cut Enumerator polynomial was known to be $\mathsf{VNP}$-intermediate, as shown by Bürgisser in 2000. We next show that over rationals and reals, two of our intermediate polynomials, based on satisfiability and Hamiltonian cycle, are not monotone affine polynomial-size projections of the permanent. This augments recent results along this line due to Grochow. Finally, we describe a (somewhat natural) polynomial defined independent of a computation model, and show that it is $\mathsf{VP}$-complete under polynomial-size projections. This complements a recent result of Durand et al. (2014) which established $\mathsf{VP}$-completeness of a related polynomial but under constant-depth oracle circuit reductions. Both polynomials are based on graph homomorphisms. A simple restriction yields a family similarly complete for $\mathsf{VBP}$.

cs.CC↗

arXiv2016

Sums of read-once formulas: How many summands suffice?

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

cs.CC↗

arXiv2015

Read-once polynomials: How many summands suffice?

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

cs.CC↗

arXiv2013

Algebraic Complexity Classes

This survey describes, at an introductory level, the algebraic complexity framework originally proposed by Leslie Valiant in 1979, and some of the insights that have been obtained more recently.

cs.CC↗

arXiv2013

Small Depth Proof Systems

A proof system for a language L is a function f such that Range(f) is exactly L. In this paper, we look at proofsystems 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(log log n) depth but with O(1) alternations (polylog 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 polylog 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 polylog 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.

cs.CC↗

arXiv2008

Longest paths in Planar DAGs in Unambiguous Logspace

We show via two different algorithms that finding the length of the longest path in planar directed acyclic graph (DAG) is in unambiguous logspace UL, and also in the complement class co-UL. The result extends to toroidal DAGs as well.

cs.CC↗