Strategy extraction in QBF proof systems usually attempts to extract winning strategies from valid proofs. However, an alternative (and arguably more powerful) view is to extract Skolem/Herbrand functions, or equivalently synthesis of the game values at all intermediate points. In this paper, we investigate the existence and properties of such proof systems from which one can extract Skolem and Herbrand functions. We propose such a proof system for QBF, which we show is sound and complete, and from which extraction of Skolem/Herbrand functions can be performed, and game values computed, in polynomial time. We also show that this system is optimal among all proof systems that allow efficient extraction of Skolem/Herbrand functions. We provide conditional lower bound results for our new proof system and compare it to several existing/standard proof systems for QBF that have been studied in the literature, showing interesting orthogonality results. Finally, we provide a compilation algorithm that takes an arbitrary QBF and synthesizes a proof in our system, from which Skolem and Herbrand functions can be easily computed.

We describe a procedure that extracts existential strategies from verification proofs in the Long-Distance Consensus (i.e., Term Resolution) proof system when augmented with dependency schemes. We prove that when the standard dependency scheme 𝙳^std is used, the extracted strategies are winning strategies, thus establishing soundness of the proof system LDQ(D^std)-Consensus. We show through a counterexample that this approach fails to show soundness for LDQ(D^rrs)-Consensus.

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öhm-LMCS2023], formalises the reasoning in the QCDCL approach on false formulas, when neither cube-learning nor dependency schemes is used. The work of [BöhmPeitlBeyersdorff-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 (𝙳^{std} and 𝙳^{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 𝙳^{std} and 𝙳^{rrs} are investigated in detail and their relative strengths are analysed.

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 show that the deterministic query complexity of total search problems 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). Using our proof along with a decision-tree manipulation technique, we give a simple and self-contained proof that the $$\text{SearchCNF}$$ problem on random $$\text{k}$$ -CNF has pseudo-deterministic query complexity $$\Omega(n^{1/3})$$ ; a lower bound of $$\Omega(\sqrt{n})$$ is known, due to Goldwasser, Impagliazzo, Pitassi, and Santhanam (CCC'21), but via a significantly more complex proof. We improve the known separation between pseudo-deterministic and randomized decision tree size for total search problems in two ways: (1) We exhibit an $$\text{exp}(\widetilde{\Omega}(n^{1/4}))$$ separation for the $$\text{SearchCNF}$$ relation for random $$k$$ -CNFs. This seems to be the first exponential lower bound on the pseudo-deterministic size complexity of $$\text{SearchCNF}$$ associated with random $$k$$ -CNFs. (2) We exhibit an $${\text{exp}(\Omega(n))}$$ separation for the $$\text{ApproxHW}$$ relation. The previous best known separation for any relation was $${\text{exp}(\Omega(n^{1/2}))}$$ . We also separate pseudo-determinism from randomness in $$\text{AND}$$ and $$\text{CONJ}$$ decision trees, and determinism from pseudo-determinism in $$\text{Parity}$$ decision trees. Finally, for a hypercube colouring problem, that was introduced by Goldwasswer et al. to analyze the pseudo-deterministic complexity of a complete problem in $$\text{TFNPdt}$$ , we prove that either the monotone block-sensitivity or the anti-monotone block sensitivity is $${\Omega(n^{1/3})}$$ ; Goldwasser et al. showed an $${\Omega(n^{1/2})}$$ bound for general block-sensitivity.

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

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.

Abstract In Quantified Boolean Formulas QBFs, dependency schemes help to detect spurious or superfluous dependencies that are implied by the variable ordering in the quantifier prefix but are not essential for constructing countermodels. This detection can provably shorten refutations in specific proof systems, and is expected to speed up runs of QBF solvers. The proof system $$\texttt{QCDCL}$$ QCDCL recently defined by Beyersdorff and Boehm (LMCS 2023) abstracts the reasoning employed by QBF solvers based on conflict-driven clause-learning (CDCL) techniques. We show how to incorporate the use of dependency schemes into this proof system, either in a preprocessing phase, or in the propagations and clause learning, or both. We then show that when the reflexive resolution path dependency scheme $$\texttt{D}^{\texttt{rrs}}$$ D rrs is used, a mixed picture emerges: the proof systems that add $$\texttt{D}^{\texttt{rrs}}$$ D rrs to $$\texttt{QCDCL}$$ QCDCL in these three ways are not only incomparable with each other, but are also incomparable with the basic $$\texttt{QCDCL}$$ QCDCL proof system that does not use $$\texttt{D}^{\texttt{rrs}}$$ D rrs at all, as well as with several other resolution-based QBF proof systems. A notable fact is that all our separations are achieved through QBFs with bounded quantifier alternation.

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

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.

We provide a tight characterisation of proof size in resolution for quantified Boolean formulas (QBF) via circuit complexity. Such a characterisation was previously obtained for a hierarchy of QBF Frege systems [ 16 ], but leaving open the most important case of QBF resolution. Different from the Frege case, our characterisation uses a new version of decision lists as its circuit model, which is stronger than the CNFs the system works with. Our decision list model is well suited to compute countermodels for QBFs. Our characterisation works for both Q-Resolution and QU-Resolution. Using our characterisation, we obtain a size-width relation for QBF resolution in the spirit of the celebrated result for propositional resolution [ 4 ]. However, our result is not just a replication of the propositional relation—intriguingly ruled out for QBF in previous research [ 12 ]—but shows a different dependence between size, width, and quantifier complexity. An essential ingredient is an improved relation between the size and width of term decision lists; this may be of independent interest. We demonstrate that our new technique elegantly reproves known QBF hardness results and unifies previous lower-bound techniques in the QBF domain.

We study the MaxSAT Resolution (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 semi-algebraic 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.

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

Abstract Strategy extraction is of great importance for quantified Boolean formulas (QBF), both in solving and proof complexity. So far in the QBF literature, strategy extraction has been algorithmically performedfromproofs. Here we devise the first QBF system where (partial) strategies are builtintothe proof and are piecewise constructed by simple operations along with the derivation. This has several advantages: (1) lines of our calculus have a clear semantic meaning as they are accompanied by semantic objects; (2) partial strategies are represented succinctly (in contrast to some previous approaches); (3) our calculus has strategy extraction by design; and (4) the partial strategies allow new sound inference steps which are disallowed in previous central QBF calculi such as Q-Resolution and long-distance Q-Resolution. The last item (4) allows us to show an exponential separation between our new system and the previously studied reductionless long-distance resolution calculus. Our approach also naturally lifts to dependency QBFs (DQBF), where it yields the first sound and complete CDCL-style calculus for DQBF, thus opening future avenues into CDCL-based DQBF solving.

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.

We prove the first 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 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 ∀Exp+Res and IR.

We provide a tight characterisation of proof size in resolution for quantified Boolean formulas (QBF) by circuit complexity. Such a characterisation was previously obtained for a hierarchy of QBF Frege systems (Beyersdorff & Pich, LICS 2016), but leaving open the most important case of QBF resolution. Different from the Frege case, our characterisation uses a new version of decision lists as its circuit model, which is stronger than the CNFs the system works with. Our decision list model is well suited to compute countermodels for QBFs.

How do we prove that a false QBF is inded false? How big a proof is needed? The special case when all quantifiers are existential is the well-studied setting of propositional proof complexity. Expectedly, universal quantifiers change the game significantly. Several proof systems have been designed in the last couple of decades to handle QBFs. Lower bound paradigms from propositional proof complexity cannot always be extended - in most cases feasible interpolation and consequent transfer of circuit lower bounds works, but obtaining lower bounds on size by providing lower bounds on width fails dramatically. A new paradigm with no analogue in the propositional world has emerged in the form of strategy extraction, allowing for transfer of circuit lower bounds, as well as obtaining independent genuine QBF lower bounds based on a semantic cost measure. This talk will provide a broad overview of some of these developments.

The ground-breaking paper “Short Proofs Are Narrow -- Resolution Made Simple” by Ben-Sasson and Wigderson (J. ACM 2001) introduces what is today arguably the main technique to obtain resolution lower bounds: to show a lower bound for the width of proofs. Another important measure for resolution is space, and in their fundamental work, Atserias and Dalmau (J. Comput. Syst. Sci. 2008) show that lower bounds for space again can be obtained via lower bounds for width. In this article, we assess whether similar techniques are effective for resolution calculi for quantified Boolean formulas (QBFs). There are a number of different QBF resolution calculi like Q-resolution (the classical extension of propositional resolution to QBF) and the more recent calculi ∀Exp+Res and IR-calc. For these systems, a mixed picture emerges. Our main results show that the relations both between size and width and between space and width drastically fail in Q-resolution, even in its weaker tree-like version. On the other hand, we obtain positive results for the expansion-based resolution systems ∀Exp+Res and IR-calc, however, only in the weak tree-like models. Technically, our negative results rely on showing width lower bounds together with simultaneous upper bounds for size and space. For our positive results, we exhibit space and width-preserving simulations between QBF resolution calculi.

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.

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.

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.

We define a cutting planes system CP+ForallRed for quantified Boolean formulas (QBF) 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+ForallRed 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 ForallExp+Res. Technically, our results establish the effectiveness of two lower bound techniques for CP+ForallRed: via strategy extraction and via monotone feasible interpolation.

The groundbreaking paper 'Short proofs are narrow - resolution made simple' by Ben-Sasson and Wigderson (J. ACM 2001) introduces what is today arguably the main technique to obtain resolution lower bounds: to show a lower bound for the width of proofs. Another important measure for resolution is space, and in their fundamental work, Atserias and Dalmau (J. Comput. Syst. Sci. 2008) show that space lower bounds again can be obtained via width lower bounds. Here we assess whether similar techniques are effective for resolution calculi for quantified Boolean formulas (QBF). A mixed picture emerges. Our main results show that both the relations between size and width as well as between space and width drastically fail in Q-resolution, even in its weaker tree-like version. On the other hand, we obtain positive results for the expansion-based resolution systems Forall-Exp+Res and IR-calc, however only in the weak tree-like models. Technically, our negative results rely on showing width lower bounds together with simultaneous upper bounds for size and space. For our positive results we exhibit space and width-preserving simulations between QBF resolution calculi.

The VP versus VNP question, introduced by Valiant, is probably the most important open question in algebraic complexity theory. Thanks to completeness results, a variant of this question, VBP versus VNP, can be succinctly restated as asking whether the permanent of a generic matrix can be written as a determinant of a matrix of polynomially bounded size. Strikingly, this restatement does not mention any notion of computational model. To get a similar restatement for the original and more fundamental question, and also to better understand the class itself, we need a complete polynomial for VP. Ad hoc constructions yielding complete polynomials were known, but not natural examples in the vein of the determinant. We give here several variants of natural complete polynomials for VP, based on the notion of graph homomorphism polynomials.

This proceedings volume has the papers presented at the 30th annual conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010), held at the Institute of Mathematical Sciences (IMSc), Chennai, during 15–18 December 2010. The conference attracted 128 submissions from 35 countries in 6 continents, most of them of very high quality. We thank the authors who submitted for making this such a competitive conference. The PC succeeded in obtaining the help of 216 external reviewers, in all producing 400 referee reports which were of immeasurable help in deciding the 38 contributed papers which have made it to this publication.

It has been known for a long time now that the problem of counting the number of perfect matchings in a planar graph is in NC.This result is based on the notion of a pfaffian orientation of a graph.(Recently, Galluccio and Loebl [7] gave a P-time algorithm for the case of graphs of small genus.)However, it is not known if the corresponding search problem, that of finding one perfect matching in a planar graph, is in NC.This situation is intriguing as it seems to contradict our intuition that search should be easier than counting.For the case of planar bipartite graphs, Miller and Naor [22] showed that a perfect matching can indeed be found using an NC algorithm.We present a very different NG-algorithm for this problem.Unlike the Miller-Naor algorithm, our approach directly uses the fact that counting is in NC, and it also generalizes to the problem of finding a perfect matching in a bipartite graph of small (O(log n)) genus.It also rekindles the hope for an NC-algorithm to find a perfect matching in a non-bipartite planar graph.Along the way, we modify the algorithm of Gallucio and Loebl [7] to show that counting the number of perfect matchings in graphs of small genus is in NC.

In this paper we approach the problem of computing the characteristic polynomial of a matrix from the combinatorial viewpoint. We present several combinatorial characterizations of the coefficients of the characteristic polynomial in terms of walks and closed walks of different kinds in the underlying graph. We develop algorithms based on these characterizations and show that they tally with well-known algorithms arrived at independently from considerations in linear algebra.

Systolic pyramid automata accepting square arrays are defined. Homogeneous and semi-homogeneous pyramid automata are shown to have equal power though regular pyramid automata are more powerful. Languages accepted by these automata are compared with languages generated by array grammars and languages accepted by one-way 2-D cellular automata. Hexagonal pyramid automata are also considered and are shown to accept some languages generated by hexagonal array grammars.