key: cord-0046600-72a2ptc7
authors: Chew, Leroy; Clymo, Judith
title: How QBF Expansion Makes Strategy Extraction Hard
date: 2020-05-30
journal: Automated Reasoning
DOI: 10.1007/978-3-030-51074-9_5
sha: 75fa938982aa4ee4f7bf8880828e7d20d1d4df06
doc_id: 46600
cord_uid: 72a2ptc7

In this paper we show that the QBF proof checking format QRAT (Quantified Resolution Asymmetric Tautologies) by Heule, Biere and Seidl cannot have polynomial time strategy extraction unless P=PSPACE. In our proof, the crucial property that makes strategy extraction PSPACE-hard for this proof format is universal expansion, even expansion on a single variable. While expansion reasoning used in other QBF calculi can admit polynomial time strategy extraction, we find this is conditional on a property studied in proof complexity theory. We show that strategy extraction on expansion based systems can only happen when the underlying propositional calculus has the property of feasible interpolation.

Quantified Boolean logic is an extension of propositional logic in which variables may be existentially or universally quantified. This can allow problems to be represented more succinctly than is possible in propositional logic. Deciding the truth of a quantified Boolean formula (QBF) is PSPACE-complete. Propositional proof systems can be lifted to the QBF situation by the addition of rules to handle the universal quantification.

In addition to deciding whether a given QBF is true or false it is desirable that algorithms for solving QBFs can provide verification by outputting a proof. The QRAT proof system [14] is sufficiently strong to simulate the reasoning steps of all current QBF solvers and preprocessors and is a candidate for a standard format for verification of solvers.

In many settings it is not simply desirable to know that a QBF is true or false but also to find functions that witness to this. For example, QBFs may be used to model safety verification so that if the QBF is false then the modelled system is able to reach an unsafe state. It may be important to also know how this state is reached. If a QBF is true (resp. false) then there must exist Skolem (resp. Herbrand) functions for the existentially (resp. universally) quantified variables that certify this. Substituting the certifying Skolem functions into the original QBF yields a tautology. Equivalently, substituting Herbrand functions results in an unsatisfiable propositional formula. The ability to efficiently extract Skolem or Herbrand functions from the proof output by a QBF solver is called strategy extraction.

There are generally two main paradigms in QBF solving: QCDCL (Conflict Driven Clause Learning) and QBF expansion. Both of these paradigms borrow techniques from propositional satisfiability solving for existential variables, but they differ in how they handle universal variables. The performance and limitations of these solvers can be analysed by studying proof systems that follow the solver steps. QCDCL adds the universal reduction rule, such as in the Q-Res proof system [20] . QBF expansion, on the other hand, adds the universal expansion rule such as in the proof system ∀Exp+Res [16] . Both Q-Res and ∀Exp+Res are based on the resolution system in propositional logic.

The relationship between the two systems has been studied extensively in both QBF theory and practice. In [4, 16] it was shown that Q-Res and ∀Exp+Res are incomparable. However the picture becomes much more nuanced on certain fragments of QBF. Lonsing and Egly ran experiments on QBFs which were parametrised by the number of quantifier alternations and found better performance in the expansion based solvers on formulas with a low number of alternations [23] . This observation was confirmed in proof complexity in [3] where the expansion calculus ∀Exp+Res was shown to polynomially simulate the QCDCL calculus Q-Res on bounded quantifier alternations.

As well as using the calculi Q-Res and ∀Exp+Res to compare the strengths of the two types of QBF solvers, other properties can be studied for each of these systems. One very important property is the aforementioned strategy extraction. Often the strategies are just as important as whether a QBF is true or false. Many QBF proof systems with the universal reduction rule (from QCDCL) have been studied and shown to have polynomial time strategy extraction using a technique from [1] and later generalised in [2, 7] . For QBF systems with universal expansion some strategy extraction results are known using a different technique [4, 12] .

QRAT is a very different kind of proof system, not only can it simulate both the universal reduction and expansion rules but it draws from a stronger form of propositional reasoning than resolution. With this power it has been shown to simulate a number of different QBF proof systems [17, 18] .

Strategy extraction on a universal checking format like QRAT would have certain benefits for the solving community. One could extract a QRAT proof from a solver and then from that proof separately extract the Skolem/Herbrand functions that give the winning strategy. This would avoid having to extract strategies directly from solvers while they are running which may affect performance.

Conversely, the property of strategy extraction can actually provide a source of weakness in QBF proof systems. In particular Q-Res can always extract strategies as bounded depth circuits. This means that QBFs with winning strategies that cannot be expressed in small bounded depth circuits necessarily have large Q-Res proofs [4] . This is similar to the proof size lower bound technique based on feasible interpolation [21, 24] where if a propositional proof system can extract Craig interpolants in polynomial time then super-polynomial interpolant size lower bounds become super-polynomial proof size lower bounds.

It was shown in [13] that Skolem functions to certify that a QBF is true can be extracted in polynomial time from a QRAT proof. In [8] a partial result was presented showing that Herbrand functions may be extracted from proofs in a restricted version of refutational QRAT. Here, we show that it is not possible in general to efficiently extract Herbrand functions certifying falsity from proofs in QRAT. This is due to QRAT providing short proofs to formulas that have PSPACE-hard strategies. Thus we show an asymmetry between the refutation of false QBF and proof of true QBF in the QRAT system. We demonstrate that this is due to the presence of universal expansion steps which manifest from the powerful reduction rules in the full QRAT proof system [14, 18] .

The universal expansion reasoning technique is present in QBF proof systems other than QRAT, but does not always exhibit the same hardness issues that we demonstrate for QRAT regarding strategy extraction. For example, the proof system ∀Exp+Res [16] uses expansion, but allows polynomial time strategy extraction [4] . In this paper we strengthen the important connection, first explored in [5] , between strategy extraction and feasible interpolation. This paper is organised as follows: Sect. 2 introduces the main concepts used in this paper. We show that strategy extraction in QRAT is PSPACE-hard in Sects. 3 and 4. In Sect. 5 we look at expansion based systems that do have strategy extraction. We show that it is necessary for their underlying proof systems to have feasible interpolation. A sufficient condition with a relationship to feasible interpolation is also shown.

Let Γ be an alphabet, with Γ * being the set of strings over Γ. Let L be a language over Γ, in other words L ⊂ Γ * . A proof system [9] for L is a polynomial time computable partial function f : Γ Γ with range L. The size |π| of a proof π in Γ is the number of characters it contains. Proof system f maps a proof to the theorem it proves (or refutes, in the case of a refutational proof system). Soundness of f requires that rng(f ) ⊆ L and completeness that rng(f ) ⊇ L. Given a family {c i | i ∈ N} of formulas f i ∈ L, and a family of f -proofs P = (1) . An even stronger property is that P is said to be uniform if there is a polynomial-time function h such that h(c i ) = p i .

In propositional logic a literal is a Boolean variable x or its negation ¬x. A clause is a disjunction of literals. A formula in conjunctive normal form (CNF) is a conjunction of clauses. Let l be a literal. If l = x thenl = ¬x, if l = ¬x thenl = x. A CNF is naturally understood as a set of clauses, and a clause as a set of literals. Where it is convenient to do so we will therefore use set notation C ∈ φ and l ∈ C to state that clause C appears in φ and literal l appears in C. It is often convenient to notationally treat clauses as unordered disjunctions and sets simultaneously, so we can use C ∨ l to denote the clause that contains all literals of clause C and also the literal l if it is not already included, and D ∪ E to denote the disjunction of all literals that appear in either clause D or E. An assignment τ for a formula φ over n variables is a partial function from the variables of φ to {0, 1} n . τ (C) is the result of evaluating clause C under assignment τ , and φ| τ = {τ (C) | C ∈ φ}. For formula (or circuit) φ, we define φ[b/x] so that all instances of variable x in φ are replaced with b ∈ {0, 1}.

Quantified Boolean formulas (QBF) extend propositional logic by allowing for Boolean variables to be universally or existentially quantified [19] . ∀x Ψ is satisfied by the same truth assignments as Ψ [0/x]∧Ψ [1/x] and ∃x Ψ is satisfied by the same truth assignments as

In a closed QBF all variables must be quantified. A prenex QBF Ψ consists of a prefix Π defining how each variable is quantified and a propositional part φ called the matrix. We write Ψ = Πφ. The prefix Π has a linearly ordered structure. A PCNF is a QBF in prenex form and with the propositional part in conjunctive normal form. We consider only closed PCNFs.

Starting from the left we can assign each variable x a level, denoted lv(x). The first variable has level 1. The level is incremented by 1 every time the quantifier type changes and otherwise remains the same. It is often convenient to write quantifiers in a prefix only when the level changes. When QBF are written in this way we can think of entire levels quantifying blocks of variables.

A closed prenex QBF is analogous to a two player game with perfect information, in which one player is responsible for assigning values to the existentially quantified variables and the other to the universally quantified variables. The players make assignments according to the quantifier prefix, so each level of the prefix corresponds to one turn in the game, moving from left to right. The existential player wins the game if the formula evaluates to true once all assignments have been made, the universal player wins if the formula evaluates to false.

A strategy for the universal player on QBF Πφ is a set of rules for making the assignments to each universal variable u. The rule for setting u must depend only on variables earlier than (to the left of) u in Π, respecting the idea that when u is being decided the universal player cannot know what choices will be made in future turns. If this strategy ensures the universal player always wins games on Πφ (however the existential player makes assignments), then it is called a winning strategy. A QBF is false if and only if the universal player has a winning strategy. Strategies for the existential player are defined analogously. A refutational proof system is said to admit strategy extraction if and only if it is possible to efficiently (i.e. in polynomial time in the size of the proof) construct a circuit representing a winning strategy for the universal player from a refutation of a QBF.

Since QBF includes and extends all propositional formulas, proving (or refuting) QBFs typically involves adapting existing propositional proof systems to deal with variables that are now quantified.

One such approach is to take the semantic definition of the universal quantifier ∀uΨ ≡ Ψ [0/u] ∧ Ψ [1/u], which can be used as a rule to eliminate universal quantifiers. If Ψ is a QBF then Ψ [0/u] and Ψ [1/u] each contain their own quantifiers, so the variables bound by these quantifiers would have to be renamed to avoid repeating the other's variables. We take a convention of renaming these variables by putting a partial assignment in the superscript such that the vari-

Note that because we started here with a prenex formula, we can maintain that throughout the expansions. In the end, once we expand all universal variables we have a prenex QBF with only existential quantifiers, this is known as a full expansion. Deciding the truth of a closed PCNF with only existential quantifiers is simply a propositional satisfiability problem. If we use a refutation system S we can attempt to refute the expanded formula.

In fact for any refutational propositional proof system S we can create a refutational QBF proof system (that is refutationally complete) by taking the full expansion and showing a contradiction using propositional system S. Such a system would easily have many exponential lower bounds due to the explosion caused by the full expansion on a linear number of universal variables.

In practice we can often do better than this. The full expansion gives a large conjunction and we may only need to use some of the conjuncts in order to prove a contradiction. This can be tightened up further when the original QBF is a prenexed conjunction (like a PCNF), checking whether a conjunct is in the full expansion can be decided in polynomial time. We define this formally below.

S+∀Exp 0, 1 We start with a propositional proof system S and prenex QBF Ψ = Πφ, where Π is the quantifier prefix and φ is a propositional matrix in variables of Π. We treat φ as a conjunction of formulas.

Let τ be a full assignment to all universal variables and let l be an existentially quantified literal. We define restrict l (τ ) to be the partial assignment of τ for all universal variables whose level (in the prefix) is less than that of the variable of l. Now let us use that to define C τ , where C is a propositional formula in both existential and universal variables.

C τ is the same as C except that we replace every existential literal l with the annotated literal l restrict l (τ ) and every universal variable u with its value τ (u). Definition 1. The refutational QBF proof system S+∀Exp 0,1 allows the instantiation of axiom C τ , whenever C is a conjunct from the matrix and τ is an assignment to all universal variables; it generates an S refutation of the conjunction of the axioms, treating differently annotated variables as different.

An S+∀Exp 0,1 proof [2] π of QBF Ψ therefore consists of a propositional S proof of a sub-conjunction of the full expansion. We denote this conjunction as subexp π (Ψ ).

A well-known example of S+∀Exp 0,1 is ∀Exp+Res [16] which is obtained when S is propositional resolution. This is the proof system that underlies the reasoning in the competitive QBF solver RAReQS [15] . Resolution is chosen because of its use in SAT solving.

The QRAT proof system [14] was introduced as a universal proof checking format for QBF. It is able to express many QBF preprocessing techniques and proof systems. QRAT works on a QBF Πφ in PCNF which is modified throughout the proof by satisfiability preserving rules. Clauses may be added, altered or deleted depending on the current status of Πφ.

QRAT may be used either to prove that a QBF is true or to refute it. The refutational version of QRAT uses the following rules: Asymmetric Tautology Addition (ATA), Quantified Resolution Asymmetric Tautology Addition (QRATA), Quantified Resolution Asymmetric Tautology Universal (QRATU), Extended Universal Reduction (EUR), and Clause Deletion. We define only the rules that are relevant for this paper, for a full definition of the QRAT system please refer to [14] .

If C is a clause, thenC is the conjunction of the negation of the literals in C. Unit propagation is a procedure on a formula φ in CNF that builds a partial assignment τ . This assignment is applied to φ and then for any literal l that appears in a singleton (unit) clause in the resulting formula, the assignment satisfying l is added to τ . This is repeated until reaching fix-point, which must happen in polynomial time in the number of clauses in φ. Unit propagation is used extensively in QRAT for deciding whether a derivation rule may be applied. We denote by φ 1 ⊥ that unit propagation derives the empty clause from φ.

In the following definitions, Πφ is a closed PCNF and C a clause not in φ. Π is a prefix including the variables of φ and C, Π is identical to Π except that it contains the variables of φ only. Addition (ATA) ). Suppose φ ∧ C 1 ⊥. Then we can make the following inference

Πφ (ATA) Π φ ∧ C Definition 3 (Outer Clause). Suppose C contains a literal l. Consider all clauses D in φ withl ∈ D. The outer clause O l D of D is {k ∈ D | lv(k) ≤ Π lv(l), k =l}.

Note that for Definition 4 we have used the original definition of QRATA as it appears in [14] , where it is explicitly stated that new variables can appear anywhere in the prefix. In [13] another definition is used where new variables only appear at the end of the prefix and are necessarily existential. This paper is in line with the original paper and recent papers such as [8, 17, 18] .

where D ∈ φ is any clause with some p : lv(p) > Π lv(u), p ∈ C andp ∈ D, until we reach a fix-point denoted C . Ifū / ∈ C then we can perform the following rule.

We can also define a weaker version of QRAT, QRAT(UR), which uses universal reduction instead of EUR.

Definition 6 (Universal Reduction (UR)). Given a clause C ∨ u with universal literal u such that lv(u) > lv(x) for all existentially quantified variables x in C we can apply the following rule.

It is rumoured that the famous chess players Alekhine and Bogoljubov were once both separately challenged to a game of correspondence chess by an anonymous opportunist. The third player had deviously remembered the moves of each opponent to play Alekhine's and Bogoljubov's moves against each other, effectively removing themselves from the game. The player was guaranteed to win or draw in at least one game, and with the money odds against them, they stood to make a profit.

We see that this devious idea can also be used in the conjunction of QBF twoplayer games. We will show that these conjunctions have short QRAT proofs. We take a QBF and conjunct it with its negation in new variables. We interleave the prefixes so that the existential player plays first and the universal player is able to copy the moves at the right time. The universal player has to win on only one of the conjuncts and an easy winning strategy is to copy the opponent's move for the other side. The easy winning strategy is essential for the short proofs, but despite the guaranteed win, it is PSPACE-hard to find out which game the universal player wins prior to playing it. In the next section we add an extra universal variable that requires the calculation of who wins in order to make the game hard. However we see that expansion allows us to quickly return to the original easy problem.

In this section we will define these formulas that conjunct a QBF and its negation and show how a short QRAT proof can be uniformly obtained.

Let X be the set of variables {x 1 , . . . , x 2n } and φ(X) a CNF in the variables of X. Then Πφ(X) with prefix Π = ∀x 1 ∃x 2 ∀x 3 . . . ∃x 2n is a closed PCNF. We also define a second set of 2n variables X = {x 1 , . . . , x 2n } and an alternative prefix Π = ∃x 1 ∀x 2 ∃x 3 . . . ∀x 2n . The QBF Πφ(X) ∧ Π ¬φ(X ) is necessarily false. However this QBF is not in PCNF, which many proof systems require.

Firstly we will transform ¬φ(X ) into a CNFφ(X , T ) via the use of Tseitin variables T = {t K | K ∈ φ(X)}. We overload the notation:

-For literal l if l = x i then l = x i and if l = ¬x i then l = ¬x i . -For each clause K in φ(X) we denote the corresponding clause in φ(X ) as K so that K = l∈K l .

We require thatφ(X , T ) is true precisely when φ(X ) is false. We will introduce clauses stating that variable t K is true if and only if clause K is satisfied. Then φ(X ) is false if and only if at least one t K is false, so we will also add a clause specifying that this must hold.

φ(X , T ) contains the following clauses:

The next part is the most important -the prenexing of the QBF. We place every universal variable to the right of its existential counterpart. The auxiliary T variables must be placed at the end of the prefix. Thus, from any PCNF Ψ = Πφ we generate a formula Duality(Πφ) encoding in PCNF the claim that both Ψ and its negation are true:

In [6] , Beyersdorff et al. showed short Frege + ∀red proofs of a family of QBFs that take an input of a graph and state that there is a k-clique (Clique) and dually that there is no k-clique (Co-Clique). The short proofs exploited the fact that the Co-Clique part of the formula was structured in a similar way to the Clique part.

We generalise this approach here for short proofs of the Duality formulas. First we will give a sketch proof of how this can be done using Frege + ∀red rules before we show those short proofs formally in QRAT. Frege + ∀red is simply a propositional Frege system augmented with the ∀red rule for removing universally quantified variables. ∀red allows to substitute a Boolean value for universally quantified u in a previously derived line, provided that lv(u) > lv(x) for all existentially quantified x in the proof line.

The clauses in Duality(Πφ) state K (t K ↔ K ), K ¬t K and K.

Recall that clause K is identical to clause K with all instances of x i replaced with x i (for all i). From assumption 2n i=1 (x i ↔ x i ) we would find a contradiction in polynomially many Frege steps. The outline of the derivation is given below:

. Now, starting from the variables quantified innermost in the prefix, we perform ∀red on all universally quantified x 2j and x 2j+1 :

Reduction can also be done with x 2j = 1

We can resolve these two disjunctions together and conclude

Now x 2n−1 is the innermost universally quantified variable. The same sequence of steps is applied for each universal variable leading to a contradiction which completes the proof.

This proof idea works for showing short proofs in QRAT. In fact these proofs have a uniform structure. Proof. Let |K| be the number of literals in clause K ∈ φ, then | Duality(Πφ)| ≥ |φ| ≥ Σ K∈φ |K|. Recall Πφ has 2n variables.

Extension Variables. The refutation begins by using QRATA to introduce extension variable eq xi for each x i ∈ X. Every eq xi is existentially quantified and is introduced to the prefix so that lv(eq xi ) > lv(x i ), lv(x i ) and lv(eq xi ) < lv(x j ), lv(x j ) for all j > i (which is possible since lv(x i ), lv(x i ) < lv(x j ), lv(x j ) in Duality(Πφ) whenever j > i). For each x i ∈ X we use QRATA to add four clauses:

Recall that adding a clause by QRATA requires that we have an existential literal l in the new clause C such that φ ∧C ∧Ō l D 1 ⊥ for all D withl ∈ D. For the first two clauses this is vacuously satisfied with l = ¬eq xi since eq xi does not appear positively anywhere in the formula. To add the latter clauses we have l = eq xi and must consider the two outer clauses (¬x i ∨ x i ) and (x i ∨ ¬x i ). The QRATA condition is satisfied for (¬x i ∨¬x i ∨eq xi ) because x i ∧x i ∧x i ∧¬x i 1 ⊥ and x i ∧ x i ∧ ¬x i ∧ x i 1 ⊥, and similarly for the final clause.

For each of the original 2n variables in Πφ we have added four clauses of constant size. Following O(n) steps the formula has increased in length by O(n) characters.

Non-Equivalence of Xand X . The next three ATA steps are equivalent to those in the derivation of

Each clause has O(n) literals and there are at most |φ| clauses of each type. In O(|φ|) proof steps the formula has increased in length by O(n|φ|).

Removing the Universal Variables. Finally, we want to derive A j = ( j−1 i=1 ¬eq xi ) for j = 2n . . . 1 (thus j = 1 means that we have derived the empty clause). Assuming that we already have A j+1 we can use ATA to add:

In these clauses whichever of x j and x j is universally quantified is innermost by the construction of Duality(Πφ) and the decision of where to introduce the variables eq xi in the prefix. Without loss of generality, assume x j is universally quantified so we can use UR to derive clauses ( 

The formulas Duality(Πφ) have short winning strategies for the universal player, namely to always play so that x i = x i . We know also that one of Πφ(X) or Π φ (X , T ) is false and so has a winning strategy for the universal player. Deciding which subformula is false is PSPACE-hard and the winning strategy for the false formula could be much more complicated than the strategy for Duality(Πφ). We introduce formulas exploiting this hardness:

and Q = ∃x 1 ∀x 1 ∃x 2 ∀x 2 . . . ∃x 2n−1 ∀x 2n−1 ∃x 2n ∀x 2n

It was shown in [13] that satisfaction QRAT has strategy extraction, and in [8] that refutational QRAT(UR) has strategy extraction. In this section we use the formulas Select(Πφ) to show that refutational QRAT does not have strategy extraction under a strong complexity assumption.

Proof. The first step in the proof is to use Extended Universal Reduction (EUR) to remove u from all clauses in φ u (X) and ¬u from all clauses inφ ¬u (X , T ). Using EUR to reduce l in C requires thatl does not appear in C (the fixpoint of the inner expansion as given in Definition 5). In other words, there is no inner resolution path between any clauses containing the removed literal and its negation. We can only add literals to the inner expansion from clauses that share variables in common with the current inner expansion. However u and ¬u appear in sections of the formula that have no other variables in common. Hence we can always reduce u (and ¬u) in Select(Πφ).

Having performed these (polynomially many) EUR steps the formula is identical to Duality(Πφ), which is uniformly refuted as in Theorem 1.

Proof. If QRAT has strategy extraction we can decide the truth of closed QBF in polynomial time -a PSPACE-complete problem.

Given a QBF Πφ, with Π a prefix and φ a propositional formula in the variables of Π, we create the formula Select(Πφ) and then in polynomial time we can output the proofs as in Theorem 2. Then from the proof of Select(Πφ) we can extract the strategy for u. Since u is outermost in the prefix, this strategy must be constant. If the strategy sets u = 0 then all clauses inφ ¬u (X , T ) are immediately satisfied so we know that the rest of the extracted strategy is a strategy for Πφ, showing that Πφ is false. Similarly, if the strategy sets u = 1 then it must be the case thatφ ¬u (X , T ) is false and so, by construction, Πφ is true. Therefore we have a polynomial time decision procedure for an arbitrary QBF.

In fact, the full power of EUR is not required. QRAT(UR) is capable of refuting the formulas Duality(Πφ), and the initial EUR step can be replaced by universal expansion of u, producing a formula equivalent to Duality(Πφ) with renamed variables. Even QBF solvers whose underlying proof system uses universal reduction to handle universally quantified variables often employ a preprocessing stage that includes universal expansion. Our Select(Πφ) formulas show that a single initial expansion step may be sufficient to prevent strategy extraction.

The results of the previous section indicate that expansion steps may prevent strategy extraction. However we have seen many proof systems and solvers that admit strategy extraction despite using universal expansion. It is clear that the other rules of the calculus play an important role on whether or not strategy extraction is admissible.

If we wish to guarantee strategy extraction in our proof systems and solvers, it may be important for future work to explore sufficient conditions for strategy extraction when using expansion. In this section we instead explore a necessary condition for strategy extraction.

In Corollary 1 the necessary condition for strategy extraction in QRAT was that we needed efficient circuits that calculated the truth of Πφ in order to have strategy extraction for Duality(Πφ). We can think of a strategy for u acting as a circuit deciding between Πφ and ¬(Πφ). In propositional logic the efficient extraction of these deciding circuits (known as interpolating circuits or interpolants) from a proof is a well studied technique known as feasible interpolation. In this section, we will use our lower bound technique to place necessary conditions for strategy extraction on a large class of QBF proof systems.

Given a true propositional implication A(P, Q) → B(P, R) (or, equivalently, a false conjunction A(P, Q)∧¬B(P, R)) Craig's interpolation theorem [11] , states that there is an interpolant C(P ) in only the joint variables P . Feasible interpolation is a property of proof systems. A proof system has feasible interpolation [21, 24] if and only if there is a polynomial time procedure that takes a proof of A(P, Q) → B(P, R) as an input and extracts an interpolating circuit C(P ).

In [5] Beyersdorff et al. lifted a version of the feasible interpolation lower bound technique from propositional logic to QBF. In Sect. 5 of [5] feasible interpolation was linked to strategy extraction by adding an extra universal variable with similarities to Sect. 4 and how the Select formulas are created from the Duality formulas. Proof. Suppose S+∀Exp 0,1 has strategy extraction and we have an S-refutation π of A(P, Q) ∧ B(P, R) with P, Q, R disjoint sets of variables. We will show that we can find an interpolant in polynomial time.

We consider the following QBF

We can refute this formula in S+∀Exp 0,1 using π. Expansion gives us

but this immediately simplifies to A(P, Q 0/u ) ∧ B(P, R 1/u ).

We can now refute this using π using Q 0/u variables instead of Q, and using R 1/u variables instead of R. The provision here is important for this as one could make S a pathological proof system that disallowed steps using variables named as in R 0/u , but allowed them named as in R.

We can then extract a strategy for u as a circuit in the variables P . However this circuit is also an interpolant for A(P, Q) ∧ B(P, R).

In regards to making sufficient conditions for strategy extraction using feasible interpolation we can look at the results that have come before. We see that ∀Exp+Res has strategy extraction. This is done by a "round-based" strategy extraction. This technique gives a winning response for the universal player by taking the outermost block of existentially quantified variables and applying a restriction to the ∀Exp+Res proof on that block in correspondence to the existential player's moves. The universal player can then "read off", from the restricted proof, which universal assignment to the next block of variables is useful in the proof. The proof can be restricted by the universal assignment and we repeat until we end up with a complete set of universal responses and a falsified formula.

The "reading off" which clauses actually contribute to the proof is a weak form of feasible interpolation and so we can say we have strategy extraction for S+∀Exp 0,1 whenever refutational proof system S satisfies two conditions. Note that because of Theorem 3 feasible interpolation is implied by these two conditions (although this can be shown without Theorem 3). The extraction technique is inspired by the one used in [12] , instead here we use it for expansion systems. Resolution would be an example of such a system with both properties. It is not possible to say for certain that any proof system lacks one or both of these properties without a separation of P and NP. The first property is fairly common, even in stronger systems, but we do not expect systems such as bounded-depth Frege to have the second property.

Proof. Suppose we have a closed prenex QBF ∃X∀Y Πφ where Π is a prefix in variables Z and φ is a propositional matrix with variables in X,Y and Z. Now suppose we have an S+∀Exp 0,1 refutation π of ∃X∀Y Πφ. This gives an S proof π of subexp π (∃X∀Y Πφ), a subset of the full expansion of ∃X∀Y Πφ using π.

We will show that under conditions 1 and 2 we have a polynomial time procedure that takes any assignment to X and outputs a response μ in Y and a Πφ| ,μ refutation in S+∀Exp 0,1 .

From π , we can extract π in polynomial time, using condition 1, which provides an S refutation of subexp π (∃X∀Y Πφ)| . For D ∈ φ we have that C = D| is in φ| , so every conjunct D τ | of subexp π (∃X∀Y Πφ)| is also an axiom C τ of ∀Y Πφ| . Therefore, π becomes an S+∀Exp 0,1 refutation π of ∀Y Πφ| . Now we find the universal response in universal variables Y . We separate Y = {y 1 . . . y m } and we can start with a response c to y 1 and then find an S+∀Exp 0,1 refutation of ∀y 2 . . . y m Πφ| ,c/y1 . We make sure the proofs do not increase in size. Then we can repeat this for each variable in Y in turn.

Suppose we have an S+∀Exp 0,1 refutation π i of the QBF ∀y i . . . y m Πφ| ,μi , where μ i 1 ≤ i ≤ m is a Boolean assignment to variables {y 1 , . . . , y i−1 }. The variables of subexp πi (∀y i . . . y m Πφ| ,μi ) can be partitioned into Z 0/yi = {z α | z ∈ Z, α(y i ) = 0} and Z 1/yi = {z α | z ∈ Z, α(y i ) = 1}. This completely partitions the variables because y i is leftmost in the prefix.

Conjunct C ∈ subexp πi (Πφ)| ,μi cannot mix variables Z 0/yi and Z 1/yi since the axiom rule in Definition 1 substitutes one or the other everywhere in the conjunct. Therefore subexp πi (∀y i . . . y m Πφ| ,μi ) can be written as A(Z 0/yi ) ∧ B(Z 1/yi ) with S refutation π i (based on the S+∀Exp 0,1 refutation π i ).

We define a new partial assignment μ i+1 , which is defined as μ i+1 (y j ) = μ i (y j ) for 1 ≤ j < i. Now we can use condition 2 to extract from π i an S refutation π i+1 of either A(Z 0/yi ) or B(Z 1/yi ) in polynomial time. If it is A(Z 0/yi ) then we let μ i+1 (y i ) = 0 and if it is B(Z 1/yi ) then we let μ i+1 (y i ) = 1. π i+1 can be used as part of an S+∀Exp 0,1 refutation π i+1 of ∀y i+1 . . . y m Πφ| ,μi+1 as subexp πi+1 (∀y i+1 . . . y m Πφ| ,μi+1 ) is equal to A(Z 0/yi ) or B(Z 1/yi ). Condition 2 guarantees |π i+1 | ≤ |π i | so |π i+1 | ≤ |π i | as well.

Once we get to μ m we have a complete assignment to Y and a guarantee that the remaining QBF game on Πφ| ,μm is false by the S+∀Exp 0,1 refutation π m , with |π m | ≤ |π|.

We can repeat this procedure for every universal block and we end up with the false proposition ⊥ and since our proofs are non-increasing in size in each step we guarantee this can be done in a polynomial time procedure.

We have answered an open question in QBF proof complexity by showing that refutational QRAT does not have strategy extraction, and have introduced a family of QBFs witnessing this fact. We have also formalised one condition for strategy extraction to be present in QBF proof systems using universal expansion. This adds to an existing awareness of the trade-off between strength of QBF proof systems and the ability to offer explanation via winning strategies [4] .

In current QBF solvers that use inference from propositional SAT solvers implementing CDCL the propositional inference used is Resolution and the feasible interpolation property applies. As such it may be possible (as it is indeed possible in ∀Exp+Res) to have both expansion solving and strategy extraction together. There is also hope that, because the Cutting Planes proof system [10] has feasible interpolation [24] , strategy extraction may still be compatible with QBF expansion if we were to use pseudo-Boolean solvers as a propositional component in QBF solvers.

However, if SAT solvers are developed with more power than both Resolution and Cutting Planes, then the problem of having both strategy extraction and expansion in QBF solvers becomes more serious. Extended Resolution is strong enough to cause these issues [22] , but there is a degree of non determinism required in choosing the correct extension variables in practice. In the case of our Select and Duality formulas this task would be to find the eq extension variables, despite the fact we are linearly increasing the number of variables this way and increasing the search space for the solver.

Resolution proofs and skolem functions in QBF evaluation and applications

Lower bounds: from circuits to QBF proof systems

Short proofs in QBF expansion

Proof complexity of resolution-based QBF calculi

Feasible interpolation for QBF resolution calculi

Understanding cutting planes for QBFs

Reasons for hardness in QBF proof systems

The equivalences of refutational QRAT

The relative efficiency of propositional proof systems

On the complexity of cutting-plane proofs

Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory

A uniform approach for generating proofs and strategies for both true and false QBF formulas

Efficient extraction of Skolem functions from QRAT proofs

A unified proof system for QBF preprocessing

Solving QBF with counterexample guided refinement

Expansion-based QBF solving versus Q-resolution

A little blocked literal goes a long way

QRAT polynomially simulates ∀-Exp+Res

Theory of quantified Boolean formulas

Resolution for quantified Boolean formulas

Interpolation theorems, lower bounds for proof systems and independence results for bounded arithmetic

Some consequences of cryptographical conjectures for S 1 2 and EF

QRAT + : generalizing QRAT by a more powerful QBF redundancy property

Lower bounds for resolution and cutting planes proofs and monotone computations