{'fraction_non_alphanumeric': 0.04186784729763595, 'fraction_numerical': 0.014200985715479075, 'mean_word_length': 3.61744966442953, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 12, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Proof Complexity Modulo the Polynomial Hierarchy: Understanding Alternation as a Source of Hardness

We present and study a framework in which one can present alternation-based lower bounds on proof length in proof systems for quantified Boolean formulas. A key notion in this framework is that of proof system ensemble, which is (essentially) a sequence of proof systems where, for each, proof checking can be performed in the polynomial hierarchy. We introduce a proof system ensemble called relaxing QU-res which is based on the established proof system QU-resolution. Our main results include an exponential separation of the tree-like and general versions of relaxing QU-res, and an exponential lower bound for relaxing QU-res; these are analogs of classical results in propositional proof complexity.


Introduction
Background. Traditionally, the area of propositional proof complexity studies proof length in propositional proof systems for certifying the unsatisfiability of instances of the SAT problem, which instances are quantifier-free propositional formulas [14,5,24]. This line of study is supported by multiple motivations; let us highlight a few. First, while satisfiable formulas can be easily certified by a satisfying assignment, it is also natural to desire efficiently verifiable proofs for unsatisfiable formulas (for instance, to check that a SAT algorithm judged unsatisfiability correctly); understanding whether and when proof systems have succinct proofs is a prime concern of this area. Relatedly, SAT algorithms for deciding the SAT problem can be typically shown to implicitly generate proofs in a proof system, and thus insight into proof length in the resulting proof system can be used to gain insight into the running-time behavior of SAT algorithms (see for example the discussions in [4,1]). In addition, the question of whether or not there are proof systems admitting polynomially bounded proofs is (when formalized) equivalent to the question of whether or not NP is equal to coNP [14], and one can thus suggest that studying proof length in propositional proof systems sheds light on the relationship between these two complexity classes.
Over recent years, researchers have devoted increasing attention to methods for solving the QBF problem, a generalization of the SAT problem and a canonical PSPACE-complete problem; an instance of this problem is a propositional formula where each variable is either existentially or universally quantified. (QBF is short for quantified Boolean formula.) It is often suggested that the move to studying this more general problem is based on advances in the efficacy of SAT algorithms (see for example [25]). As reinforces this suggestion, let us point out that one can find QBF solution techniques which use SAT algorithms as blackbox, primitive components, and hence which arguably conceive of and treat the SAT problem as feasibly solvable. For instance, sKizzo, a QBF solver dating back to 2005, would convert the QBF being processed to a SAT instance and then call a SAT solver, whenever this was affordable [8]. As another example, a different QBF solver which extensively calls a SAT solver during a backtrack-style search was developed and studied [23].
The rise in the study of the QBF problem has resulted in the identification of a number of core algorithmic techniques and corresponding proof systems that aim to capture these (see for example [12,16,15,21,3,19,9] and the references therein). We refer to these proof systems as QBF proof systems; they can be used as a basis for certifying a decision for a QBF instance. One can motivate the study of QBF proof systems in much the same way that the study of propositional proof systems has been motivated; hence, these QBF proof systems would seem to suggest a new chapter in the study of proof complexity, and a new domain for the existing lines of inquiry thereof.
However, one is immediately confronted with a dilemma upon inspecting the very basic question of whether or not a typical QBF proof system requires long (exponentially sized) proofs-again, a primary type of question in traditional proof complexity. As an example, let us discuss Q-resolution [12], a QBF proof system which is heavily studied and used, in both theory and practice (see for example [2,17,16,20,21,3,9] and the references therein). When applied to non-quantified formulas (viewed as instances of QBF by existentially quantifying all variables), Q-resolution behaves identically to resolution (a heavily studied propositional proof system), and hence the known exponential lower bounds on resolution proof length [18,7] transfer immediately to Q-resolution. This observation leaves one with a lingering sentimentwhich is often expressed by members of the community-that there is something left to be said. After all, Q-resolution is defined on QBF instances, which are substantially more general than SAT instances; the observation does not yield any information about how Q-resolution handles this extra generality, that is, how it copes with alternation of quantifiers. Indeed, there is a sharp disconnect between observing a lower bound for a QBF proof system via a set of SAT instances, and the mentioned treatment of the SAT problem, by QBF algorithms, as a feasibly solvable primitive. These considerations naturally lead to the question of whether or not one can formulate and prove a lower bound which arises from alternation.

Contributions.
In this article, we present and study a framework in which it is possible to present such alternation-based lower bounds on proof length in QBF proof systems.
We define a proof system ensemble to be a collection of proof systems, where in each proof system, whether or not a given string π constitutes a proof of a given formula Φ can be checked in the polynomial hierarchy (Definition 3.1). A proof system ensemble is considered to have polynomially bounded proofs (for a language) if it contains a proof system which has polynomially bounded proofs in the usual sense (Definition 3.3). As a result, it is straightforward to define proof system ensembles that have succinct proofs for any set of QBFs with bounded alternation, such as a set of SAT instances (and the proof system ensembles studied here all have this property); this in turn forces proof length lower bounds, by nature, to arise from a proof system's inability to cope with quantifier alternation. In terms of complexity classes, the question of whether or not there exists a polynomially bounded proof system ensemble for the QBF problem (or any other PSPACE-complete problem) is equivalent to the question of whether or not PSPACE is contained in PH, the polynomial hierarchy (Proposition 3.4). Indeed, the relationship that traditional proof complexity bears to the NP equals coNP question is analogous to the relationship between the present framework and the PSPACE equals PH question. (Let us point out that no direct implication is known between these two open questions, and so, in a certain sense, progress in one framework may proceed orthogonally to progress in the other!) One of our main motivations in pursuing this work was to gain further insight into Q-resolution; here, we focus on a slight extension, QU-resolution [16], where from existing clauses one can derive new clauses by a rule for eliminating literals on universally quantified variables and by resolution on any variable (in Q-resolution, one can only resolve on existentially quantified variables). Q-resolution, QU-resolution, and their relatives are typically defined only for clausal QBFs-QBFs that consist of a quantifier prefix followed by a conjunction of clauses. We show how to parameterize and lift QU-resolution to obtain a proof system ensemble which is in fact defined on arbitrary QBFs (indeed, it is defined on what we call quantified Boolean circuits), and not just those in clausal form. This is done by defining an axiom of a QBF to be a clause which is, in a certain precise sense, entailed by the QBF (see Section 4.1). We then define, for each QBF Φ and for each k ě 2, a set of axioms, denoted by HpΦ, Π k q, which contain increasingly more axioms as k increases. This gives us a sequence of versions of QU-resolution: for each k, we obtain a version by defining a proof to be a sequence of clauses derived from the axioms HpΦ, Π k q and the two aforementioned rules. This sequence forms our main proof system ensemble, which we call relaxing QU-res.
Let us remark that the definition of the axiom sets HpΦ, Π k q is based on what we call relaxations of QBFs; the way these are defined, it automatically holds that the empty clause is an axiom in HpΦ, Π k q whenever Φ is a false QBF whose quantifier prefix is Π k . Consequently, relaxing QU-res is polynomially bounded on any set of false QBFs having bounded alternation (this is discussed in Section 4.2). Let us also note that although here we explicitly lift QU-resolution to a proof system ensemble, the approach that we take here can be applied to analogously lift any proof system which is based on deriving clauses from a set of axiom clauses.
Apart from the formulation of the framework, our main results are as follows. We prove an exponential separation between the tree-like and general versions of relaxing QU-res (Section 6), by exhibiting a set of formulas which have polynomial size QU-resolution proofs, but which require exponential size proofs in tree-like relaxing QU-res; this gives an alternation-based analog of the known separation between treelike and general resolution [11,6]. Tree-like QU-resolution proofs can be viewed as the traces of a natural backtrack-style QBF decision procedure (this is evident from the viewpoint in Section 4.3, and is also developed explicitly in [13,Section 4.3]), and so this separation formally differentiates the power of such backtracking and general QU-resolution. The lower bound of this separation is based on a prover-delayer game for tree-like QU-resolution proofs (Section 5), which can be viewed as a generalization of a known prover-delayer game for tree-like resolution [22]; note that independently and very recently, a game similar to ours was presented for tree-like Q-resolution [10]. We also prove an exponential lower bound for relaxing QU-res (Section 7).
All in all, the ideas and techniques developed in this work draw upon and interface concepts from two-player game interaction, proof complexity, and quantified propositional logic. We believe that further progress could benefit from creative input from each of these areas, and certainly look forward to future research on the presented framework.

Preliminaries
For each integer k, we use rks to denote the set that is equal to t1, . . . , ku when k ě 1, and that is equal to the empty set H when k ă 1.
We use dompf q to indicate the domain of a function. A function f is a restriction of a function g if dompf q Ď dompgq and, for each a P dompf q, it holds that gpaq " f paq; when this holds, we also say that g is an extension of f . We write f ae S to denote the restriction of a function f to the set S. We say that two functions f and g agree if for each element a P dompf q X dompgq, it holds that f paq " gpaq.
When A and B are sets, we use rA Ñ Bs to denote the set of functions from A to B.
Clauses. In this article, we employ the following terminology to discuss clauses. A literal is a propositional variable v or the negation v thereof. A clause is a disjunction of literals that contains, for each variable, at most one literal on the variable. A clause is sometimes viewed as the set of the literals that it contains; two clauses are considered equal if they are equal as sets. A clause is empty if it does not contain any literals. The variables of a clause are simply the variables that underlie the clause's literals, and the set of variables of a clause α is denoted by varspαq. When α is a clause, we use assignpαq to denote the unique propositional assignment f with dompf q " varspαq such that α evaluates to false under f . In the other direction, when f is a propositional assignment, we use clausepf q to denote the unique clause α with varspαq " dompf q that evaluates to false under f . We will freely and tacitly interchange between a clause α and its corresponding assignment assignpαq. A clause γ is a resolvent of two propositional clauses α and β on variable v if there exists a literal L P α such that its complement M is in β, γ " pαztLuq Y pβztM uq, and v is the variable underlying L and M .
Quantified Boolean circuits and formulas. We assume basic familiarity with quantified propositional logic. A QBC (short for quantified Boolean circuit) consists of a quantifier prefix P " Q 1 v 1 . . . Q n v n , where each Q i is a quantifier in t@, Du and each v i is a propositional variable; and, a Boolean circuit φ built from the constants 0 and 1, propositional variables among tv 1 , . . . , v n u, and the gates AND (^), OR (_), and NOT ( ). We refer to the computational problem of deciding whether or not a QBC is false as the QBC problem. For brevity, we sometimes refer to existentially quantified variables as D-variables, and universally quantified variables as @-variables. While it is typical to notate a QBC by simply specifying the prefix P immediately followed by the circuit φ, we will typically separate these two parts by a colon for the sake of readability, using for example P : φ. We assume that each quantifier prefix does not contain repeated variables. When Φ " P : φ is a QBC, by a partial assignment of Φ, we refer to a propositional assignment f : S Ñ t0, 1u defined on a subset S of the variables appearing in P . A QBF is a QBC P : φ where φ is a Boolean formula. A clausal QBF is a QBF P : φ where φ is the conjunction of clauses.
Quantifier prefixes. Let i ě 1. A quantifier prefix P " Q 1 v 1 . . . Q n v n is Π i if Q 1 . . . Q n , viewed as a string over the alphabet t@, Du, is contained in the language denoted by the regular expression @˚D˚@˚D˚. . ., which contains i starred quantifiers, beginning with @˚and alternating; Σ i is defined similarly, but with respect to the regular expression D˚@˚D˚@˚. . .. The following notation is relative to a quantifier prefix P " Q 1 v 1 . . . Q n v n ; when we use it, the prefix will be clear from context. We write v i ĺ v j if i ď j or if j ă i and Q j " Q j`1 "¨¨¨" Q i . We extend this binary relation (and others) to sets in the following natural way: when U and V are sets of variables, we write U ĺ V if for each u P U and each v P V , it holds that u ĺ v. We also write, for example, that It is straightforward to verify that " is an equivalence relation; we refer to each equivalence class of " as a quantifier block. We When S is a set of variables, we use lastpSq to denote the variable of S appearing last in the quantifier prefix, that is, the variable v m , where m " maxti | v i P Su. Typically, when we use the function lastpSq, it is in conjunction with the just-defined binary relations, and hence what is most relevant will be the relative location of the quantifier block of lastpSq.
Strategies. Let Φ " P : φ be a QBC; let X denote the D-variables of Φ, and let Y denote the @-variables of Φ. When x P X, define Y ăx to be the set of variables ty P Y | y ň xu; dually, when y P Y , define X ăy to be the set of variables tx P X | x ň yu.
An D-strategy is a sequence of mappings σ " pσ x q xPX where each σ x is a mapping from rY ăx Ñ t0, 1us to t0, 1u. When τ : Y Ñ t0, 1u is an assignment to the universally quantified variables, we use xσ, τ y to denote the assignment f defined by f pyq " τ pyq for each y P Y and f pxq " σ x pτ ae Y ăx q for each x P X. We say that pσ x q xPX is a winning D-strategy if for every assignment τ : Y Ñ t0, 1u, it holds that the assignment xσ, τ y satisfies φ. A model of Φ is defined to be a winning D-strategy of Φ.
Dually, we define a @-strategy to be a sequence of mappings τ " pτ y q yPY where each τ y is a mapping from rX ăy Ñ t0, 1us to t0, 1u. When σ : X Ñ t0, 1u is an assignment to the existentially quantified variables, we use xτ, σy to denote the assignment f defined by f pxq " σpxq for each x P X and f pyq " τ y pσ ae X ăy q for each y P Y . We say that pσ y q yPY is a winning @-strategy if for every assignment σ : X Ñ t0, 1u, it holds that the assignment xτ, σy falsifies φ.
The following are well-known facts that we will treat as basic.
• There exists a winning D-strategy for Φ (that is, a model of Φ) if and only if Φ is true.
• There exists a winning @-strategy for Φ if and only if Φ is false.

Proof system ensembles
In this section, we formalize the notion of proof system ensemble and present some basic associated notions. For each m P N, let us fix Spmq to be a Σ p m -complete problem, such as the QBC problem restricted to QBCs having a Σ m prefix. Let O be a language; when discussing an algorithm A that makes oracle calls, we use A O to denote the instantiation of A where oracle calls are answered according to O. Definition 3.1 A proof system ensemble for a language L consists of an algorithm A which may make oracle calls and receives inputs of the form pk, px, πqq where k P N and x and π are strings; and, a computable function r : N Ñ N such that: • For each k P N, there exists a polynomial p k such that (for each pair px, πq) the algorithm A Sprpkqq halts on an input pk, px, πqq within time p k p|px, πq|q.
• For each k P N, when L k is set to tpx, πq | pk, px, πqq is accepted by A Sprpkq u, it holds that the language tx | Dπ such that px, πq P L k u is equal to L.

Definition 3.2 Let
S be a set of functions from N to N. A proof system ensemble pA, rq requires proofs of size S on a set tΦ 1 , Φ 2 , . . .u of instances if for each k, there exists s P S such that pk, pΦ n , πqq P L k implies |π| ě spnq. Here, |π| denotes the size of π. We may also apply this terminology to other measures defined on proofs.
We say that a function f mapping strings to strings is a polynomial-length function if there exists a polynomial q such that, for each string x, it holds that |f pxq| ď qp|x|q. Definition 3.3 A proof system ensemble pA, rq polynomially bounded on a language L if there exists k P N and there exists a polynomial-length function f such that the following holds: if x P L, then it holds that px, f pxqq P L k , where L k is defined as in Definition 3.1.

Proposition 3.4 There exists a polynomially bounded proof system ensemble for a language L if and only if L is in the polynomial hierarchy.
We next define notions of simulation between proof systems. Definition 3.5 Let pA, rq and pA 1 , r 1 q be proof system ensembles for a language L.
We say that pA 1 , r 1 q simulates pA, rq if there exists a function f : N Ñ N and a sequence of polynomial length functions pg k q kPN from strings to strings such that, for each px, πq P L k , it holds that px, g k pπqq P L 1 f pkq . Here, L k and L 1 k are defined as in Definition 3.1, for pA, rq and pA 1 , r 1 q, respectively. We say that pA 1 , r 1 q effectively simulates pA, rq if, in addition, the function f is computable and there is an algorithm that, for each k P N, computes g k pxq from x within time p k p|x|q, where p k is a polynomial.
Let us remark that variations on Definitions 3.1 and 3.5 are certainly possible. For example, one could require that the bounding polynomials pp k q in Definition 3.1 be computable, as a function of k. Perhaps more interestingly, observe that no assumption is placed on how these polynomials pp k q behave in aggregate; one could, for instance, require that their degrees are all bounded above by a constant, obtaining a definition reminiscent of that of fixed-parameter tractability. A similar comment can be offered for the polynomials associated to the functions pg k q from Definition 3.5.

Relaxing QU-resolution 4.1 QU-resolution
Let Φ " P : φ be a QBC. We define an axiom set of Φ to be a set H of clauses on variables of P such that, for each C P H, C is an axiom of Φ in the following sense: each model of P : φ is a model of P : C. Let us give examples. First, if the QBC Φ is false, then the empty clause is an axiom of Φ. Second, if C is any clause which is entailed by φ, then C is an axiom of Φ. A case of this is when a is an assignment to all variables of Φ that falsifies φ; then, clausepaq is entailed by φ and is an axiom of Φ.
Relative to a QBC Φ " P : φ, we say that a clause C is obtainable from a second clause D by @elimination if there exists a literal L P D such that C " DztLu and the variable y underlying L has dompassignpCqq ĺ y.
With these notions, we define QU-resolution for quantified Boolean circuits in the following way.

Definition 4.1
A QU-resolution proof of a QBC Φ " P : φ from an axiom set H (of Φ) is a finite sequence of clauses where each clause is either in H, is obtainable from a previous clause by @-elimination, or is obtainable from two previous clauses as a resolvent. The size of such a proof is defined as the number of clauses. Such a proof is said to be a falsity proof if it ends with the empty clause.
Note that in the case that Φ is a clausal QBF, when H is the set of clauses appearing in Φ, Definition 4.1 essentially coincides with usual definitions of QU-resolution in the literature (see for example [20]). The only difference is that here, applying @-elimination eliminates just one universally quantified variable of a clause, whereas many authors speak of @-reduction, which (when applied to a clause) eliminates each universally quantified variable that come after all existentially quantified variables. One can simulate an instance of @-reduction by applying @-elimination repeatedly.
It is a folklore fact that when one has a clausal QBF Φ " P : φ with clauses H, and C appears in a QU-resolution proof of Φ from H, then any model of Φ is a model of P : C. From this fact and the definition of axiom set, we immediately obtain the following proposition.

Relaxing
In order to define a proof system ensemble based on QU-resolution proofs, we now describe how to obtain a sequence of axiom sets for a given QBC. We start by exhibiting a way to infer that a partial assignment is an axiom of a QBC.
Let a be a partial assignment of a QBC Φ " P : φ. Define P ras to be the quantifier prefix which is equal to P but where the variables in dompaq and their corresponding quantifiers are removed, and where each quantifier of a variable v with v ň lastpaq is changed (if necessary) to an existential quantifier. As examples, when P " @y 1 Dx 1 Dx 2 @y 2 @y 3 Dx 3 , if a is an assignment with dompaq " tx 1 , y 3 u, it holds that P ras " Dy 1 Dx 2 @y 2 Dx 3 ; if a is an assignment with dompaq " tx 1 , x 2 u, it holds that P ras " Dy 1 @y 2 @y 3 Dx 3 . Define φras to be equivalent to φ, but where each variable v P dompaq is replaced with the constant apvq. Define Φras to be P ras : φras.

Proposition 4.3
Assume that a is a partial assignment of a QBC Φ " P : φ such that Φras is false. Then clausepaq is an axiom of Φ, that is, each model of P : φ is a model of P : clausepaq. Proposition 4.3 can be proved in the following way. Fix a model σ " pσ x q xPX of P : φ; here, X denotes the D-variables in P . Suppose (for a contradiction) that τ is an assignment to the @-variables of P : φ such that the assignment f " xσ, τ y falsifies clausepaq, or equivalently, f extends the assignment a. Then, we define a winning D-strategy σ 1 for Φras as follows. Define σ 1 x to be the function obtained from σ x after fixing each @-variable y P dompaq Y tv | v ň lastpaqu to τ pyq; and, for each @-variable y with y ň lastpaq (that is, for each @-variable in P that is changed to an D-variable in P ras), define σ 1 y to be τ pyq. Prima facie, Proposition 4.3 may appear to be of limited utility; even if one has oracle access to a level of the polynomial hierarchy, it may be that many partial assignments a give rise to a quantifier prefix P ras which has too many alternations to be resolved by the oracle. In order to expand the class of axioms derivable by this proposition (relative to such an oracle), we introduce the notion of a relaxation of a QBC, as follows. A relaxation of a quantifier prefix P " Q 1 v 1 . . . Q n v n is a quantifier prefix which has the form P 1 " Q πp1q v πp1q . . . Q πpnq v πpnq where π : rns Ñ rns is a permutation and where, for each @-variable y and for each D-variable x, it holds that y ĺ x implies y ĺ 1 x; here, ĺ and ĺ 1 denote the binary relations of P and P 1 , respectively. A relaxation of a QBC P : φ is a QBC of the form P 1 : φ where P 1 is a relaxation of P ; such a QBC is said to be a Π i -relaxation if P 1 is Π i . The following is straightforward to verify.

Proposition 4.4 If a relaxation of a QBC Φ is false, then the QBC Φ is false.
Let Φ be a QBC; for k ě 2, we define HpΦ, Π k q to be the set that contains a clause C if there exists a Π k -relaxation of ΦrassignpCqs that is false. The following fact follows immediately from Propositions 4.3 and 4.4.

Proposition 4.5
When Φ is a QBC and k ě 2, it holds that HpΦ, Π k q is an axiom set of Φ.
Note that when Φ " P : φ is a clausal QBF, C is a clause in φ, and a " assignpCq, it holds that φras is unsatisfiable; consequently, for any quantifier prefix P 1 on the variables of φras, it holds that P 1 : φras is false, and thus C P HpΦ, Π 2 q. Hence, the set HpΦ, Π 2 q contains each clause of φ.

Definition 4.6
Relaxing QU-res is defined as the pair pA, rq where r is defined by rpkq " k`3 and A is an algorithm defined to accept an input pk, pΦ, πqq if Φ is a QBC and π is a QU-resolution falsity proof of x from axioms in HpΦ, Π k`2 q. In particular, the algorithm A examines each clause in π in order; when a clause C is not derived from previous ones by resolution or by @-elimination, membership of C in HpΦ, Π k`2 q is checked by the Σ k`3 oracle (note that a relaxation can be guessed nondeterministically).

Proposition 4.7
Relaxing QU-res is a proof system ensemble for the QBC problem.
Note that for any set F of false QBCs having bounded alternation, it holds that relaxing QU-res is polynomially bounded on F. Why? Let k be a value such that each QBC in F is Π k`2 . For each QBC Φ P F, we have that the empty clause is in HpΦ, Π k`2 q, since Φ itself is a false Π k`2 -relaxation of Φ. Hence, for each such QBC Φ, the algorithm A of relaxing QU-res accepts pk, pΦ, Hqq, where here H denotes the proof consisting just of the empty clause.
Let us now introduce some notions which will be used in our study of tree-like relaxing QU-res (defined below). Let f and g be partial assignments of a QBC Φ. We say that g is a semicompletion of f if g is an extension of f such that for each universally quantified variable y with dompf q ĺ y and y R dompf q, it holds that dompgq ĺ y and y R dompgq. A set H of partial assignments of Φ is semicompletion-closed if, whenever f P H and g is a semicompletion of f , it holds that g P H.

A graph-based view
When π " C 1 , . . . , C n is a QU-resolution proof of a QBC P : φ from axioms H, define Gpπq to be the directed acyclic graph where there is a vertex for each clause C i , which vertex has label assignpC i q; and, where (for all pairs of clauses C i , C j ) there is a directed edge from the vertex of C j to the vertex of C i if C j is derived from C i .

Proposition 4.9
Let π be a QU-resolution proof of a QBC P : φ from axioms H. The directed acyclic graph Gpπq has the following properties: pαq If a node with label a has no out-edges, then clausepaq is an element of H.
pβq If a node with label a has 1 out-edge to a node with label a 1 , then a 1 is an extension of a with dompa 1 q " dompaq Y tyu where y is a universally quantified variable with dompaq ĺ y.
pγq If a node with label a has 2 out-edges to nodes with labels a 1 and a 2 , then there exists a variable v such that a 1 and a 2 are defined on v and a 1 pvq ‰ a 2 pvq; pdompa 1 q Y dompa 2 qqztvu " dompaq; a and a 1 are equal on the variables where they are both defined; and, a and a 2 are equal on the variables where they are both defined.
Moreover, a labelled graph with these three properties naturally induces a QU-resolution proof: for each node, let a be its label, and associate to it clausepaq. l Definition 4. 10 We say that a QU-resolution proof π is tree-like if the graph Gpπq is a tree. We define tree-like relaxing QU-res to be the proof system ensemble pA 1 , rq described as follows. Let pA, rq denote relaxing QU-res. Then, the algorithm A 1 accepts an input pk, px, πqq if A accepts it and π is tree-like.

A prover-delayer game for tree-like relaxing QU-res
In this section, we present a game that can be used to exhibit lower bounds on the size of tree-like QUresolution proofs; this game can be viewed as a generalization of a game for studying tree-like resolution, which game was presented by Pudlák and Impagliazzo [22].
We first give an intuitive description of the game. Note, however, that this description is meant only to be suggestive. For a precise description, we urge the reader to consult the formal definition, which follows (Definition 5.1); in this formal definition, the game is formulated in a positional fashion, in that the score associated with a partial assignment is independent of the particular history used to reach the assignment.
Relative to a QBC Φ and a set H of axioms, the game is played between two players, Prover and Delayer, which maintain a partial assignment. Prover's goal is to reach a partial assignment in H, while Delayer tries to slow down Prover, scoring points in the process. Prover starts by announcing the empty assignment, and Delayer responds with a semicompletion thereof. After this, the play proceeds in a sequence of rounds. In each round, Prover may perform one of three actions to the current assignment f : select a restriction of f ; assign a value to a @-variable y R dompf q having dompf q ĺ y; or, select a variable v R dompf q. In the first two cases, Delayer responds with a semicompletion of the resulting assignment. In the third case, Delayer may give a choice to the Prover. When a choice is given, the Prover sets the value of v, and Delayer may elect to claim a point which is then associated with v. When no choice is given, Delayer sets the value of v.
After v is set, Delayer responds (as in the first two cases) with a semicompletion of the resulting assignment. Delayer is said to have a p-point strategy if, he has a strategy where, by the time that Prover achieves her goal, there are p variables on which the final assignment is defined such that Delayer has claimed points on these variables.
In what follows, we assume p ě 1.

Definition 5.1
Let Φ be a QBC. Relative to a set H of axioms, a p-point delayer strategy consists of a set F of partial assignments of Φ and a function s : F Ñ N called the score function such that the following properties hold: • (semicompletion-of-empty) There exists a semicompletion g P F of the empty assignment such that spgq " 0.
• (all-points) If f P F X H, then spf q ě p.
• (monotonicity) If g P F , then each restriction of g has a semicompletion f P F such that spf q ď spgq.
• (@-branching) If f P F and y R dompf q is a universally quantified variable with dompf q ĺ y, then, for each b P t0, 1u, the assignment f ry Ñ bs has a semicompletion g P F with spgq " spf q.
• (double-branching) If f P F and v R dompf q, there exists a value b P t0, 1u such that f rv Ñ bs has a semicompletion g P F where (1) spgq ď spf q`1 and (2) if spgq " spf q`1, the assignment f rv Ñ bs has a semicompletion g 1 P F with spg 1 q ď spf q`1.

Theorem 5.2
Assume that there exists a p-point delayer strategy for a QBC Φ with respect to a semicompletionclosed axiom set H, and that π is a tree-like QU-resolution proof ending with the empty clause, from axioms H. Then, the tree Gpπq has at least 2 p leaves.
In order to prove Theorem 5.2, we introduce the following lemma.

Lemma 5.3 Assume that there exists a p-point delayer strategy for a QBC Φ with respect to a semicompletionclosed axiom set H, and that π is a tree-like QU-resolution proof from axioms H.
Let u be a node of Gpπq with label a. If a has a semicompletion f P F with spf q ă p, then u has a child v 1 with label a 1 such that a 1 has a semicompletion g 1 P F with spg 1 q ď spf q`1; moreover, when g 1 P F has spg 1 q " spf q`1, the node u has a second child v 2 whose label a 2 has a semicompletion g 2 with spg 2 q ď spf q`1.
Proof. Since spf q ă p, by the (all-points) condition, we have that f R H. Since H is assumed to be semicompletion-closed, we have that a R H, and hence that the node u is not a leaf of the tree Gpπq.
If the node u is of type pβq from Proposition 4.9, then let a 1 be the label of the child v 1 of u; a 1 has the form ary Ñ bs. By the (@-branching) condition, the assignment f ry Ñ a 1 pyqs has a semicompletion f 1 with spf 1 q ď spf q. We have that f 1 is a semicompletion of a 1 , giving the lemma.
If the node u is of type pγq from Proposition 4.9, let x denote the variable described in the proposition statement. We consider two cases. First, if x P dompf q, then pick the child of u with label a 1 having a 1 pxq " f pxq. By (monotonicity), the restriction f ae dompa 1 q has a semicompletion g 1 P F such that spg 1 q ď spf q, giving the lemma. When x R dompf q, we argue as follows. By the (double-branching) condition, there exists a value b P t0, 1u such that f rx Ñ bs has a semicompletion f 1 satisfying the properties (1) and (2) given in Definition 5.1; in particular, we have spf 1 q ď spf q`1. Let v 1 be the child of u whose label a 1 has a 1 pxq " b. The assignment a 1 restricts arx Ñ bs which restricts f rx Ñ bs, so f 1 extends a 1 . By the (monotonicity) condition, the restriction f 1 ae dompa 1 q has a semicompletion g 1 with spg 1 q ď spf 1 q. If spg 1 q ď spf q, the lemma is proved. Otherwise, we have that spg 1 q " spf q`1, and by property (2) of (double-branching), the assignment f rx Ñ bs has a semicompletion f 2 with spf 2 q ď spf q`1. Let v 2 be the child of u whose label a 2 has a 2 pxq " b. We have that a 2 restricts arx Ñ bs which restricts f rx Ñ bs; by (monotonicity), the restriction f 2 ae dompa 2 q has a semicompletion g 2 P F such that spg 2 q ď spf 2 q, giving the lemma. l Proof. (Theorem 5.2) We refer to a semicompletion of the label of a node simply as a semicompletion of the node. We prove by induction on i " 0, . . . , p that, for any node v with semicompletion f having spf q " p´i, the node v has 2 i leaf descendents. This suffices by the property (semicompletion-of-empty) of Definition 5.1.
The claim is obvious for i " 0, so suppose that it is true for i ă p; we will prove it true for i`1. We have, by assumption, a semicompletion f of v with spf q " p´pi`1q " p´i´1. Repeatedly invoke Lemma 5.3 to obtain a path from v to a leaf where each vertex has a semicompletion associated with it. Notice that, in walking along this path starting from v and looking at the semicompletions, whenever the score increases, it increases by at most 1. Since any semicompletion of a leaf must have score p or higher (by the reasoning at the beginning of the proof of Lemma 5.3), there must be some descendent u of v having semicompletion with score p´i´1 such that the the child u 1 of u provided by Lemma 5.3 has semicompletion with score p´i. By that lemma, the other child u 2 of u has semicompletion with score less than or equal to p´i. By repeatedly invoking Lemma 5.3 to obtain a path from u 2 to a leaf, one finds a descendent v 2 of u 2 having a semicompletion with score p´i. By induction, there are at least 2 i leaves below u 1 , and at least 2 i leaves below v 2 (and hence below u 2 ). Therefore, there are at least 2 i`1 leaves below u, and hence below v. l

Separation of the tree-like and general versions of relaxing QU-res
The family of sentences to be studied in this section is defined as follows. For each i P t0u Y rns, define X i to be the variable set tx i,j,k | j, k P t0, 1uu, and for each i P rns, define X 1 i analogously to be the variable set tx 1 i,j,k | j, k P t0, 1uu. Define P n to be the prefix DX 0 DX 1 1 @y 1 DX 1 DX 1 2 @y 2 DX 2 . . . DX 1 n @y n DX n . Note that, for a set of variables X, we use the notation DX to represent the existential quantification of the variables in X, in any order (our discussion will always be independent of any particular order chosen). For i P rns, we refer to the variables in X 1 i Y ty i u Y X i as the level i variables.
• For each i P rns and each j P t0, 1u define H i,j " t x 1 i,0,k _ x 1 i,1,l _x i´1,j,0 _x i´1,j,1 | k, l P t0, 1uu. Observe that the clause x 1 i,0,k _ x 1 i,1,l _x i´1,j,0 _x i´1,j,1 is logically equivalent to px 1 Define φ n to be the conjunction of the clauses contained in the just-defined sets. Define Φ n as P n : φ n . This definition of this family of sentences was inspired partially by the separating formulas of [11,6].
Let us explain intuitively what the clauses mandate and why the sentences Φ n are false. By the clauses in B, all of the variables x 0,j,k must be set to 0. By the clauses in the sets H 1,j , either both variables x 1 1,0,k or both variables x 1 1,1,k must be set to 0. Once this occurs, the universal player can set the variable y 1 to 0 or 1 (respectively) to force either both variables x 1,0,k or both variables x 1,1,k to 0, via the clauses in T 1 . This reasoning can then be repeated; for instance, at the next level, either both variables x 1 2,0,k or both variables x 1 2,1,k must be set to 0, and then after universal player assigning y 2 appropriately, either both variables x 1,0,k or both variables x 1,1,k are forced to 0. In the end, the existential player must violate one of the two clauses in B concerning level n.

Proposition 6.1 The sentences tΦ n u ně1 have QU-resolution proofs of size linear in n.
Let n ě 1; we will use the following terminology to discuss Φ n . We say that r is a normal realization of level i P rns if it is an assignment defined on the level i variables such that, when b is set to rpy i q, the following hold: We say that r is a funny realization of level i P rns if it is an assignment defined on the level i variables such that, when b is set to rpy i q, the following hold: We state two key and straightforwardly verified properties of realizations in the following proposition.

Proposition 6.2 No assignment defined on the level i variables is both a normal realization and a funny realization. Also, each normal realization and each funny realization (of level i) satisfies all clauses in T i .
We define the set of assignments F n to be the set containing all normal assignments and all funny assignments, which we now turn to define. Let f be a partial assignment of Φ n . Let ℓ ě 0 denote the maximum level ℓ such that f is defined on an D-variable in level ℓ.
We say that f is a normal assignment if the following hold: • f is defined on the variables in tx 0,j,k | j, k P t0, 1uu and equal to 0 on them.
• For each i P rℓ´1s, the restriction of f to the level i variables is a normal realization of level i.
• If ℓ ě 1, either the restriction of f to the level ℓ variables is a normal realization of level ℓ; or, f is halfdefined on level ℓ, by which is meant that f is not defined on any variables in tx ℓ,j,k | j, k P t0, 1uu, but is defined on all variables in tx 1 ℓ,j,k | j, k P t0, 1uu and has ř j,kPt0,1u x 1 ℓ,j,k " 1.
For each normal assignment f , we define s n pf q " ℓ.
We say that f is a funny assignment if there exists m P rℓs such that the following hold: • f is defined on the variables in tx 0,j,k | j, k P t0, 1uu and equal to 0 on them.
• For each i P rm´1s, the restriction of f to the level i variables is a normal realization of level i.
• The restriction of f to the level m variables is a funny realization of level m.
• For each i with m ă i ď ℓ and for each j P t0, 1u, if f is defined on one of the four variables in tx i,j,k , x 1 i,j,k | k P t0, 1uu, then it is defined on all of them and f px i,j, It is straightforward to verify that an assignment cannot be both normal and funny, and also that, if an assignment is funny, there exists a unique m P rℓs witnessing this. For each funny assignment f , we define s n pf q " m. We also identify the following properties of funny assignments which will be used.

Proposition 6.3
Each funny assignment f with s n pf q " m can be extended to a funny assignment f 1 with s n pf 1 q " m which is defined on all D-variables. Moreover, let g be any assignment defined on all variables (of Φ n ) which extends a funny assignment f 1 defined on all D-variables; then, g satisfies all clauses in φ n .

Proof. We verify each of the conditions. (semicompletion-of-empty):
The normal assignment f defined only on tx 0,j,k | j, k P t0, 1uu is a semicompletion of the empty assignment with spf q " 0.
(monotonicity): Suppose that g P F . Let W Ď dompgq. We show that g ae W has a semicompletion f P F with spf q ď spgq.
If the last variable v in W (according to P n ) has the form x 1 i,j,k or y i , then set f " g ae tz | z ĺ vu. Otherwise, the last variable v in W has the form x i,j,k , and we set f to be the restriction of g to the variables in levels 0, . . . , i.
It is straightforward to verify that f P F and that spf q ď spgq. We briefly indicate how to do so, as follows. When g is a normal assignment, then f will also be a normal assignment. When g is a funny assignment with spgq " m, then consider two cases. If the last variable v in W comes before or is equal to y m , the assignment f will be normal. Otherwise, the assignment f will be a funny assignment with spf q " m.
(@-branching): This property is straightforward to verify by examining the structure of the definitions of normal assignment and funny assignment. We perform the verification as follows. Let f P F and let y i R dompf q be a universally quantified variable. We claim that, for each b P t0, 1u, the assignment f ry i Ñ bs is a semicompletion of f having the same score as f .
When f is a normal assignment, we have i ě ℓ. We argue that f ry i Ñ bs is a normal assignment. The assignments f ry i Ñ bs and f are equal on variables in levels strictly before level ℓ. Also, if f on level ℓ is a normal realization, then i ą ℓ and f ry i Ñ bs on level ℓ is the same normal realization. If f is half-defined on level ℓ, then f ry i Ñ bs is also half-defined on level ℓ. Thus, we have that f ry i Ñ bs is a normal assignment. Clearly, spf ry i Ñ bsq " spf q.
When f is a funny assignment with spf q " m, we have i ą m. In looking at the definition of a funny assignment with a funny realization at level m, the requirements imposed on the variables coming strictly after level m concern only the existentially quantified variables. Hence f ry i Ñ bs is also a funny assignment with spf ry i Ñ bsq " m.
(double-branching): Suppose that f P F and that v R dompf q. We consider two cases. When f is a funny assignment with spf q " m, then the variable v must occur in level m`1 or later. If v is a @-variable, then set b arbitrarily; we then have that g " f rv Ñ bs is a funny assignment with spgq " spf q " m. If v is an D-variable, then it is of the form x i,j,ℓ or x 1 i,j,ℓ ; take g to be the either of the two extensions of f defined on dompf q Y tx i,j,k , i,j,1 q. We have that g is a funny assignment with spgq " spf q " m. When f is a normal assignment with spf q " ℓ, the variable v must come after all variables in dompf q. We may assume that v is an D-variable (otherwise, one may reason as in the case of the condition (@branching) to obtain a semicompletion g with spgq " spf q.) First, suppose that the restriction of f to level ℓ is a normal realization. If v is in level ℓ`1, then both f rv Ñ bs and f rv Ñ bs have semicompletions g and g 1 (respectively) which are defined on levels 0 through ℓ`1 inclusive and are equal to funny realizations on level ℓ`1. In this situation, we have spgq " spg 1 q " ℓ`1. If v is in level ℓ`2 or a later level, then we can obtain semicompletions g and g 1 of f rv Ñ bs and f rv Ñ bs (respectively) as follows. First, extend f to obtain an assignment that is equal to an arbitrary funny realization on level ℓ`1; then, we may extend the result by reasoning as in the previous case (where f is a funny assignment) to obtain the desired semicompletions g and g 1 , which are funny assignments with spgq " spg 1 q " ℓ`1.
Next, suppose that f is half-defined on level ℓ.
(a) If the variable v has the form x ℓ,j,k , then we extend f as follows: set y ℓ arbitrarily if it is not already defined, and then extend the result so that it is either a normal realization or a funny realization at level ℓ. The resulting assignment g is a semicompletion of f rv Ñ gpvqs where spgq " spf q.
(b) If the variable v has the form x 1 ℓ`1,j 1 ,k 1 , then take the assignment from the previous item (a); for each value of b P t0, 1u, this assignment can be extended to be defined on the variables x 1 ℓ`1,j,k so that it is equal to b on x 1 ℓ`1,j 1 ,k 1 and ř j,kPt0,1u x 1 ℓ`1,j,k " 1. The resulting extensions are semicompletions of f rv Ñ bs and f rv Ñ bs with score ℓ`1.
(c) Otherwise, the variable v has the form x ℓ`1,j 1 ,k 1 or occurs at level ℓ`2 or later. We first take the extension h of f that is described in item (a); h is defined on all variables in level ℓ. If h is equal to a funny realization at level ℓ, then pick b arbitrarily; it is straightforwardly verified that there is a funny assignment g that is a semicompletion of hrv Ñ bs; this assignment g has spgq " ℓ " spf q. If h is equal to a normal realization at level ℓ, then one can straightforwardly verified that both hrv Ñ bs and hrv Ñ bs have semicompletions g and g 1 (respectively) which are funny assignments having spgq " spg 1 q " ℓ`1.
l Lemma 6.5 Let d, n P N be such that 2 ď d ď 2n. Each assignment f P F n X HpΦ n , dq has spf q ą n´rd{2s.
Proof. Suppose that f P F n X HpΦ n , dq. It cannot be that f is a funny assignment, as for any funny assignment f , the QBF Φ n rf s is true as a consequence of Proposition 6.3. Thus f is a normal assignment. Suppose, for a contradiction, that spf q ď n´rd{2s. In this case, f is not defined on any of the D-variables in the last rd{2s levels, that is, f is not defined on any of the D-variables in levels n´prd{2s`1q, . . . , n´1, n.
As a consequence, the prefix of Φ n rf s is not Π d . Now, consider the relaxation Φ 1 " P 1 : φ 1 of Φ n rf s witnessing that f P HpΦ n , dq. Since P 1 is Π d , it must hold that, in P 1 , there exists a level m P tnṕ rd{2s`1q, . . . , n´1, nu such that the variable y i comes before the variables in X 1 i . We prove that Φ 1 is true (this suffices, as it contradicts f P HpΦ n , dq). We describe an D-winning strategy for Φ 1 , as follows. After each level is set, the resulting assignment is in F n . When it is time to set an D-variable in level i, first check if it holds that i " m and no previous level is set to a funny realization. If these two conditions hold, then level i " m is set to a funny realization. Otherwise, the variables at level i are set as follows.
• If a previous level is set to a funny realization, then the variables in X 1 i YX i are set so that the resulting assignment remains funny (this can in fact be done without looking at the value of y i ).
• Otherwise, proceed as follows. The variables in X 1 i are set so that the sum of their values is equal to 1. The variables in X i are set so that, at level i, one obtains either a normal or funny realization.
This D-strategy is winning, as no matter how the universal player plays, the end assignment will be a funny assignment (defined on all variables), which satisfies all clauses (Proposition 6.3). l By Theorem 6.4 and Lemma 6.5, in conjunction with Theorem 5.2, we obtain the following result. Theorem 6.6 Tree-like relaxing QU-res requires proofs of size Ωp2 n q on the sentences tΦ n u ně1 .

Lower bound for relaxing QU-res
We define a family of QBCs, to be studied in this section, as follows. Let n ě 1. Define P n to be the quantifier prefix Dx 1 @y 1 . . . Dx n @y n . Define φ n,j to be true if and only if j`ř n i"1 px i`yi q ı n pmod 3q. Define Φ n to be the sentence P n : φ n,0 ; these are the sentences that will be used to prove the lower bound. It is straightforward to verify that φ n can be represented as a circuit of size polynomial in n, and we assume that φ n is so represented. We will also make use of the QBCs defined by Φ n,j " P n : φ n,j . Proposition 7.1 For each n ě 1, the sentence Φ n is false.
It is straightforward to verify that a winning @-strategy is to set the variable y i to the value x i . Lemma 7.2 Let π be a relaxing QU-res proof of Φ n from an axiom set. Suppose t ě 1. Let f : tx 1 , . . . , x n´rt{2s u Ñ t0, 1u be an assignment. There exists a sink of Gpπq whose label agrees with f . Lemma 7.3 Let π be a relaxing QU-res proof of Φ n from axiom set HpΦ, Π t q, where t ě 2 and n ě rt{2s. Each sink of Gpπq has a label a that is defined on one of the following variables: x n´prt{2s´1q , y n´prt{2s´1q , . . . , x n´1 , y n´1 , x n , y n .
Proof. Suppose that there exists a sink of Gpπq with label a that is not defined on one of the specified variables. We show that any Π t -relaxation of Φ n ras is true, to obtain a contradiction. It suffices to prove that, for any assignment f : tx 1 , y 1 , . . . , x n´rt{2s , y n´rt{2s u Ñ t0, 1u, any Π t -relaxation of Φ n rf s is true. The sentence Φ n rf s is truth-equivalent to a sentence of the form Φ rt{2s,j . This latter sentence has an even number of variables which number is greater than or equal to t, and is not Π t . Now consider a Π t -relaxation P : φ rt{2s,j of Φ rt{2s,j . We claim that this relaxation P : φ rt{2s,j is true. Since P is a Π t -relaxation of the prefix of Φ rt{2s,j , there exists a variable x k such that y k appears to its left in P . We describe a winning D-strategy that witnesses the truth of the relaxation. First, consider the case that k " 1. In this case, the variables x 1 and x 2 can be set so that y 1`x1`x2 "´j pmod 3q, and each other variable x i can be set to be not equal to y i´1 . Then, no matter how the universal variables are set, the sum of all of the variables excluding y n will be y 1`x1`x2`p y 2`x3 q`¨¨¨`py n´1`xn q " y 1`x1`x2`p n´2q " n`1´j pmod 3q. Then, no matter how y n is set, the final sum S of the variables will have S ı n´j pmod 3q. In the case that k ‰ 1, the variable x 1 is set arbitrarily, and the variables x k and x k`1 are set so that x 1`yk´1`yk`xk`xk`1 " 1´j pmod 3q. Each other variable x i is set to be not equal to y i´1 . No matter how the universal variables are set, the sum of all of the variables excluding y n will be x 1`yk´1`yk`xk`xk`1`p n´3q " n`1´j pmod 3q, which is sufficient as in the previous case. l When f is a partial assignment of Φ n , we refer to the elements of tv | v ĺ lastpf quzdompf q as holes.

Lemma 7.4
Let π be a relaxing QU-res proof of Φ n from an axiom set of the form HpΦ n , Π t q. Each sink of Gpπq has a label f having at most one hole.
Proof. Suppose that f has 2 or more holes. There exist extensions f 0 , f 1 , and f 2 defined on V " tv | v ĺ lastpf qu such that ř vPV f i pvq " i pmod 3q for each i " 0, 1, 2. It is straightforward to verify that one of the QBCs Φ n rf 0 s, Φ n rf 1 s, Φ n rf 2 s is true, implying the truth of Φ n rf s and contradicting that clausepf q is an axiom in HpΦ n , Π t q. l Theorem 7.5 Suppose that t ě 2 and that n ě rt{2s. Let π be a QU resolution proof of Φ n from the axiom set HpΦ n , Π t q. The graph Gpπq has at least 2 n´rt{2s´1 sinks.
Proof. By Lemma 7.2, for each assignment f : tx 1 , . . . , x n´rt{2s u Ñ t0, 1u, there exists a sink v f of Gpπq whose label agrees with f . For each label g of each sink, any variable in tx 1 , . . . , x n´rt{2s u on which g is not defined must be a hole of g, by Lemma 7.3.
Fix a mapping taking each such assignment f to such a sink v f . Since the label of each sink has at most 1 hole (by Lemma 7.4), each sink is mapped to by at most two assignments. Hence the number of sinks must be at least the number of assignments of the form f : tx 1 , . . . , x n´rt{2s u Ñ t0, 1u divided by two. l From the previous theorem, we immediately obtain the following. Theorem 7.6 Relaxing QU-res requires proofs of size Ωp2 n q on the sentences tΦ n u ně1 .

Discussion
Beyond the proof systems discussed already in the paper, another natural way to certify the falsity of a QBF is by explicitly representing a winning @-strategy. Sometimes, the QBF literature refers to methods for extracting strategies from falsity proofs or by outfitting a solver; this notion is often called strategy extraction.
We can formalize a proof system ensemble based on explicit representation of @-strategies, as follows. We use the notation in Section 2. Let Φ be a QBC, and let H be an axiom set of Φ. Let us define a circuit @-strategy to be a sequence of circuits pC y q yPY where each C y has |X ăy | input gates, which are labelled with the elements of X ăy . Such a sequence pC y q yPY naturally induces a @-strategy pτ y q yPY for Φ. We say that pC y q yPY is a winning circuit @-strategy with respect to H if for every assignment σ : X Ñ t0, 1u, it holds that xτ, σy falsifies a clause in H. This naturally yields a proof system ensemble pA, rq, where rpkq " k`4 and A accepts pk, pΦ, πqq when the following condition holds: π is a winning circuit @strategy for Φ with respect to HpΦ, Π k`2 q, that is, if for each assignment σ : X Ñ t0, 1u, there exists a clause C P HpΦ, Π k`2 q such that xτ, σy falsifies C. The latter formulation of the condition can be checked with access to a Π p 4 oracle (equivalently, a Σ p 4 oracle). We call this proof system ensemble relaxing stratex. From a result appearing in previous work [17,Section 3.1], it can be shown that winning circuit @strategies can be efficiently computed from QU-resolution proofs. This implies the following. The QBC family studied in the previous section had very simple winning @-strategies which can clearly be represented by polynomial-size circuits. We can thus conclude from Theorem 7.6 that relaxing QU-res does not simulate relaxing stratex. The separation between tree-like relaxing QU-res and (general) relaxing QU-res (Proposition 6.1 and Theorem 6.6) implies that tree-like relaxing QU-res does not simulate relaxing QU-res, while it is clear that relaxing QU-res simulates tree-like relaxing QU-res. The technical results under discussion can thus be summarized via a small hierarchy of proof system ensembles: tree-like relaxing QUres is simulable by relaxing QU-res, but not the other way around; and, relaxing QU-res is simulable by relaxing stratex, but not the other way around.

Proof of Proposition 3.4
Proof. For the forward direction, let pA, rq be a polynomially bounded proof system ensemble for L. Let k and f be as in Definition 3.3. Fix k 1 " rpkq. Let q be a polynomially such that for each string x, it holds that |f pxq| ď qp|x|q. Membership of a given string x in L can be decided by nondeterministically guessing a string π of length less than or equal to qp|x|q, and then checking if A Spk 1 q accepts; this places L in the polynomial hierarchy.
For the backward direction, suppose that L is in the PH. Then, there exists a k 1 P N and a polynomial time algorithm B which may make oracle calls to Spk 1 q such that B Spk 1 q accepts a string px, πq if and only if x P L. Define r to map each n P N to k 1 . The pair pB, rq is readily verified to be a proof system ensemble which is polynomially bounded (indeed, with respect to the constant polynomial equal everywhere to 1). l 10 Proof of Proposition 4.7 Proof. Suppose first that pk, pΦ, πqq is accepted by A. Then, π is a QU-resolution falsity proof of Φ from axioms in HpΦ, Π k`2 q; by Proposition 4.5, HpΦ, Π k`2 q is an axiom set of Φ, so it follows from Proposition 4.2 that the QBC Φ is false.
Suppose that Φ " P : φ is a false QBC; let V denote its variables. Let F be the set that contains each assignment f : V Ñ t0, 1u that falsifies φ. We have that φ has the same satisfying assignments as φ 1 " Ź f PF clausepf q. Hence the QBC Φ 1 " P : φ 1 is also false. It is known that there exists a QUresolution proof π of Φ 1 ending with the empty clause, from axiom set H F " tclausepf q | f P F u; this follows from the completeness of Q-resolution on clausal QBF, see for example the proof of Theorem 2.1 in []. Since H F Ď HpΦ, Π k`2 q for each k, it holds that A accepts pk, pΦ, πqq. l 11 Proof of Lemma 4.8 Proof. Suppose that f P HpΦ, Π m q and that g is a semicompletion of f . Suppose that v P dompgqzdompf q. Assume that dompf q is non-empty. If lastpf q is a @-variable, then by definition of semicompletion, either v ň lastpf q; or, each variable of the quantifier block of lastpf q is in dompf q and v occurs in the quantifier block (of D-variables) immediately following the block of lastpf q. If lastpf q is an D-variable, then by definition of semicompletion, it holds that v ĺ lastpf q. In each of these cases and also when dompf q " H, it holds that v is in the first quantifier block of Φrf s, which block is existentially quantified.
We have thus established that each variable in dompgqzdompf q is existentially quantified in Φrf s. Let Φ 1 " P 1 : φ 1 be a false Π m -relaxation of Φrf s. Let Φ 2 be the sentence obtained from Φ by replacing each variable v P dompgqzdompf q with the constant gpvq in φ 1 , and removing each such v (and its accompanying quantifier) from P 1 . We have that Π 2 is a Π m -relaxation of Φrgs, and that the falsity of Φ 1 implies the falsity of Φ 2 . l 12 Proof of Proposition 6.1 Proof. We prove, by induction, that for c " 0, . . . , n, it holds that, for each j P t0, 1u, the clause x n´c,j,0 _ x n´c,j,1 is derivable from Φ n by QU-resolution. For c " 0, we have that the two clauses of concern are contained in B. Suppose that c P rns and that the claim is true for c´1. By induction, we have that the two clauses D 0 " x n´pc´1q,0,0 _ x n´pc´1q,0,1 and D 1 " x n´pc´1q,1,0 _ x n´pc´1q,1,1 are derivable by QU-resolution. By resolving the clause D 0 with the two clauses in t x n´pc´1q,0,k _ y i _ x 1 n´pc´1q,0,k | k P t0, 1uu Ď T n´pc´1q we derive the clause y i _ x 1 n´pc´1q,0,0 _ x 1 n´pc´1q,0,1 ; by applying @-elimination, we derive the clause E 0 " x 1 n´pc´1q,0,0 _ x 1 n´pc´1q,0,1 . Similarly, by resolving the clause D 1 with the two clauses in t x n´pc´1q,1,k _ y i _ x 1 n´pc´1q,1,k | k P t0, 1uu Ď T n´pc´1q we derive the clause y i _ x 1 n´pc´1q,1,0 _ x 1 n´pc´1q,1,1 ; by applying @-elimination, we derive the clause E 1 " x 1 n´pc´1q,1,0 _ x 1 n´pc´1q,1,1 . By resolving E 0 and E 1 with the clauses in H n´pc´1q,0 , we derive the clause x n´c,0,0 _ x n´c,0,1 . Similarly, by resolving E 0 and E 1 with the clauses in H n´pc´1q,1 , we derive the clause x n´c,1,0 _ x n´c,1,1 . This concludes the proof of the claim.
The empty clause is obtained by resolving the unit clauses t x 0,j,k | j, k P t0, 1uu Ď B with the clause x 0,0,0 _ x 0,0,1 , or with the clause x 0,1,0 _ x 0,1,1 . The resulting proof has linear size, since each step of the induction requires a constant amount of size. l

Proof of Lemma 7.2
Proof. Fix such an assignment f . Since the empty assignment, the label of the root, agrees with f , it suffices to show the following: each non-leaf node u whose label agrees with f , has an edge to a node which agrees with f . If u has one outgoing edge, then this is clear by the description in Proposition 4.9. If u has two outgoing edges, let v be the variable described in Proposition 4.9. If v is universally quantified, then both of its children agree with f ; if v is existentially quantified, then one of the children must have label a where apvq " f pvq; this child's label a then agrees with f . l