DROPS

Document

Short Paper

DOI: 10.4230/LIPIcs.SAT.2026.32

On Proof Systems for #QBF (Short Paper)

Authors: Sravanthi Chede, Leroy Chew, Vaibhav Krishan, and Anil Shukla

Published in: LIPIcs, Volume 377, 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)

Abstract

For a quantified Boolean formula (QBF), the problem of computing the number of winning strategies is known as the #QBF problem. This problem is considered harder than the analogous #SAT problem. Recently, important proof systems for QBFs and #SAT have been studied. By extending the ideas from both fields, we show that it is possible to design proof systems for #QBF. Such proof systems are important not only for advancing the theory of #QBF but also for certifying and designing better #QBF solvers, an area that is still in its early stages. In this paper, we explore #QBF proof systems to count the number of Skolem functions. In addition to a naive system, we study #QBF systems based on the ∀-expansion rule of QBFs. We observe that these systems have inherent structural weaknesses that lead to lower bounds. As an alternative, we propose a #QBF proof system that we call Q-MICE, which consists of sound inference rules for computing and certifying the #QBF solution, similar to the line-based #SAT proof system MICE. To demonstrate the strength of Q-MICE, we present various upper bounds, such as the quantified version of the propositional XOR-PAIRS formula, which are known to be hard for MICE. Consequently, we also separate Q-MICE from ∀-expansion based #QBF proof systems.

Cite as

Sravanthi Chede, Leroy Chew, Vaibhav Krishan, and Anil Shukla. On Proof Systems for #QBF (Short Paper). In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 32:1-32:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{chede_et_al:LIPIcs.SAT.2026.32,
  author =	{Chede, Sravanthi and Chew, Leroy and Krishan, Vaibhav and Shukla, Anil},
  title =	{{On Proof Systems for #QBF}},
  booktitle =	{29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
  pages =	{32:1--32:12},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-431-4},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{377},
  editor =	{Ignatiev, Alexey and Szeider, Stefan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.32},
  URN =		{urn:nbn:de:0030-drops-263380},
  doi =		{10.4230/LIPIcs.SAT.2026.32},
  annote =	{Keywords: QBF, Model Counting, Proof Systems, #QBF}
}

Document

DOI: 10.4230/LIPIcs.ITCS.2026.88

Lower Bounds and Separations for Torus Polynomials

Authors: Vaibhav Krishan and Sundar Vishwanathan

Published in: LIPIcs, Volume 362, 17th Innovations in Theoretical Computer Science Conference (ITCS 2026)

Abstract

The class ACC⁰ consists of Boolean functions that can be computed by constant-depth circuits of polynomial size with AND, NOT and MOD_m gates, where m is a natural number. At the frontier of our understanding lies a widely believed conjecture asserting that MAJORITY does not belong to ACC⁰. A few years ago, Bhrushundi, Hosseini, Lovett and Rao (ITCS 2019) introduced torus polynomial approximations as an approach towards this conjecture. Torus polynomials approximate Boolean functions when the fractional part of their value on Boolean points is close to half the value of the function. They reduced the conjecture that MAJORITY ∉ ACC⁰ to a conjecture concerning the non-existence of low degree torus polynomials that approximate MAJORITY. We reduce the non-existence problem further, to a statement about finding feasible solutions for an infinite family of linear programs. The main advantage of this statement is that it allows for incremental progress, which means finding feasible solutions for successively larger collections of these programs. As an immediate first step, we find feasible solutions for a large class of these linear programs, leaving only a finite set for further consideration. Our method is inspired by the method of dual polynomials, which is used to study the approximate degree of Boolean functions. Using our method, we also propose a way to progress further. We prove several additional key results with the same method, which include: - A lower bound on the degree of symmetric torus polynomials that approximate the AND function. As a consequence, we get a separation that symmetric torus polynomials are weaker than their asymmetric counterparts. - An error-degree trade-off for symmetric torus polynomials approximating the MAJORITY function, strengthening the corresponding result of Bhrushundi, Hosseini, Lovett and Rao (ITCS 2019). - The first lower bounds against torus polynomials approximating AND, showcasing the power of the machinery we develop. This lower bound nearly matches the corresponding upper bound. Hence, we get an almost complete characterization of the torus polynomial approximation degree of AND. - Lower bounds against asymmetric torus polynomials approximating MAJORITY, or AND, in the very low error regime. This partially answers a question posed in Bhrushundi, Hosseini, Lovett and Rao (ITCS 2019) about error-reduction for torus polynomials.

Cite as

Vaibhav Krishan and Sundar Vishwanathan. Lower Bounds and Separations for Torus Polynomials. In 17th Innovations in Theoretical Computer Science Conference (ITCS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 362, pp. 88:1-88:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{krishan_et_al:LIPIcs.ITCS.2026.88,
  author =	{Krishan, Vaibhav and Vishwanathan, Sundar},
  title =	{{Lower Bounds and Separations for Torus Polynomials}},
  booktitle =	{17th Innovations in Theoretical Computer Science Conference (ITCS 2026)},
  pages =	{88:1--88:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-410-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{362},
  editor =	{Saraf, Shubhangi},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2026.88},
  URN =		{urn:nbn:de:0030-drops-253751},
  doi =		{10.4230/LIPIcs.ITCS.2026.88},
  annote =	{Keywords: Circuit complexity, ACC, lower bounds, polynomials}
}

Document

DOI: 10.4230/LIPIcs.ITCS.2019.8

A #SAT Algorithm for Small Constant-Depth Circuits with PTF Gates

Authors: Swapnam Bajpai, Vaibhav Krishan, Deepanshu Kush, Nutan Limaye, and Srikanth Srinivasan

Published in: LIPIcs, Volume 124, 10th Innovations in Theoretical Computer Science Conference (ITCS 2019)

Abstract

We show that there is a zero-error randomized algorithm that, when given a small constant-depth Boolean circuit C made up of gates that compute constant-degree Polynomial Threshold functions or PTFs (i.e., Boolean functions that compute signs of constant-degree polynomials), counts the number of satisfying assignments to C in significantly better than brute-force time. Formally, for any constants d,k, there is an epsilon > 0 such that the zero-error randomized algorithm counts the number of satisfying assignments to a given depth-d circuit C made up of k-PTF gates such that C has size at most n^{1+epsilon}. The algorithm runs in time 2^{n-n^{Omega(epsilon)}}. Before our result, no algorithm for beating brute-force search was known for counting the number of satisfying assignments even for a single degree-k PTF (which is a depth-1 circuit of linear size). The main new tool is the use of a learning algorithm for learning degree-1 PTFs (or Linear Threshold Functions) using comparison queries due to Kane, Lovett, Moran and Zhang (FOCS 2017). We show that their ideas fit nicely into a memoization approach that yields the #SAT algorithms.

Cite as

Swapnam Bajpai, Vaibhav Krishan, Deepanshu Kush, Nutan Limaye, and Srikanth Srinivasan. A #SAT Algorithm for Small Constant-Depth Circuits with PTF Gates. In 10th Innovations in Theoretical Computer Science Conference (ITCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 124, pp. 8:1-8:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{bajpai_et_al:LIPIcs.ITCS.2019.8,
  author =	{Bajpai, Swapnam and Krishan, Vaibhav and Kush, Deepanshu and Limaye, Nutan and Srinivasan, Srikanth},
  title =	{{A #SAT Algorithm for Small Constant-Depth Circuits with PTF Gates}},
  booktitle =	{10th Innovations in Theoretical Computer Science Conference (ITCS 2019)},
  pages =	{8:1--8:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-095-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{124},
  editor =	{Blum, Avrim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2019.8},
  URN =		{urn:nbn:de:0030-drops-101010},
  doi =		{10.4230/LIPIcs.ITCS.2019.8},
  annote =	{Keywords: SAT, Polynomial Threshold Functions, Constant-depth Boolean Circuits, Linear Decision Trees, Zero-error randomized algorithms}
}

Search Results

Documents authored by Krishan, Vaibhav

On Proof Systems for #QBF (Short Paper)

Abstract

Cite as

Lower Bounds and Separations for Torus Polynomials

Abstract

Cite as

A #SAT Algorithm for Small Constant-Depth Circuits with PTF Gates

Abstract

Cite as

Thanks for your feedback!

Could not send message