Vaibhav Krishan

I am currently a Postdoc at the Theoretical Computer Science department of The Institute of Mathematical Sciences in Chennai, India. Before this, I obtained a PhD student from the Computer Science and Engineering department of Indian Institute of Technology Bombay, where I was very fortunate to be advised by Prof. Nutan Limaye and Prof. Sundar Vishwanathan. Before joining for PhD, I worked as a quantitative trader for a high frequency trading firm, and as a data scientist, for overall four years of experience. I obtained my undergraduate degree from the department of Computer Science and Engineering at Indian Institute of Technology Bombay.

I am broadly interested in theoretical computer science and how it can inform the design of practical systems. In particular, I find "hardness" in computation quite fascinating, and how practical systems can solve such problems inspite of theoretical hardness. Currently, I'm working on questions in Boolean circuit complexity, proof complexity, and QBF solving. Some other areas I like are derandomisation, meta-complexity and pseudorandomness.

[DBLP], [Google Scholar], [ECCC (IIT Bombay account), ECCC (Personal account)], [ORCID]

Contact:

• vaibhkrishan [AT] gmail [DOT] com. (recommended)

• vaibhavk [AT] imsc [DOT] res [DOT] in.

Publications

On Proof Systems for #QBF with Sravanthi Chede, Leroy Chew and Anil Shukla

• [ECCC], [Summary]

Summary: We design the first theoretical proof system capable of counting the number of winning strategies in a two-player game, encoded as a quantified Boolean formula. We show how this system can efficiently count the winning strategies for various QBFs that would be hard for simpler proof systems.

• The 29th International Conference on Theory and Applications of Satisfiability Testing, 2026 (to appear)

  • paper

Degree Lower Bounds for Torus Polynomials and MAJORITY vs ACC⁰ with Sundar Vishwanathan

• [ECCC], [Summary]

Summary: We propose an incremental approach to prove lower bounds against torus polynomials approximating the MAJORITY function, aiming to separate it from ACC⁰. The method also allows us to prove lower bounds for AND and that symmetric torus polynomials are weaker than their asymmetric counterparts.

• In The 17th Innovations in Theoretical Computer Science Conference, ITCS 2026

  • Title: Lower Bounds and Separations for Torus Polynomials

  • Proceedings version (local) , Slides, Video

\(\mathsf{MidBit}^+\), Torus Polynomials and Non-classical Polynomials: Equivalences for ACC Lower Bounds

• [ECCC], [Summary]

Summary: We prove that a function can be approximated by non-classical polynomials if and only if it can be approximated by a \(\mathsf{MidBit}^+\) circuit and setup a correspondence between relevant parameters for both models.

Upper Bound for Torus Polynomials

• [ECCC], [Summary]

Summary: We prove that functions that can be approximated within low error by torus polynomials of low degree, are in \(\mathsf{MidBit}^+\).

• In The 16th International Computer Science Symposium in Russia, CSR 2021

  • Proceedings version (local) , Slides

A #SAT Algorithm for Small Constant-Depth Circuits with PTF gates with Swapnam Bajpai, Deepanshu Kush, Nutan Limaye and Srikanth Srinivasan

• [ECCC], [Arxiv], [Summary]

Summary: We prove a better-than-brute-force satisfiability algorithm for constant degree polynomial threshold functions, and constant depth, with size slightly super-linear, circuits composed of constant degree polynomial threshold functions. A Boolean function is a polynomial threshold function if there is a polynomial such that the function evaluates to “true” if and only if the polynomial evaluates to a negative value. A satisfiability algorithm decides whether the Boolean function represented by the polynomial or the circuit evaluates to “true” on some input. A better-than-brute-force algorithm runs asymptotically much faster than simply evaluating the function over an enumeration of its inputs (aka brute-force).

• In The 10th Innovations in Theoretical Computer Science Conference, ITCS 2019

  • Proceedings version (local) , Slides, Poster

• In Algorithmica 84, 2022

  • Journal version (local)

Isolation Lemma for Directed Reachability and NL vs. L with Nutan Limaye

• [ECCC], [Summary]

Summary: We prove that an L/poly randomized procedure for isolating an s-t path for directed graphs with success probability at least 2/3 implies \(NL \subseteq L/poly\). L is the class of functions decidable by algorithms that use only logarithmic amount of space, NL is the non-deterministic version and L/poly is the non-uniform version. An algorithm for isolating an s-t path on a directed graph outputs another directed graph on the same set of nodes such that exactly one s-t path survives, provided that there was an s-t path to start with. We prove a similat result for LogCFL, a class related to push down automata.