{'fraction_non_alphanumeric': 0.04407353823352977, 'fraction_numerical': 0.009209922721338085, 'mean_word_length': 4.2301374919258095, 'pattern_counts': {'":': 0, '<': 14, '<?xml version=': 0, '>': 1, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 18, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Long-Distance Q-Resolution with Dependency Schemes

Resolution proof systems for quantified Boolean formulas (QBFs) provide a formal model for studying the limitations of state-of-the-art search-based QBF solvers that use these systems to generate proofs. We study a combination of two proof systems supported by the solver DepQBF: Q-resolution with generalized universal reduction according to a dependency scheme and long distance Q-resolution. We show that the resulting proof system—which we call long-distance Q(D)-resolution—is sound for the reflexive resolution-path dependency scheme. In fact, we prove that it admits strategy extraction in polynomial time. This comes as an application of a general result, by which we identify a whole class of dependency schemes for which long-distance Q(D)-resolution admits polynomial-time strategy extraction. As a special case, we obtain soundness and polynomial-time strategy extraction for long distance Q(D)-resolution with the standard dependency scheme. We further show that search-based QBF solvers using a dependency scheme D and learning with long-distance Q-resolution generate long-distance Q(D)-resolution proofs. The above soundness results thus translate to partial soundness results for such solvers: they declare an input QBF to be false only if it is indeed false. Finally, we report on experiments with a configuration of DepQBF that uses the standard dependency scheme and learning based on long-distance Q-resolution.


Introduction
Quantified Boolean formulas (QBFs) offer succinct encodings for problems from domains such as formal verification, synthesis, and planning [5,13,16,30,38,43]. Although the combination of (more verbose) propositional encodings with SAT solvers is still the state-of-the-art approach to many of these problems, QBF solvers are gaining ground. An arsenal of new techniques has been introduced over the past few years [10,11,14,22,23,25,26,29,32,33,35], and these advances in solver technology have been accompanied by the development of a better understanding of the underlying QBF proof systems and their limitations [4,[7][8][9]12,18,27,42].
Search-based solvers implementing the QCDCL algorithm [15,46] represent one of the principal state-of-the-art approaches in QBF solving. Akin to modern SAT solvers, these solvers rely on successive variable assignments in combination with fast constraint propagation and learning. Unlike SAT solvers, however, search-based QBF solvers are constrained by the variable dependencies induced by the quantifier prefix: 1 while SAT solvers can assign variables in any order, search-based QBF solvers can only assign variables from the leftmost quantifier block that contains unassigned variables, since the assignment of a variable further to the right might depend on the variable assignment to this block. In the most extreme case, this forces solvers into a fixed order of variable assignments, rendering decision variable heuristics ineffective.
The search-based solver DepQBF uses dependency schemes to partially bypass this restriction [10,31]. Dependency schemes can sometimes identify pairs of variables as independent, allowing the solver to assign them in any order. This gives decision heuristics more freedom and results in increased performance [10].
While this provides a strong motivation to use dependency schemes, their integration with QCDCL poses challenges of its own. Soundness of the proof system underlying QCDCL with the standard dependency scheme as implemented in DepQBF was shown only recently [42], and combining other state-of-the-art techniques with dependency schemes is often highly nontrivial. In this paper, we focus on two such issues: (a) Long-distance Q-resolution permits the derivation of tautological clauses in certain cases [2,45,47]. This system can be used in constraint learning as an alternative to Q-resolution, leading to fewer backtracks during search and, sometimes, reduced runtime [19]. In addition, clause learning based on long-distance Q-resolution is substantially easier to implement. However, it is open whether QCDCL with learning based on long-distance Q-resolution is sound when combined with known dependency schemes. (b) For applications in verification and synthesis, it is not enough for solvers to decide whether an input QBF is true or false-they also have to generate a certificate. Such certificates can be efficiently constructed from Q-resolution [2] and even long-distance Q-resolution proofs [3]. However, it is not clear whether this is possible for proofs generated by QCDCL with the standard dependency scheme. We define LDQ(D)-resolution as consisting of long-distance Q-resolution with a dependency scheme D, and show that a search-based QBF solver using dependency scheme D and learning based on long-distance Q-resolution generates an LDQ(D)-resolution refutation whenever it declares an input QBF to be false. This allows us to partially address (a) by showing that longdistance Q-resolution combined with the reflexive resolution-path dependency scheme [42] is sound. In fact, we prove that this proof system allows for certificate extraction in polynomial time, thus resolving (b) as well. These results also hold for long-distance Q-resolution 2 Preliminaries

Formulas and Assignments
A literal is a negated or unnegated variable. If x is a variable, we write x = ¬x and ¬x = x, and let var(x) = var(¬x) = x. We sometimes call literals x and ¬x the positive and negative polarity of variable x. If X is a set of literals, we write X for the set { x : x ∈ X }. A clause is a finite disjunction of literals, and a term is a finite conjunction of literals. We call a clause tautological if it contains the same variable negated as well as unnegated. A CNF formula is a finite conjunction of non-tautological clauses. Whenever convenient, we treat clauses and terms as sets of literals, and CNF formulas as sets of sets of literals. We write var(S) for the set of variables occurring (negated or unnegated) in a clause or term S, that is, var(S) = { var( ) : ∈ S }. Moreover, we let var(ϕ) = C∈ϕ var(C) denote the set of variables occurring in a CNF formula ϕ.
A truth assignment (or simply assignment) to a set X of variables is a mapping τ : X → {0, 1}. We write [X ] for the set of truth assignments to X , and extend τ : X → {0, 1} to literals by letting τ (¬x) = 1 − τ (x) for x ∈ X . Let τ : X → {0, 1} be a truth assignment.

PCNF Formulas
A PCNF formula is denoted by Φ = Q.ϕ, where ϕ is a CNF formula and Q = Q 1 X 1 . . . Q n X n is a sequence such that Q i ∈ {∀, ∃}, Q i = Q i+1 for 1 ≤ i < n, and the X i are pairwise disjoint sets of variables. We call ϕ the matrix of Φ and Q the (quantifier) prefix of Φ, and refer to the X i as quantifier blocks. We require that var(ϕ) = X 1 ∪ · · · ∪ X n and write var(Φ) = var(ϕ). We define a partial order < Φ on var(ϕ) as x < Φ y ⇔ x ∈ X i , y ∈ X j , i < j. We extend < Φ to a relation on literals in the obvious way and drop the subscript whenever Φ is understood. For x ∈ var(Φ) we let R Φ (x) = { y ∈ var(Φ) : x < Φ y } and L Φ (x) = { y ∈ var(Φ) : y < Φ x } denote the sets of variables to the right and to the left of x in Φ, respectively. Relative to the PCNF , where Q is the quantifier prefix obtained from Q by deleting variables that do not occur in ϕ [τ ]. True and false PCNF formulas are defined in the usual way.

Dependency Schemes and LDQ(D)-Resolution
In this section, we introduce the proof system LDQ(D), which combines Q(D)-resolution [42] with long-distance Q-resolution [2]. Q-resolution is a generalization of propositional resolution to PCNF formulas [28]. Q-resolution is of practical interest due to its relation to search based QBF solvers that implement Quantified Conflict Driven Constraint Learning (QCDCL) [15,46]: the traces of QCDCL solvers correspond to Q-resolution proofs [19,21]. QCDCL-which will be described in more detail in Sect. 4-generalizes the well-known DPLL procedure [17] from SAT to QSAT. In a nutshell, DPLL searches for a satisfying assignment of an input formula by propagating unit clauses and assigning pure literals until the formula cannot be simplified any further, at which point it picks an unassigned variable and branches on the assignment of this variable. Any of the remaining variables can be chosen for assignment, but the order of assignment can have significant effects on the runtime. Modern conflict driven clause learning (CDCL) SAT solvers derived from the DPLL algorithm use sophisticated heuristics to determine what variable to assign next [34]. In QCDCL, the quantifier prefix imposes constraints on the order of variable assignments: a variable may be assigned only if it occurs in the leftmost quantifier block with unassigned variables. Often, this is more restrictive than necessary. For instance, variables from disjoint subformulas may be assigned in any order. Intuitively, a variable can be assigned as long as it does not depend on any unassigned variable. This is the intuition underlying a generalization of QCDCL implemented in the solver DepQBF [10,31]. DepQBF uses a dependency scheme [39] to compute an overapproximation of variable dependencies. Dependency schemes are mappings that associate every PCNF formula with a binary relation on its variables that refines the order of variables in the quantifier prefix. 2 The mapping which simply returns the prefix ordering of an input formula can be thought of as a baseline dependency scheme: DepQBF uses a dependency relation to determine the order in which variables can be assigned: if y is a variable and there is no unassigned variable x such that (x, y) is in the dependency relation, then y is considered ready for assignment. DepQBF also uses the dependency relation to generalize the ∀-reduction rule used in clause learning [10]. As a result of its use of dependency schemes, DepQBF generates proofs in a generalization of Q-resolution called Q(D)-resolution [42], a proof system that takes a dependency scheme D as a parameter.
Dependency schemes can be partially ordered based on their dependency relations: if the dependency relation computed by a dependency scheme D 1 is a subset of the dependency relation computed by a dependency scheme D 2 for each PCNF formula, then D 1 is more general than D 2 . The more general a dependency scheme, the more freedom DepQBF has in choosing decision variables. Currently, (aside from the trivial dependency scheme) DepQBF supports the so-called standard dependency scheme [39]. 3 We will work with the more general reflexive resolution-path dependency scheme [42], a variant of the resolution-path dependency scheme [41,44]. This dependency scheme computes an overapproximation of variable dependencies based on whether two variables are connected by a (pair of) resolution path(s).

Definition 3 (Resolution Path)
Let Φ = Q.ϕ be a PCNF formula and let X be a set of variables. A resolution path (from 1 to 2k ) via X (in Φ) is a sequence 1 , . . . , 2k of literals satisfying the following properties: If π = 1 , . . . , 2k is a resolution path in Φ via X , we say that 1 and 2k are connected in Φ (with respect to X ). For every i ∈ {1, . . . , k − 1} we say that π goes through var( 2i ).
One can think of a resolution path as a potential chain of implications: if each clause C i contains exactly two literals, then assigning 1 to 0 requires setting 2k to 1. If, in addition, there is such a path from 1 to 2k , then 1 and 2k have to be assigned opposite values. Accordingly, the resolution path dependency scheme identifies variables connected by a pair of resolution paths as potentially dependent on each other.  Definition 4 (Dependency Pair) Let Φ be a PCNF formula and x, y ∈ var(Φ). We say {x, y} is a resolution-path dependency pair of Φ with respect to X ⊆ var ∃ (Φ) if at least one of the following conditions holds: x and y, as well as ¬x and ¬y, are connected in Φ with respect to X . x and ¬y, as well as ¬x and y, are connected in Φ with respect to X .

Definition 5
The reflexive resolution-path dependency scheme is the mapping D rrs that assigns to each PCNF formula Φ = Q.ϕ the relation D rrs Both Q-resolution and Q(D)-resolution only allow for the derivation of non-tautological clauses, that is, clauses that do not contain a literal negated as well as unnegated. Longdistance Q-resolution is a variant of Q-resolution that admits tautological clauses in certain cases [2]. Variants of QCDCL that allow for learned clauses to be tautological [45,47] have been shown to generate proofs in long-distance Q-resolution [19].
In long-distance Q-resolution, when a tautological clause is created by resolution, a variable that appears in both polarities must be to the right of the pivot variable. We generalize this by requiring that the pivot be independent of a tautological variable to obtain long-distance Q(D)-resolution (LDQ(D)-resolution). The derivation rules of LDQ(D)-resolution are shown in Fig. 1. 4 Here, as in the rest of the paper, D denotes an arbitrary dependency scheme.
A derivation in a proof system consists of repeated applications of the derivation rules to derive a clause from the clauses of an input formula. Here, derivations will be represented by node-labeled directed acyclic graphs (DAGs). More specifically, we require these DAGs to have a unique sink (that is, a node without outgoing edges) and each of their nodes to have at most two incoming edges. We further assume an ordering on the in-neighbors (or parents) of every node with two incoming edges-that is, each node has a "first" and a "second" in-neighbor. Referring to such DAGs as proof DAGs, we define the following two operations to represent resolution and ∀-reduction: 1. If is a literal and P 1 and P 2 are proof DAGs with distinct sinks v 1 and v 2 , then P 1 P 2 is the proof DAG consisting of the union of P 1 and P 2 along with a new sink v that has two incoming edges, the first one from v 1 and the second one from v 2 . Moreover, if C 1 is the label of v 1 in P 1 and C 2 is the label of v 2 in P 2 , then v is labeled with the clause (C 1 \{ }) ∪ (C 2 \{ }). 2. If u is a variable and P is a proof DAG with a sink w labeled with C, then P − u denotes the proof DAG obtained from P by adding an edge from w to a new node v such that v is labeled with C\{u, ¬u}.
Definition 6 (Derivation) An LDQ(D)-resolution derivation (LDQ(D)-derivation for short) of a clause C from a PCNF formula Φ = Q.ϕ is a proof DAG P satisfying the following properties.
-Source nodes are labeled with input clauses from ϕ.
-If a node with label C has parents labeled C 1 and C 2 then C can be derived from C 1 and C 2 by (long-distance) resolution. -If a node labeled with a clause C has a single parent with label C then C can be derived from C by ∀-reduction with respect to the dependency scheme D.
We refer to these nodes as input nodes, resolution nodes, and ∀-reduction nodes, respectively.
Let P be an LDQ(D)-derivation from a PCNF formula Φ. The (clause) label of the sink node is called the conclusion of P, denoted Cl(P). If the conclusion of P is the empty clause then we refer to P as an LDQ(D)-refutation of Φ. For a node v of P, the subderivation (of P) rooted at v is the proof DAG induced by v and its ancestors in P. It is straightforward to verify that the resulting proof DAG is again an LDQ(D)-derivation from Φ. For convenience, we will identify (sub)derivations with their sinks. The size of P, denoted |P|, is the total number of literal occurrences in clause labels of P.

QCDCL with Dependency Schemes Generates LDQ(D)-Proofs
In this section, we present a version of the QCDCL algorithm that uses dependency schemes [10,31] and performs constraint learning based on long-distance Q-resolution [19,46]. 5 Generalizing an argument by Egly et al. [19], we will show that this algorithm produces LDQ(D)-proofs when using a dependency scheme D.
Starting from an input PCNF formula Φ, QCDCL generates ("learns") constraintsclauses and terms-until it produces an empty constraint, at which point it returns true (if the empty term is learned) or false (if the empty clause is learned).
One can think of QCDCL solving as proceeding in rounds. Along with a set of clauses and terms, the solver maintains an assignment σ (the trail, which we will represent by a sequence of literals in the order of their assignment). During each round, this assignment is extended by quantified Boolean constraint propagation (QBCP) and-possibly-branching.
Quantified Boolean constraint propagation (with dependency scheme D) consists in the exhaustive application of universal and existential reduction (relative to D Φ ) in combination with unit assignments. 6 More specifically, QBCP reports a clause C as falsified if C[σ ] = 1 and universal reduction can be applied to C[σ ] to obtain the empty clause. Dually, a term T is considered satisfied if T [σ ] = 0 and T [σ ] can be reduced to the empty term. A clause C is unit under σ if C[σ ] = 1 and universal reduction yields a clause C = ( ), for some existential literal such that var( ) is unassigned. Dually, a term T is unit under σ if T [σ ] = 0 and existential reduction can be applied to obtain a term T = ( ) containing a single universal literal . If C = ( ) is a unit clause, then the assignment σ has to be extended by in order not to falsify C, and if T = ( ) is a unit term, then σ has to be extended by in order not to satisfy T . If several clauses or terms are unit under σ , QBCP nondeterministically picks one and extends the assignment accordingly. This is repeated until a constraint is empty or no unit constraints remain.
If QBCP does not lead to an empty constraint, the assignment σ is extended by branching. That is, the solver chooses an unassigned variable y such that every variable x with (x, y) ∈ D Φ is assigned, and extends the assignment σ by y or ¬y.
The resulting assignment can be partitioned into so-called decision levels. The decision level of an assignment σ is the number of literals in σ that were assigned by branching. The decision level of a literal in σ is the decision level of the prefix of σ that ends with . Note that each decision level greater than 0 can be associated with a unique variable assigned by branching.
Eventually, the assignment maintained by QCDCL must falsify a clause or satisfy a term. When this happens (we call this a conflict), the solver proceeds to conflict analysis to derive a learned constraint C. Initially, C is the falsified clause (satisfied term), called the conflict clause (term). The solver finds the existential (universal) literal in C that was assigned last by QBCP, and the antecedent clause (term) R responsible for this assignment. A new constraint is derived by resolving C and R and applying universal (existential) reduction (again, relative to D Φ ). This is done repeatedly until the resulting constraint C is asserting. A clause (term) S is asserting if there is a unique existential (universal) literal ∈ S with maximum decision level (greater than zero) among literals in S, the corresponding decision variable is existential (universal), and every universal (existential) variable y ∈ var(S) such that (y, var( )) ∈ D Φ is assigned at a lower decision level (an asserting constraint becomes unit after backtracking). Once an asserting constraint has been found, it is added to the solver's set of constraints. Finally, QCDCL backtracks, undoing variable assignments until reaching a decision level computed from the learned constraint.
Pseudocode for the main QCDCL loop is shown as Algorithm 1, and pseudocode for conflict analysis is shown as Algorithm 2. We now formally state and prove a correspondence between clauses learned by QCDCL and LDQ(D)-resolution.

Proposition 2 Every clause learned by Algorithm 1 given an input PCNF Φ can be derived from Φ by LDQ(D)-resolution.
Proof We will show that each learned clause constructed during conflict analysis can be derived by LDQ(D)-resolution from input clauses or previously learned clauses. In addition, we prove an invariant saying that each such clause C can be reduced to the empty clause under the trail assignment restricted to variables up to and including the existential variable assigned last among those in C. Formally, if 1 . . . k is the trail and i = max{ j : j ∈ C, 1 ≤ j ≤ k }, then the restricted trail is 1 . . . i . If such an i does not exist-which can happen only if C contains no existential variable-the restricted trail is empty. Let τ denotes the assignment corresponding to the restricted trail. We want to show that C[τ ] simplifies to the empty clause by ∀-reduction. The proof is by induction on the number of resolution operations performed by Algorithm 2.
The base case with C being the conflict clause is trivial. For the inductive step, suppose that C can be reduced to the empty clause under the restricted trail assignment τ = 1 . . . i . Thus i ∈ C is the existential literal falsified last among literals in C and conflict analysis would resolve C with the antecedent R of i next. We have to show the resolvent satisfies the above invariant and that this resolution operation is permissible in LDQ(D)-resolution. btlevel = getBacktrackLevel(constraint) 10: return constraint, btlevel 11: end procedure Let τ = 1 . . . i−1 denote the trail at the time when i was propagated. Clause R is unit under τ , that is, R[τ ] reduces to ( i ). In particular, we have τ ( ) = 0 for every existential literal ∈ R\{ i } and every universal literal ∈ R assigned by τ . Since C[τ ] reduces to the empty clause by assumption, we further must have τ ( ) = 0 for every existential literal and every assigned universal literal of C. We conclude that τ ( ) = 0 for every existential literal and every assigned universal literal in the resolvent C = (C ∪ R)\{ i , i }. This property is clearly not affected by unassigning universal variables or unassigning existential variables not occurring in C , so C reduces to the empty clause under its corresponding restricted trail assignment, proving that the invariant is preserved. Furthermore, it entails that any literal ∈ R such that ∈ C must be universal and unassigned by τ . Since R[τ ] can be reduced to ( i ) by ∀-reduction, we must have (var( ), var( i )) / ∈ D Φ for each such literal , so C can be derived from C and R in LDQ(D)-resolution.
As in the case of QCDCL without dependency schemes [19,21] an analogue of this result can be proved for learned terms and a dual proof system ("Q-consensus") that operates on terms instead of clauses.
The proof of Proposition 2 uses the fact that two clauses C 1 ∨ u ∨ e and C 2 ∨ ¬u ∨ ¬e can be resolved on variable e even if u < e as long as (u, e) / ∈ D Φ . The following example illustrates that this generalization of the resolution rule is necessary for LDQ(D)-resolution to trace QCDCL with dependency schemes and long-distance Q-resolution.
, and ψ consists of auxiliary clauses The clauses in ψ are there simply to enforce that a and b are set to true and (in conjunction It is straightforward to check that the set of dependencies computed by the reflexive resolution-path dependency scheme is That is, the dependency scheme identifies the syntactic dependencies (x, y), (x, z 2 ), and (x, z 3 ) as spurious.
We now construct a possible trace of QCDCL on Φ with D rrs and learning based on long-distance Q-resolution. At decision level 0 the unit clauses in ψ are propagated, setting a = 1 and b = 1. This does not lead to further propagation and QCDCL proceeds with the decision y d = 0. Note that y can be assigned before x because (x, y) / ∈ D rrs Φ . This assignment does not lead to any literals being propagated, so the algorithm makes another decision z 2 d = 0. Now clause C 2 simplifies to the unit clause (z 1 ) and z 1 = 1 is propagated. Clause C 1 only contains x under the resulting assignment and we have a conflict. Conflict analysis first resolves clauses C 1 and C 2 to obtain the clause C 12 = (x ∨ y ∨ z 2 ∨ ¬a). Variable a depends on x, so ∀-reduction cannot be applied. Since z 2 is the only variable from the second decision level in clause C 12 and z 2 does not depend on x, C 12 is asserting and the clause is learned by QCDCL. Backtracking undoes the decision involving z 2 and propagates z 2 = 1 instead. As a result, C 4 simplifies to (z 0 ), unit propagation assigns z 0 = 1, and clause C 5 is falsified. Conflict analysis resolves C 4 and C 5 to derive the learned (unit) clause C 45 = (z 2 ), which causes QCDCL to backtrack to decision level 0 and propagate z 2 = 0. Now clause C 12 simplifies to (x ∨ y). Since y is independent of x we can apply ∀-reduction to obtain the unit clause (y) which propagates the assignment y = 1. Clause C 6 in turn becomes unit and propagates z 3 = 0. As a result, clause C 3 simplifies to (x) and reduces to the empty clause by ∀-reduction. Conflict analysis resolves C 3 and C 6 so as to obtain the clause ( Further resolution steps involving unit clauses yield the clause (x ∨ x), which can be reduced to the empty clause, so that QCDCL terminates with return value FALSE.

Polynomial-Time Strategy Extraction from LDQ(D)-Refutations
A PCNF formula can be associated with an evaluation game played between an existential and a universal player. These players take turns assigning quantifier blocks in the order of the prefix. The existential player wins if the matrix evaluates to 1 under the resulting variable assignment, while the universal player wins if the matrix evaluates to 0. One can show that the formula is true (false) if and only if the existential (universal) player has a winning strategy in this game, and this winning strategy is a (counter)model.
Goultiaeva et al. [24] proved that a Q-resolution refutation can be used to compute winning moves for the universal player in the evaluation game. The idea is that universal maintains a "restriction" of the refutation by the assignment constructed in the evaluation game, which is a refutation of the restricted formula.
For assignments made by the existential player, the universal player only needs to consider each instance of resolution whose pivot variable is assigned: one of the premises is not satisfied and can be used to (re)construct a refutation.
When it is universal's turn, the quantifier block for which she needs to pick an assignment is leftmost in the restricted formula. This means that ∀-reduction of these variables is blocked by any of the remaining existential variables and can only be applied to a purely universal clause. In a Q-resolution refutation, these variables must therefore be reduced at the very end, and because Q-resolution does not permit tautological clauses, only one polarity of each universal variable from the leftmost block can appear in a refutation. It follows that universal can maintain a Q-resolution refutation by assigning variables from the leftmost block in such a way as to map the associated literals to 0, effectively deleting them from the remaining Q-resolution refutation.
In this manner, the universal player can maintain a refutation until the end of the game, when all variables have been assigned. At that point, a refutation consists only of the empty clause, which means that the assignment chosen by the two players falsifies a clause of the original matrix and universal has won the game.
Egly et al. [19] observed that this argument goes through even in the case of long-distance Q-resolution, since a clause containing both u and ¬u for a universal variable u can only be derived by resolving on an existential variable to the left of u, but no such existential variable exists if u is from the leftmost block.
In this section, we will prove that this argument can be generalized to LDQ(D rrs )refutations. We illustrate this correspondence with an example: Figure 2 shows an LDQ(D rrs )-refutation of Φ. The only universal variable is u, so a strategy for the universal player in the evaluation game associated with Φ has to determine an assignment to u given an assignment to x, the only (existential) variable preceding u. The figure illustrates how to compute the assignment to u for the two possible assignments τ : {x} → {0, 1} from the restriction of the refutation by τ . In both cases, only one polarity of u occurs in the restricted refutation and therefore it is easy for universal to determine the correct assignment. Notice that in one of the cases, a generalized ∀-reduction node remains present in the restriction-this shows that we cannot limit ourselves to looking at the final reduction step in the proof when looking for the variables to assign (as is the case with ordinary Q-resolution refutations, cf. [24]).
The key property that allows universal to maintain a refutation in the above example is that universal variables from the leftmost quantifier block may appear in at most one polarity. We now show that this property is in fact sufficient for soundness of LDQ(D) when combined with a natural monotonicity property of dependency schemes.
for every PCNF formula Φ and every assignment τ to a subset of var(Φ). We say that D is simple if, for every PCNF formula Φ = ∀X Q.ϕ, every LDQ(D)-derivation P from Φ, and every universal variable u ∈ X , u or u does not appear in P. A dependency scheme D is normal if it is both monotone and simple.
As in the case of Q-resolution, universal's move for a particular quantifier block can be computed from the assignment corresponding to the previous moves and the refutation in polynomial time. Since every polynomial-time algorithm can be implemented by a family of polynomially-sized circuits, and because these circuits can even be computed in polynomial time [1, p. 109], it follows that LDQ(D) admits polynomial-time strategy extraction when D is normal (in "Appendix Appendix:", we present an explicit construction with a more specific bound on the runtime).
Theorem 1 Let D be a normal dependency scheme. There is a polynomial-time algorithm that, given a PCNF formula Φ and an LDQ(D)-refutation of Φ, computes a countermodel of Φ.
As an application of this general result, we will prove that the reflexive resolution-path dependency scheme is normal in Sect. 5.2 below.

Theorem 2 D rrs is normal.
Corollary 1 There is a polynomial-time algorithm that, given a PCNF formula Φ and an LDQ(D rrs )-refutation of Φ, computes a countermodel of Φ.
This result immediately carries over to the less general standard dependency scheme.

Corollary 2
There is a polynomial-time algorithm that, given a PCNF formula Φ and an LDQ(D std )-refutation of Φ, computes a countermodel of Φ.
In combination with Proposition 1, these results imply soundness of both proof systems.

Corollary 3
The systems LDQ(D std ) and LDQ(D rrs ) are sound.

The Reflexive Resolution-Path Dependency Scheme is Normal
In order to prove Theorem 2 and show that D rrs is normal, we will need some insight into the relationship between resolution paths and LDQ(D rrs )-derivations. For a formula Φ and a universal literal u, we will denote by T u (Φ) the set of existential literals e such that u < e and such that e is reachable from u by a resolution path via existential variables to the right of u in Φ.
Lemma 1 Let Φ = ∀X Q.ϕ be a PCNF formula and let u be a universal literal with var(u) ∈ X. Let C 1 , C 2 ∈ ϕ be clauses such that for some existential literal x, x ∈ C 1 and x ∈ C 2 , and let C = Of course, by adding clauses to a formula, we preserve all existing resolution paths, so T u (Φ) ⊆ T u (Φ ). We will prove that the opposite inclusion holds as well. Let e ∈ T u (Φ ) and let π be a resolution path in Φ certifying this. If π is also a resolution path in Φ, we are done. If it is not, it must be because it performs a C-transition, namely it contains two consecutive literals l 1 , l 2 such that var(l 1 ) = var(l 2 ), l 1 , l 2 ∈ C, but {l 1 , l 2 } C 1 and {l 1 , l 2 } C 2 . In this case, without loss of generality, we have l 1 ∈ C 1 and l 2 ∈ C 2 . Let π 1 be the prefix of π up to and including l 1 and π 2 be the suffix of π starting with l 2 . Let π be the concatenation of π 1 , x, x, and π 2 . It is clearly a valid resolution path and it uses one fewer C-transitions than π. Iterating this process, we can remove all C-transitions from π to obtain a resolution path in Φ. The resulting resolution path has the same endpoints and therefore certifies that e ∈ T u (Φ).
The previous lemma implies that when considering reachability from an outermost universal literal in a formula Φ, we can use clauses derived from Φ by LDQ(D rrs )-resolution as well. Indeed, adding clauses produced by the resolution rule does not change the set of reachable literals by Lemma 1, and adding clauses produced by universal reduction clearly does not even create new resolution paths. Particularly, if two literals ever appear together in a derived clause, there is a resolution path between them. This is summarized by the following corollary.

Corollary 4
Let P be an LDQ(D rrs )-derivation from a PCNF formula Φ = ∀X Q.ϕ and let u ∈ X, u ∈ Cl(P). Then for all existential literals e ∈ Cl(P), there is a resolution path from u to e in Φ.
As a first step towards proving Theorem 2, we will prove that both polarities of an outermost universal literal cannot appear together in a single clause of a derivation.
Proof Towards a contradiction, suppose u, ¬u ∈ Cl(P). Since input clauses do not contain both polarities of any literal, there must be a resolution step inside the derivation, which merges u and ¬u into one clause. Let P = P 1 x P 2 be such a step. Then, without loss of generality, x, u ∈ Cl(P 1 ) and ¬x, ¬u ∈ Cl(P 2 ) and by Corollary 4, there is a resolution path from u to x and from ¬u to ¬x, i.e. (u, x) ∈ D rrs Φ . However, if x depends on u, opposite polarities of u cannot be merged in a resolution step with the pivot x, a contradiction.
We will further assume that the derivation considered in the proof of Theorem 2 is in the normal form given by the following lemma. Lemma 3 Let P be an LDQ(D rrs )-derivation from a PCNF formula Φ = ∀X Q.ϕ, let u ∈ X be a universal variable such that both u and ¬u appear in P, and let Y = var ∃ (Φ). There exists an LDQ(D rrs )-derivation P from a PCNF formula Φ = ∀u∃Y.ϕ such that P contains both u and ¬u but only ∀-reduction steps with respect to one polarity of u.
Proof Let ϕ be the result of removing all universal variables except u from ϕ. Removing universal variables does not introduce new resolution paths, so D rrs Φ ⊆ D rrs Φ . The derivation P can be obtained from P in the following way. We first delete all occurrences of universal variables other than u from P, along with ∀-reduction steps involving such variables. The result is an LDQ(D rrs )-derivation from Φ , and it still contains both u and ¬u. Next, we choose a subderivation containing both u and ¬u such that none of its proper subderivations contains both literals. By Lemma 2, the conclusion C of this derivation can contain at most one of u and ¬u. If u ∈ C we omit all ∀-reduction steps involving u. Otherwise, we omit all ∀-reduction steps involving ¬u. This yields the desired LDQ(D rrs )-derivation P from Φ .
Using Lemmas 2 and 3, we can proceed to finish the proof of Theorem 2.
Proof of Theorem 2 Towards a contradiction, consider an LDQ(D rrs )-derivation from a formula Φ = ∀X Q.ϕ and let u ∈ X be such that both polarities of u occur in this derivation. Let Y = var ∃ (Φ) and let P denote the simplified derivation given by Lemma 3. Assume without loss of generality that P is a tree (any derivation can be turned into a tree-like derivation by copying proof nodes), and that P does not contain ∀-reduction steps involving ¬u. Since ¬u occurs in P but is not reduced, ¬u must occur in the conclusion of P. Thus u cannot occur in the conclusion by Lemma 2. Since u is present in the derivation P, this means there must be a reduction step on u somewhere in P. As u is the only universal variable and we omitted all reduction steps on ¬u, all reduction steps in P are on u and P must have the form depicted in Fig. 3, where P n = P n+1 − u is a lowermost reduction step on u and the subsequent resolutions are on pivots x n , . . . , x 1 . Let C 0 = Cl(P), C i = Cl(P i ), C i = Cl(P i ). The clauses C 1 , . . . , C n , C n+1 are derived by LDQ(D rrs )-resolution and by Lemma 1 we know that we can use them to show resolution-path connections as if they were input clauses. By the transformations we considered we know that starting from an arbitrary LDQ(D rrs )-derivation we can obtain a valid LDQ(D rrs )-derivation in this form, so any contradiction we derive from here means a contradiction with the assumption that an LDQ(D rrs )-derivation contains both polarities of a universal variable from the outermost block, thus proving Theorem 2. With that, we are ready to finish the proof.
We will prove that there is a resolution path from ¬u to u going through an existential literal in C n+1 , which is in contradiction with the soundness of reduction of u from C n+1 . Let us consider open resolution paths, i.e. resolution paths without their final literal. If an open resolution path ends in a literal of clause C, we say that the path leads to the clause C. By induction on n, we will prove that there is an open resolution path from ¬u which leads to the clause C n . If n = 1, we have the path ¬u, ¬x 1 , x 1 . For n > 1, let π be the open path leading to C n−1 and let be its last literal. Then either ∈ C n , in which case we have an open path leading to C n , or ∈ C n , in which case we have the open path π, ¬x n , x n leading to C n . An open path that leads to C n also leads to C n+1 , because those two clauses only differ in the presence of u and therefore can be closed by the literal u to obtain the required resolution path.

Experiments
To gauge the potential of clause learning based on LDQ(D std ), we ran experiments with the search-based solver DepQBF 7 in version 5.0. By default, DepQBF supports proof generation only in combination with the trivial dependency scheme-in that case, it generates Q-resolution or long-distance Q-resolution proofs (depending on whether long-distance resolution is enabled). However, by uncommenting a few lines in the source code, proof generation can also be enabled with the standard dependency scheme, and this option can even be combined with long-distance resolution. This leads to the solver generating Q(D std )-resolution or LDQ(D std )-resolution proofs (see Sect. 4).

Ordinary Q-resolution (Q).
These experiments were performed on a cluster with Intel Xeon E5649 processors at 2.53 GHz running 64-bit Linux. We set time and memory limits of 900 s and 4 GB, respectively. Instances were taken from two tracks of the QBF Gallery 2014: the applications track consisting of 6 instance families and a total of 735 formulas, and the QBFLib track consisting of 276 formulas.
For our first set of experiments, we disabled dynamic QBCE (Quantified Blocked Clause Elimination), a technique introduced with version 5.0 of DepQBF [32]. We further used bloqqer 9 (version 037) with default settings as a preprocessor. Since LDQ(D std ) generalizes both long-distance Q-resolution and Q(D std )-resolution, we were expecting a performance increase with LDQ(D std )-learning compared to learning based on the other proof systems. However, all four configurations showed virtually identical performance on both the application and QBFlib benchmark sets in terms of total runtime and instances solved within the time limit (see Table 1).
To get a more detailed picture, we broke down the results for the application track by instance family, limiting ourselves to instances that were solved by at least one configuration. The barplot in Fig. 4 shows that there are considerable differences in performance between solver configurations for individual instances families, with each solver configuration being outperformed by another configuration on at least one family.  Fig. 4 Average runtime in seconds (y-axis) for instances from the application track for each instance family (x-axis), by solver configuration (with preprocessing, but without dynamic QBCE). Here, we only considered instances that were solved by at least one configuration For our second set of experiments, we turned on dynamic QBCE. This led to a significant performance increase both in terms of number of instances solved within the time limit and total runtime for both benchmark sets, a result that is consistent with the findings in [32]. However, as far as the performance of LDQ(D std )-learning is concerned, the application and QBFlib tracks differed significantly for this experiment. While LDQ(D std )-learning fared worst among the configurations both with respect to instances solved and total runtime on the application track, it was the best configuration for the QBFlib track in both respects (see Table 2). Figure 5 shows that using the standard dependency scheme was beneficial both with and without long-distance resolution for the QBFlib instances.
For our final set of experiments, we left dynamic QBCE enabled but disabled preprocessing for the application track, as this was shown to lead to a performance increase in the case of learning with ordinary Q-resolution [32]. Indeed, this resulted in a performance increase   across the board (see Table 3). Moreover, LDQ(D std )-learning was the best configuration in terms of instances solved (on par with Q(D std )-resolution) as well as in terms of overall runtime. Moreover, LDQ(D std )-learning was the best configuration in terms of instances solved (on par with Q(D std )-resolution) as well as in terms of overall runtime.

Related Work
QCDCL with learning based on long-distance Q-resolution was first described by Zhang and Malik [45]. They presented an argument for the soundness of using tautological clauses (respectively, contradictory terms) within their algorithm but did not study long-distance Qresolution as a proof system. Lacking a sound theoretical foundation, the use of tautological clauses in QCDCL was abandoned in favour of more complicated methods for constraint learning that avoid their generation [20,21,33]. Interest in long-distance Q-resolution was renewed when Balabanov and Jiang [2] introduced the proof system we presented in Sect. 3 (restricted to the trivial dependency scheme) and proved its soundness. Egly et al. [19] showed that a family of formulas known to be hard for Q-resolution [28] admits short long-distance Q-resolution proofs. They also demonstrated that QCDCL with learning based on long-distance resolution generates long-distance Q-resolution proofs and presented a new version of DepQBF that implements this algorithm. Finally, they showed that a long-distance Q-resolution proof can be interpreted as a winning strategy in the evaluation game associated with a QBF, generalizing a result by Goultiaeva et al. [24]. While these results established a solid theoretical framework for the use of long-distance Q-resolution within QCDCL they did not provide an intuitive account of the semantics of individual tautological clauses. Such an account was subsequently presented by Balabanov et al. [3], who showed that tautological literals u, ¬u ∈ C can be interpreted as proxies for "phase functions" that determine whether a variable or its negation is present in clause C based on the values assigned to pivot variables appearing in the derivation of C. The authors used this interpretation to generalize the linear-time strategy extraction algorithm of Balabanov and Jiang [2] to long-distance Q-resolution proofs.
Recently and independently of this work, Beyersdorff and Blinkhorn investigated the soundness of Q-resolution proof systems parameterized by dependency schemes [6]. They define a property of dependency schemes D-full exhibition-which ensures that a certain version of long-distance Q(D)-resolution is sound, and show that the reflexive resolution-path dependency scheme has that property.
In a nutshell, a dependency scheme D is fully exhibited if every true QBF Φ has a model { f e } e∈var ∃ (Φ) such that f e may only depend on a universal variable u if (u, e) ∈ D Φ (such models have elsewhere been referred to as D-models [40]). It is fairly straightforward to show that Q(D)-resolution is sound if D has this property, but generalizing this result to proof systems with long-distance resolution presents a challenge. Beyersdorff and Blinkhorn show that full exhibition is sufficient for soundness of a restricted version of LDQ(D)-resolution, where complementary universal literals that are "merged" by resolution must be annotated with the (existential) pivot variable, and universal reduction can be applied only if every existential variable occurring in the premise or the annotation of a universal variable is independent of the universal variable to be reduced. However, it is uncertain whether proofs generated by DepQBF with LDQ(D)-learning satisfy this additional restriction.
How full exhibition relates to our normality property is not entirely clear. Beyersdorff and Blinkhorn prove that full exhibition is not sufficient for soundness of LDQ(D)-resolution as defined here. In combination with Theorem 1, this shows that dependency schemes that are fully exhibited need not be normal. Whether there are normal dependency schemes that are not fully exhibited, on the other hand, remains open. Indeed, there is some evidence to the effect that normality entails full exhibition: consider a dependency scheme D that is not fully exhibited, and let Φ = ∀uQ.ϕ be a true QBF that does not have a D-model. Suppose u is the only universal variable of Φ. In this restricted case, the (non-)existence of a D-model can be expressed as a QBF Ψ by simply shifting existentials independent of u to the left. Because Φ does not have a D-model, Ψ must be false and admit a Q-resolution refutation P, which is also an LDQ(D)-refutation of Φ. Because Φ is true, LDQ(D)-resolution must be unsound and so D cannot be normal by Theorem 1. Obviously, the assumption that u is the only universal variable of Φ is very restrictive, but since we can suppose that D is monotone (recall that a dependency scheme is normal if it is both simple and monotone), there is hope that the argument for an arbitrary QBF can be reduced to this case by instantiating with a suitable variable assignment.

Discussion
The results of Sects. 4 and 5 establish a partial soundness proof of QCDCL with learning based on LDQ(D std ): we now know that we can trust such a solver when it outputs "false". To prove that "true" answers can be trusted as well, one has to show soundness of quantified term resolution (Q-consensus) when combined with the standard dependency scheme and long-distance resolution. The reason this does not follow from the results proved here is that they rely on a correspondence of Q-resolution derivations with dependency-inducing resolution paths that is not immediate for terms generated from an input PCNF: there is a correspondence of Q-consensus derivations with dual "resolution paths" that connect such terms, but these "resolution paths" do not induce resolution-path dependencies in the input PCNF.
The experiments in Sect. 6 indicate that we should not expect significant performance gains when switching from learning with Q(D std )-resolution to LDQ(D std ). This is in spite of the fact that, from a purely theoretical perspective, LDQ(D std ) is a stronger proof system: a well-studied class of QBFs introduced by Kleine Büning, Karpinski, and Flögel requires exponentially-sized Q-resolution proofs [28] but admits short long-distance Q-resolution refutations [19], and since the standard dependency scheme does not offer any improvement over trivial dependencies on these formulas (see [12]) we obtain an exponential separation of LDQ(D std )-resolution from Q(D std )-resolution. From a practical point of view, the main benefit of using LDQ(D std )-resolution over Q(D std )-resolution is that conflict analysis is much simpler (cf. [19]). A learned constraint can be obtained from a conflict simply by resolving variables in the reverse order of their propagation (see Sect. 4). Methods that avoid the generation of tautological clauses (contradictory terms) during learning are significantly more involved [20,21,33].
We have shown that LDQ(D rrs )-refutations allow for polynomial-time strategy extraction. In practice, the corresponding algorithm generates circuits that are frequently larger by an order of magnitude than the refutations provided as input. It is unclear whether this increase in size can be avoided by careful engineering alone or only by using a different approach. Faster (linear time) strategy extraction algorithms are known for "ordinary" Q-resolution and longdistance Q-resolution [2,3]. Unfortunately, their underlying idea of setting universal variables so as to falsify the premise of some ∀-reduction step no longer works when dependency schemes enter the mix: generalized ∀-reduction may remove a universal variable u even in the presence (in the premise) of an existential variable e such that u < e and the universal player can only be sure to falsify the premise if the e-literal is false, but she does not know the value of e at the time of assigning u. We believe that developing linear-time strategy extraction algorithms for Q(D)-resolution or LDQ(D)-resolution is going to require a better understanding of the power of these proof systems vis-à-vis Q-resolution and long-distance Q-resolution [12].
Acknowledgements Open access funding provided by Austrian Science Fund (FWF). We would like to thank Florian Lonsing for helpful discussions and for pointing out how to configure DepQBF so that it generates LDQ(D std ) proofs. This research was partially supported by Austrian Science Fund (FWF) Grants P27721 and W1255-N23.
Open Access This article is distributed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate if changes were made.

Appendix: Proof of Theorem 1
We begin by formally defining the "restriction" of an LDQ(D)-derivation by an assignment, which is a straightforward generalization of this operation for Q-resolution derivations [24]. 10 The result of restricting a derivation is either a derivation or the object , which can be interpreted as representing the tautological clause containing every literal. Accordingly, we stipulate that ∈ for every literal .
Definition 8 (Restriction) Let Φ be a PCNF formula and let P be an LDQ(D)-derivation from Φ. Further, let X ⊆ var(Φ) and let τ : X → {0, 1} be a truth assignment. The restriction of P by τ , in symbols P[τ ], is defined as follows. 3. If P = P − u, that is, if P is a ∀-reduction node, we distinguish three cases: If D is a monotone dependency scheme, LDQ(D)-refutations are preserved under restriction by an existential assignment (cf. [24,Lemma 4]). This is stated in the following lemma, which can by proved by a straightforward induction on the structure of the LDQ(D)-derivation.  Above, we argued that the universal player can use an LDQ(D)-refutation for a normal dependency scheme D in order to compute winning moves in the evaluation game associated with a PCNF formula and that this can be used to compute a countermodel of the formula in polynomial time. We now prove this directly, by showing how to construct a circuit implementing a countermodel from an LDQ(D)-refutation.
We begin by describing auxiliary circuits simulating the restriction operation. Let Φ = Q 1 X 1 . . . Q k X k .ϕ be a PCNF formula and let P be a refutation of Φ. For each quantifier block X i , each subderivation S of P, and each literal , we will construct circuits top i S and contains i S, with inputs from X = j<i X j such that, for every assignment σ : X → {0, 1}, We first describe our construction and then prove that it satisfies the above properties in Lemma 5. Let S be an input node. We let and define top i S for 1 < i ≤ k as Moreover, for 1 ≤ i ≤ k we define contains i S, as For non-input nodes, we proceed as follows.
and if S = S − u, we let For the contains i S, circuit, we distinguish two cases. Let be a literal and S a derivation. If / ∈ Cl(S) we simply let Otherwise, if ∈ Cl(S), we have to consider two cases. First, if S = S 1 q S 2 , we let To implement the winning strategy for universal sketched above, we further construct circuits polarity S,u for each node S of P and each universal variable u ∈ var ∀ (Φ), such that, for each assignment τ : L Φ (u) → {0, 1}, Let u ∈ X i be a universal variable from the ith quantifier block. If S is an input node, we simply define polarity S,u := contains i S,u , and if S = S − u is a ∀-reduction node, we let polarity S,u := polarity S ,u .
Proof Let X = X 1 ∪ · · · ∪ X i−1 . As (1) and (2) are related, we will prove them first. We will use induction on the structure of P, with the induction hypothesis that (1) and (2) hold. The inductive step will be carried out in two phases. In the first phase, we prove that (1) holds and in the second phase we use this additional information to prove that (2) holds as well.  (1) and (2) hold for P by induction hypothesis, these properties must hold for P as well.
Let us now turn to the proof of (3). These auxiliary circuits can be efficiently constructed in a top-down manner, from the input nodes to the conclusion. By a careful analysis, we obtain the following:

Lemma 6
There is an algorithm that, given a PCNF formula Φ and an LDQ(D)-derivation P from Φ, computes the circuits polarity P,u for every universal variable u in time O(|P|·n), where n = |var(Φ)|.
Proof The algorithm first sorts clauses according to a fixed order of literals. Let k be the number of quantifier blocks in the prefix of Φ. There is at most one circuit top i P for each node S of P and each 1 ≤ i ≤ k. Similarly, there is at most one circuit contains i S, for each node S of P, each 1 ≤ i ≤ k, and each literal ∈ Cl(S).
Once top i S has been computed for each 1 ≤ i ≤ k, the circuits contains i S, can easily be constructed for each 1 ≤ i ≤ k and every literal ∈ Cl(S). Overall, this can be done in time

O(|Cl(S)| · k) ≤ O(|Cl(S)| · n).
Assume that the circuits contains i S, are stored in lists following the order of literals in Cl(S). Then for each node S, the circuits top i S and contains i S, associated with S can again be computed in time O(|Cl(S)| · n), so that overall, these circuits can be computed in time O(|P| · n) for all nodes of P. Having computed the circuits contains and top, the circuits polarity S,u can be computed for each node S and each universal variable u ∈ var ∀ (Φ) in time O(|P| · n).
Using Lemma 4, we can spell out the argument sketched at the beginning of this section and prove that for normal dependency schemes D, the universal player can maintain an LDQ(D)-refutation throughout the evaluation game by successively restricting an initial LDQ(D)-refutation by both players' moves and assigning universal variables from the leftmost remaining block X so as to falsify the (unique) literals from X remaining in the refutation. Lemma 5 tells us that the polarity circuits can be used to implement this strategy. In order to put things together, we will need the following two lemmas, which tell us that successive restriction and bulk restriction in fact yield the same result. With that, we are ready to prove the final statement.

Lemma 9
Let D be a normal dependency scheme, let P be an LDQ(D)-refutation of a PCNF formula Φ. Then the family { f u } u∈var ∀ (Φ) of functions f u = ¬polarity P,u is a countermodel of Φ.
Proof Let Φ = Q 1 X 1 . . . Q k X k .ϕ and let τ : var(Φ) → {0, 1} be a truth assignment such that τ (u) = f u τ | L Φ (u) for each universal variable u. Let X <i = i−1 j=1 X j , and let τ i = τ | X <i for each 1 ≤ i ≤ k + 1. We claim that P[τ i ] is an LDQ(D)-refutation of Φ[τ i ] for 1 ≤ i ≤ k + 1. The assignment τ 1 is empty so P[τ 1 ] = P and Φ[τ 1 ] = Φ so the statement holds in that case. Suppose the claim holds for i such that 1 ≤ i ≤ k. If Q i = ∃, then Theorem 1 follows immediately from Lemmas 6 and 9. In fact, we obtain the following result.
Theorem 3 Let D be a normal dependency scheme. There is an algorithm that computes a countermodel of a PCNF formula Φ with n variables from an LDQ(D)-refutation P of Φ in time O(|P| · n).