How QBF Expansion Makes Strategy Extraction Hard
 164 Downloads
Abstract
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 PSPACEhard 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.
Keywords
QBF Proof complexity QRAT Strategy extraction Quantifier expansion Feasible interpolation1 Introduction
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 PSPACEcomplete. 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 QRes proof system [20]. QBF expansion, on the other hand, adds the universal expansion rule such as in the proof system Open image in new window [16]. Both QRes and Open image in new window 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 QRes and Open image in new window 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 Open image in new window was shown to polynomially simulate the QCDCL calculus QRes on bounded quantifier alternations.
As well as using the calculi QRes and Open image in new window 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 QRes 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 QRes 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 superpolynomial interpolant size lower bounds become superpolynomial 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 PSPACEhard 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 Open image in new window [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 PSPACEhard 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.
2 Preliminiaries
2.1 Proof Complexity
Let \(\mathsf {\Gamma }\) be an alphabet, with \(\mathsf {\Gamma }^*\) being the set of strings over \(\mathsf {\Gamma }\). Let \(\mathcal {L}\) be a language over \(\mathsf {\Gamma }\), in other words \(\mathcal {L}\subset \mathsf {\Gamma }^*\). A proof system [9] for \(\mathcal {L}\) is a polynomial time computable partial function \(f:\mathsf {\Gamma }^\star \rightharpoondown \mathsf {\Gamma }^\star \) with range \(\mathcal {L}\). The size \(\pi \) of a proof \(\pi \) in \(\mathsf {\Gamma }^\star \) 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)\subseteq \mathcal {L}\) and completeness that \( rng (f)\supseteq \mathcal {L}\). Given a family \(\{c_i \mid i \in \mathbb {N} \}\) of formulas \(f_i \in \mathcal {L}\), and a family of fproofs \(P=\{p_i \mid , i \in \mathbb {N} \}\) such that \(f(p_i)=c_i\) we can say that \(p_i\) is polynomially bounded if \(p_i \le c_i^{O(1)}\). An even stronger property is that P is said to be uniform if there is a polynomialtime function h such that \(h(c_i)=p_i\).
In propositional logic a literal is a Boolean variable x or its negation \(\lnot {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\) then \(\bar{l} = \lnot {x}\), if \(l = \lnot {x}\) then \(\bar{l} = 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 \in \phi \) and \(l \in C\) to state that clause C appears in \(\phi \) 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 \vee 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\cup E\) to denote the disjunction of all literals that appear in either clause D or E. An assignment \(\tau \) for a formula \(\phi \) over n variables is a partial function from the variables of \(\phi \) to \(\{0,1\}^n\). \(\tau (C)\) is the result of evaluating clause C under assignment \(\tau \), and \(\phi _\tau = \{ \tau (C) \  \ C \in \phi \}\). For formula (or circuit) \(\phi \), we define \(\phi [b/x]\) so that all instances of variable x in \(\phi \) are replaced with \(b \in \{0,1\}\).
2.2 Quantified Boolean Formulas
Quantified Boolean formulas (QBF) extend propositional logic by allowing for Boolean variables to be universally or existentially quantified [19]. \(\forall x\,\varPsi \) is satisfied by the same truth assignments as \(\varPsi [0/x]\wedge \varPsi [1/x]\) and \(\exists x\,\varPsi \) is satisfied by the same truth assignments as \(\varPsi [0/x]\vee \varPsi [1/x]\). In a closed QBF all variables must be quantified. A prenex QBF \(\varPsi \) consists of a prefix \(\varPi \) defining how each variable is quantified and a propositional part \(\phi \) called the matrix. We write \(\varPsi = \varPi \phi \). The prefix \(\varPi \) 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 Open image in new window . 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.
2.3 Winning Strategies
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 \(\varPi \phi \) 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 \(\varPi \), 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 \(\varPi \phi \) (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.
2.4 Expansion Based Proof Systems
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.
In fact for any refutational propositional proof system \(\mathsf 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 \(\mathsf 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.
Open image in new window We start with a propositional proof system \(\mathsf S\) and prenex QBF \(\varPsi = \varPi \phi \), where \(\varPi \) is the quantifier prefix and \(\phi \) is a propositional matrix in variables of \(\varPi \). We treat \(\phi \) as a conjunction of formulas.
Let \(\tau \) be a full assignment to all universal variables and let l be an existentially quantified literal. We define Open image in new window to be the partial assignment of \(\tau \) 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^\tau \), where C is a propositional formula in both existential and universal variables.
\(C^\tau \) is the same as C except that we replace every existential literal l with the annotated literal Open image in new window and every universal variable u with its value \(\tau (u)\).
Definition 1
The refutational QBF proof system Open image in new window allows the instantiation of axiom \(C^\tau \), whenever C is a conjunct from the matrix and \(\tau \) is an assignment to all universal variables; it generates an \(\mathsf S\) refutation of the conjunction of the axioms, treating differently annotated variables as different.
An Open image in new window proof [2] \(\pi \) of QBF \(\varPsi \) therefore consists of a propositional \(\mathsf S\) proof of a subconjunction of the full expansion. We denote this conjunction as \(\mathsf {subexp}_\pi (\varPsi )\).
A wellknown example of Open image in new window is Open image in new window [16] which is obtained when \(\mathsf 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.
2.5 QRAT
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 \(\varPi \phi \) 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 \(\varPi \phi \).
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, then \(\bar{C}\) is the conjunction of the negation of the literals in C. Unit propagation is a procedure on a formula \(\phi \) in CNF that builds a partial assignment \(\tau \). This assignment is applied to \(\phi \) and then for any literal l that appears in a singleton (unit) clause in the resulting formula, the assignment satisfying l is added to \(\tau \). This is repeated until reaching fixpoint, which must happen in polynomial time in the number of clauses in \(\phi \). Unit propagation is used extensively in QRAT for deciding whether a derivation rule may be applied. We denote by \( \phi \vdash _{1} \bot \) that unit propagation derives the empty clause from \(\phi \).
In the following definitions, \(\varPi \phi \) is a closed PCNF and C a clause not in \(\phi \). \(\varPi '\) is a prefix including the variables of \(\phi \) and C, \(\varPi \) is identical to \(\varPi '\) except that it contains the variables of \(\phi \) only.
Definition 2 (Asymmetric Tautology Addition (ATA))
Definition 3 (Outer Clause)
Suppose C contains a literal l. Consider all clauses D in \(\phi \) with \(\bar{l} \in D\). The outer clause \(O^l_D\) of D is Open image in new window .
Definition 4 (Quantified Resolution Asymmetric Tautology Addition (QRATA))
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].
Definition 5 (Extended Universal Reduction (EUR))
Given a clause \(C\vee u\) with universal literal u, consider extending C by
Open image in new window or \( k= \bar{u} \}\),
We can also define a weaker version of QRAT, QRAT(UR), which uses universal reduction instead of EUR.
Definition 6 (Universal Reduction (UR))
3 Cheating a QBF Game
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 PSPACEhard 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.
3.1 Duality Formulas
Let X be the set of variables \(\{x_1, \dots , x_{2n} \}\) and \(\phi (X)\) a CNF in the variables of X. Then \(\varPi \phi (X)\) with prefix \(\varPi = \forall x_1 \exists x_2 \forall x_3 \dots \exists x_{2n}\) is a closed PCNF. We also define a second set of 2n variables \(X'= \{x'_1, \dots , x'_{2n}\}\) and an alternative prefix \(\varPi '= \exists x'_1 \forall x'_2 \exists x'_3 \dots \forall x'_{2n}\). The QBF \(\varPi \phi (X)\wedge \varPi ' \lnot \phi (X')\) is necessarily false. However this QBF is not in PCNF, which many proof systems require.

For literal l if \(l=x_i\) then \(l'= x'_i\) and if \(l=\lnot x_i\) then \(l'=\lnot x'_i\).

For each clause K in \(\phi (X)\) we denote the corresponding clause in \(\phi (X')\) as \(K'\) so that \(K'= \bigvee _{l\in K} l'\).
We require that \(\bar{\phi }(X', T)\) is true precisely when \(\phi (X')\) is false. We will introduce clauses stating that variable \(t_K\) is true if and only if clause \(K'\) is satisfied. Then \(\phi (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.

\(\left( \lnot {t_K} \vee K' \right) \) for each clause K in \(\phi (X)\)

\(\left( \lnot {l'} \vee t_K \right) \) for each literal l in K and each K in \(\phi (X)\)

\(\left( \bigvee _{K\in \phi (X)} \lnot t_K \right) \)
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 \(\varPsi = \varPi \phi \) we generate a formula Open image in new window encoding in PCNF the claim that both \(\varPsi \) and its negation are true:
3.2 Short Proofs of Duality Formulas
In [6], Beyersdorff et al. showed short Open image in new window proofs of a family of QBFs that take an input of a graph and state that there is a kclique (Clique) and dually that there is no kclique (CoClique). The short proofs exploited the fact that the CoClique part of the formula was structured in a similar way to the Clique part.
We generalise this approach here for short proofs of the Open image in new window formulas. First we will give a sketch proof of how this can be done using Open image in new window rules before we show those short proofs formally in QRAT. Open image in new window is simply a propositional Frege system augmented with the Open image in new window rule for removing universally quantified variables. Open image in new window allows to substitute a Boolean value for universally quantified u in a previously derived line, provided that Open image in new window for all existentially quantified x in the proof line.
The clauses in Open image in new window state \(\bigwedge _K \ (t_K \leftrightarrow K')\), \(\bigvee _K \ \lnot {t_K}\) and \(\bigwedge K\).
We therefore conclude that Open image in new window .
Now \(x_{2n1}\) 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.
Theorem 1
Given a formula Open image in new window we can in polynomial time construct a quadratic size QRAT(UR) refutation of Open image in new window .
Proof
Let K be the number of literals in clause \(K \in \phi \), then Open image in new window . Recall \(\varPi \phi \) has 2n variables.

\((\lnot {x_i} \vee x'_i \vee \lnot {\mathrm {eq}_{x_i}})\)

\((x_i \vee \lnot {x'_i} \vee \lnot {\mathrm {eq}_{x_i}})\)

\((\lnot {x_i} \vee \lnot {x'_i} \vee \mathrm {eq}_{x_i})\)

\((x_i \vee x'_i \vee \mathrm {eq}_{x_i})\)
Recall that adding a clause by QRATA requires that we have an existential literal l in the new clause C such that \(\phi \wedge \bar{C} \wedge \bar{O}^l_D \vdash _{1} \bot \) for all D with \(\bar{l} \in D\). For the first two clauses this is vacuously satisfied with \(l = \lnot {\mathrm {eq}_{x_i}}\) since \(\mathrm {eq}_{x_i}\) does not appear positively anywhere in the formula. To add the latter clauses we have \(l = \mathrm {eq}_{x_i}\) and must consider the two outer clauses \((\lnot {x_i} \vee x'_i )\) and \( (x_i \vee \lnot {x'_i})\). The QRATA condition is satisfied for \((\lnot {x_i} \vee \lnot {x'_i} \vee \mathrm {eq}_{x_i})\) because \(x_i \wedge x'_i \wedge x_i \wedge \lnot {x'_i} \vdash _{1} \bot \) and \(x_i \wedge x'_i \wedge \lnot {x_i} \wedge x'_i \vdash _{1} \bot \), and similarly for the final clause.
For each of the original 2n variables in \(\varPi \phi \) we have added four clauses of constant size. Following O(n) steps the formula has increased in length by O(n) characters.
NonEquivalence of Xand \(X'\). The next three ATA steps are equivalent to those in the derivation of \(\bigvee _{i=1}^{2n} \ \lnot {(x_i \leftrightarrow x'_i)}\) in the sketch proof above.

\((\bigvee _{i=1}^{2n} \lnot {\mathrm {eq}_{x_i}} \vee t_K \vee \bar{l})\) for every \(K \in \phi (X)\) and every \(l \in K\)

\((\bigvee _{i=1}^{2n} \lnot {\mathrm {eq}_{x_i}} \vee t_K)\) for every \(K \in \phi (X)\)

\((\bigvee _{i=1}^{2n} \lnot {\mathrm {eq}_{x_i}})\)
Each clause has O(n) literals and there are at most \(\phi \) clauses of each type. In \(O(\phi )\) proof steps the formula has increased in length by \(O(n\phi )\).

\((\bigvee _{i=1}^{j1} \lnot {\mathrm {eq}_{x_i}} \vee x_j \vee x'_j)\)

\( (\bigvee _{i=1}^{j1} \lnot {\mathrm {eq}_{x_i}} \vee \lnot {x_j} \vee \lnot {x'_j})\)
In these clauses whichever of \(x_j\) and \(x'_j\) is universally quantified is innermost by the construction of Open image in new window and the decision of where to introduce the variables \(\mathrm {eq}_{x_i}\) in the prefix. Without loss of generality, assume \(x'_j\) is universally quantified so we can use UR to derive clauses \((\bigvee _{i=1}^{j1} \lnot {\mathrm {eq}_{x_i}} \vee x_j)\) and \((\bigvee _{i=1}^{j1} \lnot {\mathrm {eq}_{x_i}} \vee \lnot {x_j})\), then ATA allows to add the resolvent \(A_j\).
For each of the 2n variables from \(\phi \) there are five proof steps in this final part of the refutation, each introducing a new clause of size O(n), and in total the formula has increased in length by \(O(n^2)\). The whole refutation therefore has size Open image in new window . \(\square \)
4 Making Strategies Hard
4.1 Short Proofs of Select Formulas in QRAT
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 Open image in new window to show that refutational QRAT does not have strategy extraction under a strong complexity assumption.
Theorem 2
QRAT has short uniform proofs of Open image in new window for any QBF \(\varPi \phi \).
Proof
The first step in the proof is to use Extended Universal Reduction (EUR) to remove u from all clauses in \(\phi _u(X)\) and \(\lnot u\) from all clauses in \(\bar{\phi }_{\lnot {u}}(X', T)\). Using EUR to reduce l in C requires that \(\bar{l}\) 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 \(\lnot {u}\) appear in sections of the formula that have no other variables in common. Hence we can always reduce u (and \(\lnot {u}\)) in Open image in new window .
Having performed these (polynomially many) EUR steps the formula is identical to Open image in new window , which is uniformly refuted as in Theorem 1. \(\square \)
Corollary 1
Refutational QRAT does not have strategy extraction unless P = PSPACE.
Proof
If QRAT has strategy extraction we can decide the truth of closed QBF in polynomial time – a PSPACEcomplete problem.
Given a QBF \(\varPi \phi \), with \(\varPi \) a prefix and \(\phi \) a propositional formula in the variables of \(\varPi \), we create the formula Open image in new window and then in polynomial time we can output the proofs as in Theorem 2. Then from the proof of Open image in new window 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 \(\bar{\phi }_{\lnot {u}}(X', T)\) are immediately satisfied so we know that the rest of the extracted strategy is a strategy for \(\varPi \phi \), showing that \(\varPi \phi \) is false. Similarly, if the strategy sets \(u=1\) then it must be the case that \(\bar{\phi }_{\lnot {u}}(X', T)\) is false and so, by construction, \(\varPi \phi \) is true. Therefore we have a polynomial time decision procedure for an arbitrary QBF. \(\square \)
In fact, the full power of EUR is not required. QRAT(UR) is capable of refuting the formulas Open image in new window , and the initial EUR step can be replaced by universal expansion of u, producing a formula equivalent to Open image in new window 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 Open image in new window formulas show that a single initial expansion step may be sufficient to prevent strategy extraction.
5 Relation to Feasible Interpolation
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 \(\varPi \phi \) in order to have strategy extraction for Open image in new window . We can think of a strategy for u acting as a circuit deciding between \(\varPi \phi \) and \(\lnot (\varPi \phi )\). 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) \rightarrow B(P,R)\) (or, equivalently, a false conjunction \(A(P,Q) \wedge \lnot 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) \rightarrow 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 Open image in new window formulas are created from the Open image in new window formulas.
Theorem 3
Given any propositional refutation system \(\mathsf S\), if the refutational QBF proof system Open image in new window has strategy extraction then \(\mathsf S\) must have feasible interpolation.^{1}
Proof
Suppose Open image in new window has strategy extraction and we have an \(\mathsf S\)refutation \(\pi \) of \(A(P,Q) \wedge B(P,R)\) with P, Q, R disjoint sets of variables. We will show that we can find an interpolant in polynomial time.
We can now refute this using \(\pi \) 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 \(\mathsf 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) \wedge B(P,R)\). \(\square \)
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 Open image in new window has strategy extraction. This is done by a “roundbased” 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 Open image in new window 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 Open image in new window whenever refutational proof system \(\mathsf 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.
Theorem 4
 1.
\(\mathsf S\) is closed under restriction, meaning that from a refutation \(\pi \)of \(\phi \) one can extract in polynomial time an \(\mathsf S\) refutation \(\pi _\epsilon \) of \(\phi _\epsilon \) for any assignment \(\epsilon \) with \(\pi _\epsilon \le \pi \).
 2.
From any refutation \(\rho _1\) in \(\mathsf S\) of \(A(Q)\wedge B(R)\) where Q, R share no common variables another refutation \(\rho _{2}\) of either A(Q) or B(R) can be extracted in polynomial time with \(\rho _{2}\le \rho _1\).
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 boundeddepth Frege to have the second property.
Proof
Suppose we have a closed prenex QBF \(\exists X \forall Y \varPi \phi \) where \(\varPi \) is a prefix in variables Z and \(\phi \) is a propositional matrix with variables in X,Y and Z. Now suppose we have an Open image in new window refutation \(\pi \) of \(\exists X \forall Y \varPi \phi \). This gives an \(\mathsf S\) proof \(\pi '\) of \(\mathsf {subexp}_\pi (\exists X \forall Y \varPi \phi )\), a subset of the full expansion of \(\exists X \forall Y \varPi \phi \) using \(\pi \).
We will show that under conditions 4 and 2 we have a polynomial time procedure that takes any assignment \(\epsilon \) to X and outputs a response \(\mu \) in Y and a \(\varPi \phi _{\epsilon , \mu }\) refutation in Open image in new window .
From \(\pi '\), we can extract \(\pi '_\epsilon \) in polynomial time, using condition 4, which provides an \(\mathsf S\) refutation of \(\mathsf {subexp}_\pi ( \exists X\forall Y \varPi \phi )_\epsilon \). For \(D\in \phi \) we have that \(C=D_\epsilon \) is in \(\phi _\epsilon \), so every conjunct \(D^\tau _\epsilon \) of \(\mathsf {subexp}_\pi ( \exists X\forall Y \varPi \phi )_\epsilon \) is also an axiom \(C^\tau \) of \(\forall Y \varPi \phi _\epsilon \). Therefore, \(\pi '_\epsilon \) becomes an Open image in new window refutation \(\pi _\epsilon \) of \(\forall Y \varPi \phi _\epsilon \).
Now we find the universal response in universal variables Y. We separate \(Y=\{y_1 \dots y_m\}\) and we can start with a response c to \(y_1\) and then find an Open image in new window refutation of \(\forall y_2 \dots y_m \varPi \phi _{\epsilon , c/y_1}\). 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 Open image in new window refutation \(\pi _i\) of the QBF \(\forall y_i \dots y_m \varPi \phi _{\epsilon , \mu _i}\), where \(\mu _i\) \( 1\le i\le m\) is a Boolean assignment to variables \(\{y_1, \dots , y_{i1}\}\). The variables of \(\mathsf {subexp}_{\pi _i}(\forall y_i \dots y_m \varPi \phi _{\epsilon , \mu _i})\) can be partitioned into \(Z_{0/y_i}= \{z^\alpha \mid z\in Z, \alpha (y_i)=0\}\) and \(Z_{1/y_i}= \{z^\alpha \mid z\in Z, \alpha (y_i)=1\}\). This completely partitions the variables because \(y_i\) is leftmost in the prefix.
Conjunct \(C \in \mathsf {subexp}_{\pi _i}(\varPi \phi )_{\epsilon , \mu _i}\) cannot mix variables \(Z_{0/y_i}\) and \(Z_{1/y_i}\) since the axiom rule in Definition 1 substitutes one or the other everywhere in the conjunct. Therefore \(\mathsf {subexp}_{\pi _i}(\forall y_i \dots y_m \varPi \phi _{\epsilon , \mu _i})\) can be written as \(A(Z_{0/y_i})\wedge B(Z_{1/y_i})\) with \(\mathsf S\) refutation \(\pi '_i\) (based on the Open image in new window refutation \(\pi _i\)).
We define a new partial assignment \(\mu _{i+1}\), which is defined as \(\mu _{i+1}(y_j)=\mu _{i}(y_j)\) for \(1\le j <i\). Now we can use condition 2 to extract from \(\pi '_i\) an \(\mathsf S\) refutation \(\pi '_{i+1}\) of either \(A(Z_{0/y_i})\) or \(B(Z_{1/y_i})\) in polynomial time. If it is \(A(Z_{0/y_i})\) then we let \(\mu _{i+1}(y_i)= 0\) and if it is \(B(Z_{1/y_i})\) then we let \(\mu _{i+1}(y_i)= 1\). \(\pi '_{i+1}\) can be used as part of an Open image in new window refutation \(\pi _{i+1}\) of \(\forall y_{i+1} \dots y_m \varPi \phi _{\epsilon , \mu _{i+1}}\) as \(\mathsf {subexp}_{\pi _{i+1}}(\forall y_{i+1} \dots y_m \varPi \phi _{\epsilon , \mu _{i+1}})\) is equal to \(A(Z_{0/y_i})\) or \(B(Z_{1/y_i})\). Condition 2 guarantees \(\pi '_{i+1} \le \pi '_{i}\) so \(\pi _{i+1} \le \pi _{i}\) as well.
Once we get to \(\mu _{m}\) we have a complete assignment to Y and a guarantee that the remaining QBF game on \(\varPi \phi _{\epsilon ,\mu _m}\) is false by the Open image in new window refutation \(\pi _m\), with \(\pi _m\le \pi \).
We can repeat this procedure for every universal block and we end up with the false proposition \(\bot \) and since our proofs are nonincreasing in size in each step we guarantee this can be done in a polynomial time procedure. \(\square \)
6 Conclusion
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 tradeoff 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 Open image in new window ) 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 pseudoBoolean 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 Open image in new window and Open image in new window formulas this task would be to find the \(\mathrm {eq}\) extension variables, despite the fact we are linearly increasing the number of variables this way and increasing the search space for the solver.
Footnotes
 1.
Provided the refutations of \(\mathsf S\) work independently of the variable names. This is usually the case but one could create a pathological proof proof system where annotated variables are treated differently to normal ones.
References
 1.Balabanov, V., Jiang, J.H.R.: Resolution proofs and skolem functions in QBF evaluation and applications. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 149–164. Springer, Heidelberg (2011). https://doi.org/10.1007/9783642221101_12CrossRefGoogle Scholar
 2.Beyersdorff, O., Bonacina, I., Chew, L.: Lower bounds: from circuits to QBF proof systems. In: Proceedings of the ACM Conference on Innovations in Theoretical Computer Science (ITCS 2016), pp. 249–260. ACM (2016)Google Scholar
 3.Beyersdorff, O., Chew, L., Clymo, J., Mahajan, M.: Short proofs in QBF expansion. In: Janota, M., Lynce, I. (eds.) SAT 2019. LNCS, vol. 11628, pp. 19–35. Springer, Cham (2019). https://doi.org/10.1007/9783030242589_2CrossRefGoogle Scholar
 4.Beyersdorff, O., Chew, L., Janota, M.: Proof complexity of resolutionbased QBF calculi. In: Proceedings of the Symposium on Theoretical Aspects of Computer Science, pp. 76–89. LIPIcs series (2015)Google Scholar
 5.Beyersdorff, O., Chew, L., Mahajan, M., Shukla, A.: Feasible interpolation for QBF resolution calculi. Logical Methods Comput. Sci. 13(2) (2017). https://doi.org/10.23638/LMCS13(2:7)2017. https://lmcs.episciences.org/3702
 6.Beyersdorff, O., Chew, L., Mahajan, M., Shukla, A.: Understanding cutting planes for QBFs. Inf. Comput. 262, 141–161 (2018). https://doi.org/10.1016/j.ic.2018.08.002. http://www.sciencedirect.com/science/article/pii/S0890540118301184
 7.Beyersdorff, O., Hinde, L., Pich, J.: Reasons for hardness in QBF proof systems. In: Electronic Colloquium on Computational Complexity (ECCC) 24, Report no. 44 (2017). https://eccc.weizmann.ac.il/report/2017/044
 8.Chew, L., Clymo, J.: The equivalences of refutational QRAT. In: Janota, M., Lynce, I. (eds.) SAT 2019. LNCS, vol. 11628, pp. 100–116. Springer, Cham (2019). https://doi.org/10.1007/9783030242589_7zbMATHCrossRefGoogle Scholar
 9.Cook, S.A., Reckhow, R.A.: The relative efficiency of propositional proof systems. J. Symb. Logic 44(1), 36–50 (1979)MathSciNetzbMATHCrossRefGoogle Scholar
 10.Cook, W.J., Coullard, C.R., Turán, G.: On the complexity of cuttingplane proofs. Discret. Appl. Math. 18(1), 25–38 (1987)MathSciNetzbMATHCrossRefGoogle Scholar
 11.Craig, W.: Three uses of the HerbrandGentzen theorem in relating model theory and proof theory. J. Symb. Logic 22(3), 269–285 (1957)MathSciNetzbMATHCrossRefGoogle Scholar
 12.Goultiaeva, A., Van Gelder, A., Bacchus, F.: A uniform approach for generating proofs and strategies for both true and false QBF formulas. In: Walsh, T. (ed.) International Joint Conference on Artificial Intelligence IJCAI, pp. 546–553. IJCAI/AAAI (2011)Google Scholar
 13.Heule, M., Seidl, M., Biere, A.: Efficient extraction of Skolem functions from QRAT proofs. In: Formal Methods in ComputerAided Design, FMCAD 2014, Lausanne, Switzerland, 21–24 October 2014, pp. 107–114 (2014). https://doi.org/10.1109/FMCAD.2014.6987602
 14.Heule, M.J.H., Seidl, M., Biere, A.: A unified proof system for QBF preprocessing. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 91–106. Springer, Cham (2014). https://doi.org/10.1007/9783319085876_7CrossRefGoogle Scholar
 15.Janota, M., Klieber, W., MarquesSilva, J., Clarke, E.: Solving QBF with counterexample guided refinement. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 114–128. Springer, Heidelberg (2012). https://doi.org/10.1007/9783642316128_10CrossRefGoogle Scholar
 16.Janota, M., MarquesSilva, J.: Expansionbased QBF solving versus Qresolution. Theor. Comput. Sci. 577, 25–42 (2015)MathSciNetzbMATHCrossRefGoogle Scholar
 17.Kiesl, B., Heule, M.J.H., Seidl, M.: A little blocked literal goes a long way. In: Gaspers, S., Walsh, T. (eds.) SAT 2017. LNCS, vol. 10491, pp. 281–297. Springer, Cham (2017). https://doi.org/10.1007/9783319662633_18CrossRefGoogle Scholar
 18.Kiesl, B., Seidl, M.: QRAT polynomially simulates \(\forall \text{Exp+Res }\). In: Janota, M., Lynce, I. (eds.) SAT 2019. LNCS, vol. 11628, pp. 193–202. Springer, Cham (2019). https://doi.org/10.1007/9783030242589_13CrossRefGoogle Scholar
 19.Kleine Büning, H., Bubeck, U.: Theory of quantified Boolean formulas. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 735–760. IOS Press (2009)Google Scholar
 20.Kleine Büning, H., Karpinski, M., Flögel, A.: Resolution for quantified Boolean formulas. Inf. Comput. 117(1), 12–18 (1995)MathSciNetzbMATHCrossRefGoogle Scholar
 21.Krajíček, J.: Interpolation theorems, lower bounds for proof systems and independence results for bounded arithmetic. J. Symb. Logic 62(2), 457–486 (1997)MathSciNetzbMATHCrossRefGoogle Scholar
 22.Krajíček, J., Pudlák, P.: Some consequences of cryptographical conjectures for \(S^1_2\) and \(EF\). Inf. Comput. 140(1), 82–94 (1998)MathSciNetzbMATHGoogle Scholar
 23.Lonsing, F., Egly, U.: \({\sf QRAT}^{+}\): generalizing QRAT by a more powerful QBF redundancy property. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) IJCAR 2018. LNCS (LNAI), vol. 10900, pp. 161–177. Springer, Cham (2018). https://doi.org/10.1007/9783319942056_12CrossRefGoogle Scholar
 24.Pudlák, P.: Lower bounds for resolution and cutting planes proofs and monotone computations. J. Symb. Logic 62(3), 981–998 (1997)MathSciNetzbMATHCrossRefGoogle Scholar