International Workshopon
Quantiﬁed Boolean Formulas 20131
Informal Workshop Report2
Florian Lonsing, Martina Seidl
florian.lonsing@tuwien.ac.at, martina.seidl@jku.at
July 10, 2013

1

This work was partially funded by the Vienna Science and Technology Fund(WWTF) under grant ICT10-018 and by the Austrian Science Fund under grants
S11408-N23 and S11409-N23.
2
The copyright of all contributions remains with the authors.

LL

Preface
After a break of more than one decade, the International Workshop on Quantiﬁed Boolean Formulas 2013 (QBF 2013), collocated with the 16th International
Conference on Theory and Applications of Satisﬁability Testing (SAT 2013), is
the ﬁrst event dedicated to research on quantiﬁed Boolean formulas (QBF).
Recently, there has been a lot of progress in QBF research on a variety of
topics ranging from solving, to preprocessing, to certiﬁcations, and to encodings. All of these results were presented at many diﬀerent scientiﬁc events.
The purpose of the QBF workshop is to provide a dedicated forum for QBF
researchers and users to meet, share ideas, and discuss the status quo. Almost
40 registered participants clearly state the general interest in an event like the
QBF Workshop 2013.
During the workshop seven presentations will be given based on the peerreviewed extended abstracts collected in this informal report, which is available
from the workshop’s website:
http://fmv.jku.at/qbf2013/
Due to the informal nature of the QBF Workshop, the authors of accepted
papers are free to submit their work to other scientiﬁc events or journals without
any restrictions.
The topics of the contributions are manifold, ranging from theoretical results to practical encodings. At this point we would like to highlight that allcontributions contain novel content, to a certain extent, which has not been presented in this form before. Moreover, certain contributions share insights which
are entirely new and have never been published before. This is particularly remarkable because in the call for contributions we put emphasis on works which
trigger interesting discussions during the workshop. Novelty was not a strict requirement. Therefore, we would like to thank the contributors for their papers
as well as the program committee members and reviewers for their support andtheir high quality feedback.

LLLAs preparation for the QBF Workshop, we organized the QBF Gallery 2013
which is a non-competitive evaluation of state-of-the-art tools. Like the QBF
Workshop, the QBF Gallery is aﬃliated to the SAT conference 2013. Details
are available at the event’s website:
http://www.kr.tuwien.ac.at/events/qbfgallery2013/
Results will be presented during the QBF Workshop and at the SAT conference.
We hope that with the seven accepted presentations and with the report on the
QBF Gallery, the QBF Workshop will oﬀer an interesting meeting for the QBF
research community.

Florian Lonsing and Martina Seidl, Wien/Linz, July 2013

LY

5
Program Committee• Fahiem Bacchus, University of Toronto, Canada• Armin Biere, University of Linz, Austria• Nikolaj Björner, Microsoft Research, USA• Uwe Bubeck, University of Paderborn, Germany• Hans Kleine Büning, University of Paderborn, Germany• Hubie Chen, Universidad del Paı́s Vasco and Ikerbasque, Spain• Nadia Creignou, Université de la Méditerranée Aix-Marseille, France• Uwe Egly, Vienna University of Technology, Austria• Allen Van Gelder, University of California at Santa Cruz, USA• Enrico Giunchiglia, Università di Genova, Italy• Mikoláš Janota, INESC-ID Lisboa, Portugal• Massimo Narizzano, Università di Genova, Italy• Stefan Szeider, Vienna University of Technology, AustriaYYLContents
1 Martin Kronegger, Andreas Pfandler and Reinhard Pichler:
1
Conformant Planning as a Benchmark for QBF-Solvers
2 Uwe Egly and Magdalena Widl: Solution extraction from long6
distance resolution proofs
3 Mikoláš Janota and Joao Marques-Silva: ∀-Exp+Res Does not
17
P-Simulate Q-resolution
4 Friedrich Slivovsky and Stefan Szeider: Variable Dependencies
23
and Q-Resolution
5 William Klieber, Mikolas Janota, Joao Marques-Silva and Edmund Clarke: Extending DPLL-Based QBF Solvers to Handle
30
Free Variables
6 Allen Van Gelder: Certiﬁcate Extraction from Variable Elimi35
nation QBF Preprocessors
7 Charles Jordan and Lukasz Kaiser: Benchmarks from Reduc40
tion Findingvii

Conformant Planning as a Benchmark for
QBF-Solvers
Martin Kronegger, Andreas Pfandler, and Reinhard Pichler
Vienna University of Technology, Austria{kronegger, pfandler, pichler}@dbai.tuwien.ac.at

1

Introduction

Planning has a long history as an important ﬁeld of artiﬁcial intelligence. The
task of domain-independent planning is to ﬁnd a sequence of actions (called aplan) to achieve a desired goal, given some initial state.
Concerning the computational complexity, even the most basic case, i. e.,
STRIPS-like planning (also called classical planning), is NP-complete whenrestricted to plans with length polynomial in the input. To cope with this highcomplexity, powerful heuristics such as Fast Forward [9] and Fast Downward [7]have been developed. In addition, also exact methods have been proposed. For
instance, a planner called SATPLAN [11] reduces a classical planning problem to
SAT. Another promising SAT-based approach is the planner Mp by Rintanen [18].
In practice one often has to deal with uncertainty, i. e., incomplete knowledge. Thus, it is of high importance to study this form of planning (also called
conformant planning). Here we consider the case of deterministic actions withincomplete knowledge. Baral et al. [2] have shown that the complexity raises toΣ2 P-completeness for this form of planning. Following the successful history of
SAT in the area of classical planning it is a natural step to encode conformant
planning problems as quantiﬁed Boolean formulas (QBFs). Several encodings
have been proposed in the literature, such as the encodings by Rintanen [17].
In this paper we present a framework for transforming conformant planninginstances to QBFs in order to analyze how well QBF-solvers can handle planningproblems. Since the planning instances are given in a non-ground modelling
language several reﬁnements are necessary to obtain QBFs of reasonable size.
A key feature of our approach is that we aim at optimal plans, i. e., plans ofminimum length. The goal of this work is to gather some experience with thisapproach and highlight desiderata that could improve the performance andapplicability of QBF-solvers in the area of planning.
Our main contributions are as follows: (1) We have implemented a prototype
of our framework that encodes planning instances given in a fragment of thewidely used planning domain deﬁnition language (PDDL) with uncertainty inthe initial state as QBFs. (2) We introduce a new kind of benchmarks that has astrong focus on uncertainty and hence gives challenging new instances. (3) Basedon these instances we perform a detailed experimental evaluation – comparing
specialized planning tools with the performance of several QBF-solvers whenapplied to QBFs generated by our framework.
This research was supported by the Austrian Science Fund (FWF): P25518-N23.

2

SolverWe consider planning instances given in PDDL restricted to the STRIPS-subset
and extended by uncertainty in the initial state. Our framework (depicted in
Figure 1) is capable of computing the minimal plan length of planning instances.
After parsing the input, the grounding algorithm analyzes the given planninginstance and calculates a lower bound  on the plan length. Starting with a plan
length of , the grounder then grounds only “important” parts of the instances.
The QBF-encoder takes the ground representation as input, transforms it to aquantiﬁed Boolean formula (QBF) that is satisﬁable if and only if the planningproblem has a plan of length . Then, the QBF-encoder invokes an external
QBF-solver. In case the generated QBF is satisﬁable, our framework extracts
the plan (with optimal length) from the assignment of the leftmost ∃-block. If
the QBF is unsatisﬁable,  is incremented, additional “important” parts of the
problem may need grounding, and the subsequent QBF is passed to the solver.
The grounding step is the bottleneck of the approach, since the planning instances
are given in a non-ground modelling language and a naive implementation cancause an exponential blow-up in the number of variables. Clearly, a smaller
grounding directly yields smaller QBFs. Therefore, we use information from thespeciﬁcation to guide the grounding process and apply techniques for computing
lower bounds to avoid the generation of unnecessary QBFs.
The QBF-encoder essentially employs the ∃∀∃-encoding for conformant planning by Rintanen [17] using explanatory framing axioms. The resulting QBF
expresses “there exists a sequence of actions from the initial state to a goalstate such that for all unknown variables in the initial state there exist a truth
assignment for the remaining variables”. During the generation of the formula,the encoder also applies mild forms of preprocessing such as unit-propagation and(in some cases) labeling of sub-formulas. By using these simple enhancements andthe reﬁnements for grounding, we are able to drastically reduce the size of thegenerated QBFs by a factor of approximately 17 in the new type of benchmark
which we introduce in Section 3.

3

Evaluation

We have evaluated a prototype of our framework. Below, we show how the runtime
behavior depends on the used QBF-solver and compare it with other planning
tools (T0 [14, 20], ConformantFF [8, 4]). To allow for a better comparison, we
have created a new type of benchmark that focuses on uncertainty in the initialstate. Due to space limitations, we only report on this new benchmark type.
dyn. grounding

PDDL
instance

Yes
ParserGrounderQBF-Encoder

QBF-Solver
No

Fig. 1. Architecture of our solver.



Plan

The new benchmark we introduce is called “Dungeon”. In this setting a player
wants to defeat monsters living in a dungeon. Each monster requires diﬀerent
items to be defeated. In the beginning, the player picks at most one item fromeach pool of items. In addition, the player can exchange several items for one
more powerful item if he holds all necessary “ingredients”. Eventually, the player
enters the dungeon. When entering the dungeon, the player is forced to pick
additional items. The dilemma is that the player does not know which items hewill get, i. e., the additional items are unknown. The goal is to pick items suchthat irrespective of the additional items he defeats at least one monster.
We have run our tests on a server with two Intel Xeon E5345 processors,
48GB RAM, and openSUSE 11.4. We ran the single threaded solvers with a
15 minutes timeout and a memory limit of 16GB. The upper bound for theplan length of our solver was set to 200. We used AQME [15, 1], DepQBF [12,5], QuBE[6, 16] and sKizzo [3, 19] in conjunction with our solver. For a better
comparison we also evaluated ConformantFF and T0 on the same instances. If a
QBF-solver supported the generation of certiﬁcates or returning an assignmentof the leftmost ∃-block (currently, from the considered solvers only sKizzo and
DepQBF), we enabled this option and included the additional amount of timeneeded in the runtime measurement.
Our results indicate that randomly generated “Dungeon” instances are hardfor both, specialized planning tools and QBF-solvers. Considering only the numberof solved instances, T0 is the winner with 102 out of 144 solved instances. The
other solvers were able to solve the following amount of instances: 96 (AQME), 81(QuBE), 80 (DepQBF), 76 (sKizzo), 64 (ConformantFF). It turned out that thestrength of our framework (with diﬀerent QBF-solvers) is that it sometimes ﬁnds
considerably shorter plans than heuristics do. Compared to T0 our solver founda shorter plan in 33 instances and compared to ConformantFF in 15 instances.
In Figure 2 we depict the minimum plan lengths obtained for an instance by a
QBF-solver/planning tool. Table 1 shows the performance of the diﬀerent solvers
on selected interesting cases of the “Dungeon”-instances using the abbreviation“unsol” for “unsolvable”, “to” for “timeout” and “ex250” for “exit code 250”.
Due to space limitations, we mention only a few observations made in ourevaluation. In the benchmark results we see that AQME explicitly shows that
there is no plan of length at most 200, while other solvers run into a timeout.
Unfortunately, AQME does not return certiﬁcates nor assignments, which makes
it inapplicable in practice, as no plans can be extracted. Clearly, building aportfolio solver that returns certiﬁcates is a special challenge, since all solvers in
the portfolio should handle certiﬁcates in a uniform way. Interestingly, AQME
performs quite well compared to current state-of-the-art tools. Furthermore, it
seems that a large number of monsters inﬂuences the performance of the planning
tools much more than the QBF-based approach. In contrast, a large numberof unknowns seems to be more critical for the QBF-approach. Finally, consider
an instance that has an optimal solution with plan length . It is interesting to
see that the runtime of the QBF-solvers increases quite dramatically with theplan length, but drops on satisﬁable formulas with plan length . Due to theincremental generation of QBFs for each plan length an incremental QBF-solver(see, e. g., [13]) could give a notable performance boost.



AQME
ConfFF
DepQBFQuBE
sKizzoT0plan length

20

10

0

0

20

40

60
80
instance number

100

120

140

Fig. 2. An overview of all solutions found by the considered solvers.
AQME
ConfFF DepQBF
QuBE
sKizzoT0# #i #m #u t/pl cl/vars t/pl t/pl cl/vars t/pl cl/vars t/pl cl/vars t/pl
30 10
5 10 603.53 111887 0.04
to 27478 to 9031
to 11826 0.43>200 41377 unsol ≥49 10271 ≥16 3473 ≥21 4503 unsol?
40 10 20 4 2.24 1733 437.39 0.25 1733 0.29 1733 0.32 1733 0.09
3
648
8
3
648
3
648
3
648
5
72 15 75 10 428.26 7195
to1.06 7195 0.92 7195
5398 565.85
42093
4 2093 4 2093 ex250 1651
4
111 25 50 3 41.31 63922
toto 35374 to 42511
49648 0.62
97321
≥5 4329 ≥6 5077 ex250 5825
16
143 30 150 5 690.02 133543
toto 65899 to 82810
48988
to
8
10616
≥4 5756 ≥5 6971 ex250 4541
Table 1. Detailed results for some interesting instances showing the instance number(#), the number of: items (#i), monsters (#m), unknown variables (#u), clauses (cl),variables (vars), the time in seconds (t) and the plan length (pl).

4Conclusion

In this work we have presented a framework for transforming planning instanceswith uncertainty in the initial state to QBFs. Big collections of conformant
planning instances that ﬁt the input language of our framework (i. e., including
the plethora of instances provided by the International Planning Competition [10]),thus become accessible as interesting, hard benchmarks for QBF-solvers.
Our experiments have revealed that on some instances the QBF-approach
outperforms conventional planning tools. Still, we see several interesting points tobe addressed by the QBF-community in order to make the QBF-based approach
yet more eﬃcient and beneﬁcial. Returning assignments is necessary to be able
to extract the actual plan. Obtaining full certiﬁcates is desirable as it also allows
to verify the solution. Furthermore, as for each plan length a new QBF has to begenerated, incremental QBF-solvers could give especially in this setting a drastic
boost in performance. Since the QBF-solvers need most time on QBF-instances
for plan lengths that are close to a solution, also QBF-solvers biased towards
unsatisﬁability could be a promising approach. Clearly any progress made in theworld of QBF-solvers will directly carry over to our approach for planning.
We see further experiments as well as creating solver-speciﬁc QBF transformations as the most important tasks. Also developing additional hard benchmarktypes and improving the dynamic grounder remains future work.

References
1. Website of AQME. http://www.mind-lab.it/aqme/, [accessed: April 25, 2013]
2. Baral, C., Kreinovich, V., Trejo, R.: Computational complexity of planning andapproximate planning in the presence of incompleteness. Artiﬁcial Intelligence
122(1-2), 241–267 (2000)
3. Benedetti, M.: Evaluating QBFs via symbolic skolemization. In: Proc. LPAR. pp.
285–300 (2004)
4. Website of ConformantFF. http://fai.cs.uni-saarland.de/hoffmann/cff.html,[accessed: April 25, 2013]
5. Website of DepQBF. http://fmv.jku.at/depqbf/, [accessed: April 25, 2013]
6. Giunchiglia, E., Marin, P., Narizzano, M.: QuBE7.0, system description. Journal of
Satisﬁability. 7(8), 83–88 (2010)
7. Helmert, M.: The fast downward planning system. Journal of Artiﬁcial Intelligence
Research (JAIR) 26, 191–246 (2006)
8. Hoﬀmann, J., Brafman, R.I.: Conformant planning via heuristic forward search: A
new approach. Artiﬁcial Intelligence 170(6-7), 507–541 (2006)
9. Hoﬀmann, J., Nebel, B.: The FF planning system: Fast plan generation throughheuristic search. Journal of Artiﬁcial Intelligence Research (JAIR) 14, 253–302(2001)
10. International conference on automated planning and scheduling (ICAPS). http://ipc.icaps-conference.org, [accessed: April 25, 2013]
11. Kautz, H., Selman, B., Hoﬀmann, J.: SATPlan: Planning as satisﬁability. In:
Abstract booklet of the 5th International Planning Competition, event in thecontext of ICAPS 2006 (2006)
12. Lonsing, F., Biere, A.: Integrating dependency schemes in search-based QBF solvers.
In: Proc. SAT. pp. 158–171 (2010)
13. Marin, P., Miller, C., Lewis, M.D.T., Becker, B.: Veriﬁcation of partial designs
using incremental QBF solving. In: Proc. DATE. pp. 623–628 (2012)
14. Palacios, H., Geﬀner, H.: Compiling uncertainty away in conformant planningproblems with bounded width. Journal of Artiﬁcial Intelligence Research (JAIR)
35, 623–675 (2009)15. Pulina, L., Tacchella, A.: A self-adaptive multi-engine solver for quantiﬁed Boolean
formulas. Constraints 14(1), 80–116 (2009)
16. Website of QuBE. http://www.star-lab.it/~qube/, [accessed: April 25, 2013]
17. Rintanen, J.: Asymptotically optimal encodings of conformant planning in QBF.
In: Proc. AAAI. pp. 1045–1050 (2007)
18. Rintanen, J.: Madagascar: Eﬃcient planning with SAT. In: The 2011 International
Planning Competition – Description of Participating Planners – Deterministic
Track. pp. 61–64 (2011)
19. Website of sKizzo. http://skizzo.info, [accessed: April 25, 2013]
20. Website of T0. http://ldc.usb.ve/~hlp/, [accessed: April 25, 2013]

Solution extraction
from long-distance resolution proofs 
Uwe Egly and Magdalena Widl
Institute of Information Systems, Vienna University of Technology, Austria{uwe,widl}@kr.tuwien.ac.at

1

Introduction

Much effort has been devoted in the past decade to the development of decision procedures for quantiﬁed Boolean formulas (QBFs) in order to improve their performance.
Besides solving the decision problem of whether a closed QBF is true and returning
yes or no, modern QBF solvers can produce clause or cube proofs to certify their answer. These proofs can be used to derive solutions to problems formulated as QBFs.
For instance, if the QBF describes a synthesis problem, the solution to this problem
can be generated from the proof. Examples for representations of such solutions arecontrol circuits (manifested in Herbrand or Skolem functions) or control strategies. We
review two approaches for solution generation below. We focus on false QBFs and clause
Q-refutations. For true QBFs, both approaches work in a symmetric fashion.
Balabanov and Jiang [1] propose to extract a Herbrand function for each universal(∀) variable from a Q-refutation of a false QBF. These functions are constructed in sucha way that replacing each ∀ variable by its Herbrand function in the matrix and removing
the preﬁx yields an unsatisﬁable Boolean formula. Unsatisﬁability can be checked by acommon SAT solver if required. Their algorithm traverses the refutation and constructs
a formula for each ∀ variable from the nodes of the refutation where the variable isreduced by universal reduction. The run-time of their extraction algorithm is polynomialin the size of the refutation.
Goultiaeva et al. [3] employ a game-theoretic view to QBFs. They present an algorithm which executes a winning strategy for the universal player from the refutation. The
existential (∃) player chooses a move, i.e., an assignment of truth values to all ∃ variablesin the outermost quantiﬁer block. The algorithm modiﬁes the Q-refutation according tothis move and removes the current quantiﬁer block from the preﬁx. From the resulting
refutation, the ∀ player computes her move, i.e., an assignment of truth values to all∀ variables in the outermost quantiﬁer block which is now universal. Modiﬁcations
take place as above and the ∃ player continues. The run-time of this algorithm is also
polynomial in the size of the refutation.
For both methods, their runtime is directly related to the refutation size. It is therefore
desirable to have short refutations. Since there are families of QBFs (like the one from
Kleine Büning et al. [4] discussed below), for which any Q-refutation is exponential,
This work was supported by the Austrian Science Foundation (FWF) under grant S11409-N23
and by the Vienna Science and Technology Fund (WWTF) through project ICT10-018.

the use of more powerful calculi to allow more succinct refutations is essential for fast
extraction of Herbrand functions or strategies.
A way to strengthen the Q-resolution calculus is to add the additional inference
rules presented in [1]. The resulting calculus is called long-distance resolution (LDQresolution) [9]. Its inference rules are reproduced in Appendix A as rules r1 to r4
and u1 . LDQ-resolution allows to resolve two clauses upon an ∃ pivot p resulting ina resolvent with complementary pairs of ∀ literals provided each pair’s variable has ahigher quantiﬁer level than p. The derived clause is thus tautological.
This paper is intended to advertise the use of LDQ-resolution. First, LDQ-resolution
may greatly simplify the clause learning component [2,6] in current QBF solvers. In
this component, additional effort (in terms of Q-resolution steps) is required in order
to avoid the generation of tautological clauses over ∀ literals. This additional effort
often results in an increase of refutation size. Second, we show that LDQ-resolution has
the potential to produce shorter refutations. More precisely, we show an exponential
speed-up in refutation size compared to Q-resolution using the family (ϕt )t≥1 of false
QBFs introduced by Kleine Büning et al. in [4]. Third, we show that the strategy
extraction algorithm in [3] can handle LDQ-refutations. Therefore, the performance of
this algorithm directly beneﬁts from exponentially shorter LDQ-refutations. Finally, we
point out open questions with respect to the certiﬁcate extraction procedure in [1].

2

Short proofs for hard formulas

Let (ϕt )t≥1 be a family of QBFs in PCNF. The formula ϕt has preﬁx∃d0 d1 e1 ∀x1 ∃d2 e2 ∀x2 ∃d3 e3 · · · ∀xt−1 ∃dt et ∀xt ∃f1 · · · ft
and the following clauses in the matrix:
d0
K0
K2j
dj ∨ xj ∨ dj+1 ∨ ej+1
dt ∨ x t ∨ f1 ∨ · · · ∨ ft
K2t
B2j−1 xj ∨ fj

K1
d0 ∨ d1 ∨ e 1
K2j+1 ej ∨ xj ∨ dj+1 ∨ ej+1
K2t+1 et ∨ xt ∨ f1 ∨ · · · ∨ ft
B2j
xj ∨ fj

j = 1, . . . , t − 1
j = 1, . . . , t

Kleine Büning et al. prove in [4, Theorem 3.2] that any Q-refutation for ϕt is exponential
in t. Van Gelder [8] shows that there exists a short Q-resolution refutation for formulasof this class if resolution over universal variables is allowed. We show that ϕt has
polynomial size LDQ-refutations. They have the form of a directed acyclic graph (DAG).
Following the notation in [1], we will use x∗ as a shorthand for x ∨ x.
t−1
t−1
1. Derive dt ∨ xt ∨ i=1 fi from B2t and K2t . Derive et ∨ xt ∨ i=1 fi similarly.
2. Use both clauses from Step 1 together with K2(t−1) and derive the clause dt−1 ∨t−1
xt−1 ∨ i=1 fi ∨ x∗t . Observe that the quantiﬁcation level of dt and et is less thant−2
the level of xt . Use B2(t−1) to get dt−1 ∨ xt−1 ∨ i=1 fi ∨ x∗t . Derive the clauset−2
et−1 ∨ xt−1 ∨ i=1 fi ∨ x∗t in a similar way.
1t
3. Iterate the procedure to derive d2 ∨ x2 ∨ i=1 fi ∨ i=3 x∗i as well as e2 ∨ x2 ∨1
t∗
i=1 fi ∨i=3 xi .

tt
4. With K2 , derive d1 ∨ x1 ∨ f1 ∨ i=2 x∗i . Use B2 to obtain d1 ∨ x1 ∨ i=2 x∗i . Derivet
e1 ∨ x1 ∨ i=2 x∗i in a similar fashion.
t
5. Use the two derived clauses together with K0 and K1 to obtain i=1 x∗i , which canbe reduced to 2.
The number of clauses in this refutation is in O(t).
We have identiﬁed formulas which have short LDQ-refutations, but any Q-refutationof the same formula is exponential. Hence the processing of the short refutations byextraction algorithms can be much faster provided the algorithms can handle such a
refutation without too much additional complication.

3

Strategy extraction from long-distance resolution

We show that the strategy extraction method from Q-refutations presented by Goultiaeva
et al. in [3] can be applied in the same manner to LDQ-refutations.
As sketched in the introduction, the method is described as a game between a ∀player and an ∃ player. The game proceeds through the quantiﬁer preﬁx from the left
to the right alternating the two players according to the quantiﬁer blocks. The ∃ player
arbitrarily chooses an assignment to the variables in the current block. The assignment
for the ∀ player is then computed according to previous assignments as follows.
First, all leaf nodes of the refutation, the clauses of the input formula, are modiﬁed
according to the existential assignment as deﬁned below similarly to [3,7].
Deﬁnition 1. A (partial) assignment to a set V of variables of a QBF in PCNF is a set σof literals of V such that if l ∈ σ then l ∈ σ. A clause K under an assignment σ is denotedKσ and deﬁned as follows: Kσ =  if K ∩σ = ∅ and Kσ = K \{q | q ∈ K ∧q ∈ σ}otherwise.
Second, the inner nodes and 2 are derived by applying LDQ-resolution rules or, incases where the pivot element has been removed by the assignment, by applying additional sound derivation rules (P-rules) presented by Goultiaeva et al. [3] and reproducedin Appendix A. Then the refutation, now containing rules outside the LDQ-resolution
calculus, is transformed back into an LDQ-refutation. This transformation results in each∀ variable of the next quantiﬁer block to be reduced at most once. At the ∀ player’s turn,the assignment to each of these variables is determined by either choosing the opposite
polarity of the variable’s literal removed in the remaining universal reduction or any
polarity in case the variable is not reduced at all. It is shown in [3] that for a Q-refutation,
after each restriction of either the ∃ or the ∀ player, 2 is derived.
We show that this method also works for LDQ-refutations. First, we show in a
fashion similar to [3,7] that in a refutation applying LDQ-rules and P-rules, each node
generated from the restricted leaves subsumes the restriction of the node by the partial
assignment. The proof of the following lemma can be found in Appendix A.
Lemma 1. (cf. Lemma 2.6 in [7]) Given a QBF in PCNF ψ = ∃V Pφ with V the set of
all variables of the outermost quantiﬁer block, P the preﬁx of ψ without ∃V , and φ thematrix of ψ, let K, K l and K r be clauses of φ, and σ an assignment to V . Then it holdslrthat res(Kσ, Kσ, p) ⊆ res(K l , K r , p)σ and red(Kσ , x) ⊆ red(K, x)σ .

Using this lemma, we show with an argument similar to Goultiaeva et al. [3], that (1)by applying the restriction rules with respect to an assignment to the variables of an ∃quantiﬁer block to an LDQ-refutation, the resulting proof derives 2, and (2) that further
restricting the LDQ-refutation by the computed assignment to the ∀ variables of the next
turn also derives 2. (More details can be found in Appendix A.)
The key reason why this works for LDQ-refutations in the same fashion as for
Q-refutations is the following. In a restricted refutation, the applications of rules deriving
tautologies of some ∀ variables (LD-steps, r2 to r4 in Appendix A) are always removedby the partial assignment to ∃ variables of the previous quantiﬁer blocks. This is the casebecause an LD-step can result in a tautology x ∨ x of some ∀ variable x only if the pivot
element p (an ∃ variable) has a lower quantiﬁer level than x. Thus before the ∀ player’sturn, the pivot element of each LD-step that results in tautologies involving ∀ variablesof the respective quantiﬁer block is contained in the partial assignment. Therefore, eitherof the parents of the LD-step is set to , and by applying the corresponding derivation
rule, only one polarity of the ∀ variable is left in the derived clause.

4

Conclusion and future work

We have shown an exponential speed-up in refutation size if LDQ-resolution insteadof Q-resolution is employed to any QBF ϕt belonging to the family introduced in [4].
Given the fact that state of the art methods for the extraction of Herbrand functions or
strategies require traversing the refutation, it is desirable to retrieve LDQ-refutations
instead of Q-refutations from QBF solvers in order to speed up such extraction methods.
We have further shown that strategies can be retrieved from LDQ-refutations by applying
the state of the art algorithm described in [3]. This implies an exponential speed-up forthe strategy extraction from any QBF in the family (ϕt )t≥1 .
It remains an open question how Herbrand functions can be extracted efﬁciently from
LDQ-refutations. It is possible to build Boolean formulas from truth tables generated
by the strategy extraction method in [3]. However, since each possible assignment to
the existential variables has to be considered, this naive method is exponential in thequantiﬁer preﬁx.
Further, to the best of our knowledge, a workﬂow including output and veriﬁationof LDQ-resolution proofs is currently not supported by state of the art QBF solvers.
(According to Van Gelder [8], QuBE-cert produces tautological clauses, but it is unclear
whether the LDQ calculus is used.) In QBF solvers based on clause learning such as
DepQBF [5], the generation of tautological clauses is avoided by additional resolution
steps which remove existential variables with a higher quantiﬁer level in order to enablea separate universal reduction for each problematic universal variable. By allowing long
distance resolution steps, the learning component could be simpliﬁed and the obtained
refutations could be shorter.

References
1. V. Balabanov and J.-H. R. Jiang. Uniﬁed QBF certiﬁcation and its applications. Formal
Methods in System Design, 41(1):45–65, Apr. 2012.

2. E. Giunchiglia, M. Narizzano, and A. Tacchella. Clause/Term Resolution and Learning in the
Evaluation of Quantiﬁed Boolean Formulas. Journal of Artiﬁcial Intelligence Research (JAIR),
26:371–416, Sept. 2006.
3. A. Goultiaeva, A. Van Gelder, and F. Bacchus. A uniform approach for generating proofs andstrategies for both true and false QBF formulas. In International joint conference on Artiﬁcial
Intelligence (IJCAI), IJCAI’11, pages 546–553. AAAI Press, 2011.
4. H. Kleine Büning, M. Karpinski, and A. Flögel. Resolution for Quantiﬁed Boolean Formulas.
Information and Computation, 117(1):12–18, Feb. 1995.
5. F. Lonsing and A. Biere. DepQBF: A Dependency-Aware QBF Solver (System Description).
Journal on Satisﬁability, Boolean Modeling and Computation (JSAT), 7:71–76, 2010.
6. F. Lonsing, U. Egly, and A. Van Gelder. Efﬁcient clause learning for quantiﬁed boolean
formulas via QBF pseudo unit propagation. In Theory and Application of Satisﬁability Testing(SAT), 2013.
7. A. Van Gelder. Input Distance and Lower Bounds for Propositional Resolution Proof Length.
In Theory and Application of Satisﬁability Testing (SAT), 2005.
8. A. Van Gelder. Contributions to the Theory of Practical Quantiﬁed Boolean Formula Solving.
In M. Milano, editor, Principles and Practice of Constraint Programming (CP), Lecture Notes
in Computer Science, pages 647–663. Springer Berlin Heidelberg, 2012.
9. L. Zhang and S. Malik. Towards a Symmetric Treatment of Satisfaction and Conﬂicts in
Quantiﬁed Boolean Formula Evaluation. In P. Hentenryck, editor, Principles and Practice ofConstraint Programming (CP), volume 2470 of Lecture Notes in Computer Science, pages
200–215. Springer Berlin Heidelberg, 2006.



A

Strategy extraction from LDQ-resolution proofs

We write e for an existential variable, x (with or without subscript) for a universal
variable, x∗ for x ∨ x, var(q  ) for the variable of a literal q  ∈ {q, q}, lev(q  ) for thequantiﬁer level of the variable var(q  ) counting from the left to the right of the preﬁx,
K l , K r , and K for leaf clauses or derived clauses, p for the existential pivot variable,
and 2 for the empty clause. By QBF we refer to a QBF in PCNF. An LDQ-refutation is
an LDQ-resolution derivation of 2.
The following reproduces the rules of the LDQ-resolution calculus (LDQ-rules)
presented by Balabanov and Jiang [1] with the differences that universal reduction is
not integrated in the resolution rules but represented by a separate rule and that only one
universal literal is reduced in one step.
[p]

Kl ∨ pKr ∨ pKl ∨ Kr

(r1 )

[p]

Kl ∨ p ∨ x
Kr ∨ p ∨ x
K l ∨ K r ∨ x∗lev(p) < lev(x)

(r2 )

[p]

Kl ∨ p ∨ x
K r ∨ p ∨ x∗
K l ∨ K r ∨ x∗lev(p) < lev(x)

(r3 )

[p]

K l ∨ p ∨ x∗
K r ∨ p ∨ x∗
K l ∨ K r ∨ x∗lev(p) < lev(x)(r4 )for x ∈ {x, x, x∗ } andfor all e ∈ K it holds that lev(e) < lev(x )(u1 )[x] K ∨ xK

As in [1], we extend universal reduction to delete also x∗ and call x∗ the merged
variable in r2 , r3 , r4 , because x, x occur in both parent clauses, but they are merged into
one occurrence of x∗ in the resolvent. We require the restriction on the quantiﬁer levelin these rules to also apply to other merged variables in K l and K r . In r1 , K l and K r
may contain x, x or x∗ but no merging is allowed.
We deﬁne a (partial) assignment and a clause under a (partial) assignment similarly
to [3,7]:Deﬁnition 1. A (partial) assignment to a set V of variables of a QBF in PCNF is a set σof literals of V such that if l ∈ σ then l ∈ σ. A clause K under an assignment σ is denotedKσ and deﬁned as follows: Kσ =  if K ∩σ = ∅ and Kσ = K \{q | q ∈ K ∧q ∈ σ}otherwise.
The algorithms play and restrict describe the algorithm presented by Goultiaeva et al. [3]. play implements the alternating turns of the universal (∀) and theexistential (∃) player moving from the left to the right in the quantiﬁer preﬁx. Each
player chooses an assignment to the variables in the current quantiﬁer block. The proof
is modiﬁed after each assignment and results in an LDQ-refutation of the QBF underthe partial assignment. The ∃ player chooses an arbitrary assignment and the ∀ playerchooses an assignment that depends on the current modiﬁed proof.
The modiﬁcation of the LDQ-resolution consists of two steps represented by the procedures restrict and transform. First, restrict restricts the proof according
to the chosen assignment. It modiﬁes the leaves of the proof by applying the assignment
according to Deﬁnition 1 and then modiﬁes the successor nodes by either applying one of
the LDQ-resolution rules described above or, if the pivot variable has been removed fromat least one of the parents, by applying one of the additional rules presented in [3,7]. The
additional rules (P-rules) are reproduced in the following (symmetric rules are omitted):Kl ∨ pKl ∨ pKr
p ∈ K r
[p]
r
K
Kl
Kr
[p]
p, p ∈ K l and p, p ∈ K r
narrower(K l ,K r )x ∈ K
[x] K
K
[x] 

[p]

(r5 )
(r6 )
(r7 )
(u2 )
(u3 )

where narrower(K l , K r ) returns the clause containing less literals. If K l and K r containthe same number of literals, K l is returned. Observe that 2 is the narrowest clause and contains all literals.
Note that, even though each P-rule represents a sound derivation step, applying
P-rules results in a proof outside the LDQ-calculus. Starting at the leaves of the proof,
the function transform (Π p ), where Π p is a proof containing clauses derived using
LDQ-rules and P-rules, removes parts of the proof that have become redundant due tothe application of P-rules. Thereby also all applications of P-rules are removed. Morespeciﬁcally, for node K =  derived by rule r5 , its parent K l ∨ p is removed with all its
ancestors, and K is merged with its other parent . A similar procedure is applied tonodes derived by rules r6 and r7 . Each node derived by rules u1 to u3 is merged with its
parent. When 2 is derived, the procedure stops and all nodes that are not ancestors of 2
are removed. -clauses are eliminated by eventually applying rule r6 or by removing
nodes when 2 is found. The resulting refutation is an LDQ-refutation.
After restricting the LDQ-refutation by a computed assignment σ∀ to ∀ variables,
only one redundant clause, namely 2, has to be removed because after the previous
restriction by σ∃ and the following repair, the refutation contains at most one universal
reduction for any universal variable x of the current quantiﬁer block. This is the casebecause the condition for x to be reduced from any clause K is that K does not containany ∃ variables with a quantiﬁer level higher than x. Any ∃ variable in K is thereforein σ∃ , and after restricting the refutation, K is either (1) set to  or (2) all ∃ variables
are removed. The topologically ﬁrst clause (furthest to 2) where (2) happens derives 2
after reducing each of its ∀ variables. An assignment σ∀ to a ∀ variable x as computedin Line 8 of Algorithm 1 chooses the opposite polarity of x when it is reduced in node
K. This way, according to Deﬁnition 1, K becomes 2 and only the 2 derived from K
has to be removed.

In the following we present a proof that restrict, when called in Line 4 or Line
9 of play, returns a derivation of 2 using LDQ-rules and P-rules. Proposition 1 showsthat this holds for an arbitrary assignment to all ∃ variables in the outermost quantiﬁer
block, and Proposition 2 shows the same for the computed assignment to ∀ variables.
We write res(K l ,K r ,p) for a resolution step over pivot element p according to rules r1
to r7 , and red(K,x) for a reduction step reducing variable x according to rules u1 to u3 .
We start by showing that any node generated by applying an LDQ-rule or a P-rulefrom the restricted leaves subsumes the restriction of the node by the partial assignment.
Lemma 1. (cf. Lemma 2.6 in [7]) Given a QBF in PCNF ψ = ∃V Pφ with V the set of
all variables of the outermost quantiﬁer block, P the preﬁx of ψ without ∃V , and φ thematrix of ψ, let K, K l and K r be clauses of φ, and σ an assignment to V . Then it holdslrthat res(Kσ, Kσ, p) ⊆ res(K l , K r , p)σ and red(Kσ , x) ⊆ red(K, x)σ .
Proof. We distinguish between each case of K containing or not containing literals of σ.
C0 (σ, K): ∃q ∈ σ such that q ∈ K ∧ q ∈ K. This case never happens because notautologies over ∃ variables are allowed.
C1 (σ, K): ∀q ∈ σ it holds that q ∈ K and q ∈ K. Then Kσ = K.
C2 (σ, K): ∃q ∈ σ such that q ∈ K. Then Kσ = .
C3 (σ, K): ∀q ∈ σ it holds that q ∈ K and ∃q ∈ σ such that q ∈ K. Then Kσ =K \ {q | q ∈ σ}.
For resolution steps, either of the following cases applies (symmetric cases are omitted):lr(1) C1 (σ, K l ) and C1 (σ, K r ): Kσ= K l , Kσ= K r , and res(K l , K r , p)σ =
l
r
l
r
, Kσ
, p) =
res(K , K , p). By applying rule r1 , r2 , r3 , or r4 , we obtain res(Kσlrres(K , K , p). Therefore the subset relation holds.
lr(2) C2 (σ, K l ) and C1 (σ, K r ): Kσ= , Kσ= K r , and res(K l , K r , p)σ = . Bylr
applying rule r5 , we obtain res(Kσ, Kσ, p) = . Therefore the subset relation holds.
lr(3) C3 (σ, K ) and C1 (σ, K ): Since C1 (σ, K r ), ∀q ∈ σ it holds that p = q and p = q.
lrThen Kσ= K l \ {q | q ∈ σ}, Kσ= K r , and res(K l , K r , p)σ = K l ∪ K r \ {q | q ∈
l
r
, Kσ
, p) = K l ∪K r {q | q ∈ σ}.
σ}. By applying rule r1 , r2 , r3 , or r4 , we obtain res(KσTherefore the subset relation holds.
lr(4) C2 (σ, K l ) and C2 (σ, K r ): Kσ= , Kσ= , and res(K l , K r , p)σ = . Bylr
applying rule r5 , we obtain res(Kσ, Kσ, p) = . Therefore the subset relation holds.
lrlr(5) C2 (σ, K ) and C3 (σ, K ): Then Kσ = , and Kσ= K r \ {q | q ∈ σ}. We haveto distinguish two cases:(a) ∃q ∈ σ such that var(q) = p. Then res(K l , K r , p)σ = (K l ∪ K r ) \ {q | q ∈ σ}.
l
r
, Kσ
, p) = K r \ {q | q ∈ σ}. Therefore theBy applying rule r6 , we obtain res(Kσsubset relation holds.
(b) Otherwise (σ does not contain the pivot p). Then res(K l , K r , p)σ = . By applyinglrrule r5 , we obtain res(Kσ, Kσ, p) = . Therefore the subset relation holds.
lrlr(6) C3 (σ, K ) and C3 (σ, K ) Kσ= K l \ {q | q ∈ σ}, Kσ= K r \ {q | q ∈ σ}, andlrlrres(K , K , p)σ = K ∪ K \ {q | q ∈ σ}. By applying rule r1 , r2 , r3 , or r4 , we obtainlrres(Kσ, Kσ, p) = K l ∪ K r \ {q | q ∈ σ}. Therefore the subset relation holds.

For reduction steps, either of the following cases applies:(7) C1 (σ, K): Kσ = K and red(K, x)σ = red(K, x). Therefore the subset relation
holds.
(8) C2 (σ, K): Kσ =  and red(K, x)σ = . By applying rule u3 we obtainred(Kσ , x) = . Therefore the subset relation holds.
(9) C3 (σ, K): Kσ = K \ {q | q ∈ σ} and red(K, x)σ = (K \ {x}) \ {q | q ∈ σ}.
By applying rule u1 , we obtain red(Kσ , x) = (K \ {x}) \ {q | q ∈ σ}. Therefore thesubset relation holds.
With respect to the application of rules r2 to r4 (LD-steps), we observe the following
from the play algorithm and cases (1) to (6) in the above lemma: play iterates overthe quantiﬁer preﬁx from the left to the right. The condition for a clause to be derived by
an LD-step is that the quantiﬁer level of the pivot variable p is lower than the level ofthe merging variable x∗ . If the algorithm is executing the existential quantiﬁer level ,
any of the cases (1) to (6) except (5a), i.e. all cases where the pivot remains unassigned,
can only happen on an LD-step if lev(x∗ ) −  > 1. That is, var(x) is not in the next
quantiﬁer block. Otherwise (if x∗ is on the next quantiﬁer level) p must be assigned in
the current turn and case (5a) applies. Case (5a), where p is assigned, can happen on any
LD-step. In this case, the LD-step is modiﬁed by rule r6 , which removes the merged
variable. It is thus always the case that after restricting the refutation according to an
existential quantiﬁer block on the -th level, the refutation does not contain any LD-step
generating a variable x∗ with lev(x∗ ) =  + 1. Therefore, in the following ∀ player’sturn, none of the respective ∀ variables occurs as tautology.
Lemma 2. Given a QBF in PCNF ψ = ∃V Pφ with V the set of all variables of theoutermost quantiﬁer block, P the preﬁx of ψ without ∃V , and φ the matrix of ψ, an
LDQ-resolution Π deriving a clause K from ψ, and an assignment σ∃ to V , it holds
that Π  = restrict(Π, σ∃ ) derives a clause K  from Pφσ∃ such that K  ⊆ Kσ∃ .
Proof. By induction on the structure of Π using Lemma 1.

Proposition 1. Given a QBF in PCNF ψ = ∃V Pφ with V the set of all variables ofthe outermost quantiﬁer block, P the preﬁx of ψ without ∃V , and φ the matrix of ψ,an LDQ-resolution Π deriving 2 from ψ, and an assignment σ∃ to V , it holds that
Π p = restrict(Π, σ∃ ) derives 2 from Pφσ∃ .
Proof. By Lemma 2, for any clause K derived in Π it holds that Π  derives a clause K such that K  ⊆ Kσ∃ . Therefore, if K = 2, then Π  must derive a clause K  = 2. 
Proposition 2. Given a QBF in PCNF ψ = ∀V Pφ with V the set of all variables ofthe outermost quantiﬁer block, P the preﬁx of ψ without ∀V , and φ the matrix of ψ, an
LDQ-resolution Π deriving 2 from ψ, and an assignment σ∀ to V as computed in Line
8 of Algorithm 1, Π p = restrict(Π, σ∀ ) derives 2 from Pφσ∀ .
Proof. For any q ∈ σ∀ it holds that q is either not reduced at all, or reduced exactly oncein Π. If q is not reduced at all, then it is not involved in Π and therefore its assignment
does not alter the proof. Let R ⊆ σ∀ be the set of dual literals that are reduced exactly
once in the proof. Then there is a set K with |K| = |R| of nodes such that the nodes

in K are directly following one another, each reducing exactly one literal r in R. The
last reduced node of K results in 2. This is the case because all literals of R are in theoutermost quantiﬁer block. restrict (Π,σ∀ ) then applies rule u2 to each clause K,
setting each K in K to 2.
Algorithm 1: play
Input : QBF P.ψ, LDQ-refutation Π
1 foreach Quantiﬁer block Q in P from left to right do
2
if Q is existential then3σ∃ ← any assignment to variables in Q4
Π p ← restrict (Π,σ∃ )(Π p is not an LDQ-resolution)p5Π ← transform (Π )(Π is an LDQ-resolution)
6
7
8
9
10

else Q is universal
K ← topologically ﬁrst node with no existential literalsσ∀ ← {x | x ∈ K ∧ var(x) ∈ Q} ∪ {x | x ∈ K ∧ x ∈ K ∧ var(x) ∈ Q}
Π p ← restrict (Π,σ∀ )Π ← transform (Π p )11

Algorithm 2: restrict
Input : LDQ-refutation Π, assignment σ for variables in outermost block
Output: Restricted refutation containing LD-rules and P-rules
1 foreach leaf node K in Π do2
K ← Kσ ;foreach inner node K topologically in Π do
if K is a resolution node then5
K l ,K r ← parents of K
6p ← pivot of K
7
K ← res(K l ,K r ,p)
3
4

8
9
10
11

else K is a reduction nodeK c ← parent of Kx ← variable reduced from K c
K ← red(K c ,p)12
13

return Π∀Exp+Res Does not P-Simulate Q-resolution
Mikoláš Janota1 and Joao Marques-Silva1,21
2

1

IST/INESC-ID, Lisbon, Portugal
University College Dublin, Ireland

Introduction

In our recent work [9], we formalized a proof system ∀Exp+Res underlying expansion–
based QBF solvers, namely sKizzo [1], RAReQS [8], and to some extend Quantor [2].
In the same work, we conjectured that ∀Exp+Res and Q-resolution [4] cannot psimulate one another. In this work we conﬁrm one half of this conjecture, i.e. that
∀Exp+Res cannot p-simulate Q-resolution. This observation furthers our understanding of the differences between the different underlying methods for solving QBFs aswell as the differences between the underlying proof systems.

2

Preliminaries

A literal is a Boolean variable or its negation. For a literal l, we write ¯l to denote theliteral complementary to l, i.e. x̄ = ¬x, ¬x = x. A clause is a disjunction of ﬁnitely
many literals. A formula in conjunctive normal form (CNF) is a conjunction of ﬁnitely
many clauses. As usual, whenever convenient, a clause is treated as a set of literals anda CNF formula as a set of sets of literals.
For a literal l = x or l = x̄, we write var(l) for x. Analogously, for a clause C,
var(C) denotes {var(l) | l ∈ C} and for a CNF ψ, var(ψ) denotes {l | l ∈ var(C), C ∈ ψ}.
Substitutions are denoted as x1 /ψ1 , . . . , xn /ψn , with xi = xj for i = j. The set ofvariables x1 , . . . , xn is called the domain of the substitution. An application of a substitution is denoted as φ[x1 /ψ1 , . . . , xn /ψn ] meaning that variables xi are simultaneously
substituted with corresponding formulas ψi in φ. A substitution is called an assignment
iff each ψi is one of the constants 0, 1. An assignment is called total, or complete, for aset of variables X if each x ∈ X is in the domain of the assignment. For substitutions
τ1 = x1 /ψ1 , . . . , xn /ψn and τ2 = y1 /ξ1 , . . . , ym /ξm with distinct domains we writeτ1 ∪ τ2 for the substitution x1 /ψ1 , . . . , xn /ψn , y1 /ξ1 , . . . , ym /ξm .
Quantiﬁed Boolean Formulas (QBFs) [3] are an extension of propositional logic
with quantiﬁers with the standard semantics that ∀x. Ψ is satisﬁed by the same truth
assignments as Ψ [x/0] ∧ Ψ [x/1] and ∃x. Ψ as Ψ [x/0] ∨ Ψ [x/1]. Unless speciﬁed otherwise, QBFs are in closed prenex form with a CNF matrix, i.e. Q1 X1 . . . Qk Xk . φ,where Xi are pairwise disjoint sets of variables; Qi ∈ {∃, ∀} and Qi = Qi+1 . The formula φ is in CNF and is deﬁned only on variables X1 ∪ . . . ∪ Xk . The propositional partφ is called the matrix and the rest the preﬁx. We write QCNF to talk about formulas inthis form. If a variable x is in the set Xi , we say that x is at level i and write lv(x) = i;we write lv(l) for lv(var(l)). A closed QBF is false (resp. true), iff it is semanticallyequivalent to the constant 0 (resp. 1).

If a variable is universally quantiﬁed, we say that the variable is universal. For aliteral l and a universal variable x such that var(l) = x, we say that l is universal. The
notions of existential variable and literal are deﬁned analogously.
2.1

Q-resolution

Q-resolution [4] is an extension of propositional resolution for showing that a QCNF is
false. For a clause C, a universal literal l ∈ C is blocked by an existential literal k ∈ C
iff lv(l) < lv(k). ∀-reduction is the operation of removing from a clause C all universal
literals that are not blocked by some existential literal. For two ∀-reduced clauses x∨C1
and x̄ ∨ C2 , where x is an existential variable, a Q-resolvent [4] is obtained in two steps.
(1) Compute Cu = C1 ∪ C2  {x, x̄}. If Cu contains complementary literals, the Qresolvent is undeﬁned. (2) Compute Cr by ∀-reducing Cu ; Cr is called the resolvent of
C1 and C2 . For a QCNF P .φ, a Q-resolution proof of a clause C is a ﬁnite sequenceof clauses C1 , . . . , Cn where Cn = C and any Ci in the sequence is part of the given
matrix φ or it is a Q-resolvent for some pair of the preceding clauses. A Q-resolution
proof is called a refutation iff C is the empty clause, denoted by ⊥.
In this paper Q-resolution proofs are treated as connected directed C ∨ x C ∨ x̄1
2
acyclic graphs, i.e. each clause in the proof corresponds to somenode labeled with that clause. We assume that the input clauses are
Cualready ∀-reduced. Q-resolution steps are depicted as on the right.
Note that the ∀-reduction step is depicted separately.
C
2.2

Proof complexity

A proof system P is a relation P (Φ, π) computable in polynomial time such that aformula Φ is true iff there exists a proof π for which P (Φ, π). A proof system P1 psimulates a proof system P2 iff any proof in P2 of a formula Φ can be translated into a
proof in P1 of Φ in polynomial time (c.f. [5,10]).
We count the sizes of Q-resolution proofs as the number of resolution steps plus thenumber of ∀-reductions where each reduced literal is counted separately.
2.3

Expansions

Based on the equivalence ∀y.Φ = Φ[y/0] ∧ Φ[y/1], expansion of universal quantiﬁers
enables decreasing the number of quantiﬁers and maintaining prenex normal form at
the cost of introducing fresh variables. Once all universal variables are expanded, a
SAT solver can be invoked. Partial expansions enable us to mitigate the size of theformula. For instance, for the formula ∀y∃x. (y ∨ x) ∧ (y ∨ x̄) it is sufﬁcient to consider
an expansion with y/0 to show the formula false.
For a general QBF Φ = ∀ U 1 ∃ E 2 . . . ∀ U 2N −1 ∃ E 2N . φ (WLOG we start with auniversal quantiﬁer) our recent work [9] deﬁnes an expansion as follows.
Deﬁnition 1 (∀-expansion tree). A ∀-expansion tree is a rooted tree T such that eachτN
τ1path p0 →p1 . . . →pN in T from the root node p0 to some leaf node pN has exτiactly N edges and each edge pi−1 −→pi is labeled with a total assignment τi to thevariables U 2i−1 , for i ∈ 1..N . Each path in T is uniquely determined by its labeling.

uN ∨ c2NēN ∨ c2N −1

DN −2 ∨ uN ∨ c̄2N −1

DN −2 ∨ ūN ∨ c̄2N

DN −2 ∨ ēN ∨ uN
DN −2 ∨ ēNūN ∨ c2N −1

DN −2 ∨ c̄2N −1 ∨ c̄2NeN ∨ c2N

DN −2 ∨ eN ∨ ūN
DN −2

DN −2 ∨ eN

Fig. 1. Q-resolution proof sketch (where DN −2 = c̄1 ∨ · · · ∨ c̄2N −3 ∨ c̄2N −2 )Deﬁnition 2 (∀-expansion). Let T be a ∀-expansion tree. For a root-to-leaf path P in
T and a clause C, the following rules deﬁne the ∀-expansion of C by P , ∀-expansionof φ by P , and ∀-expansion of Φ by T . These expansions are denoted as E (P, C),
E (P, ψ), and E (T , Φ), respectively.
1. For each path Pk in T from the root, labeled by assignments τ1 , . . . , τk , and an
existential variable x with lv(x) = 2k deﬁne a fresh variable xτ1 ,...,τk .
2. For each path P in T from the root to some leaf labeled by τ1 , . . . , τN , and a clauseC ∈ φ deﬁne E (P, C) as C[τ1 ∪ . . . τN ∪ τR ] whereτR = {x/xτ1 ,...,τk | 1 ≤ k ≤ N, x an existential variable s.t. lv(x) = 2k}
3. For each path P in T from the root to some leaf deﬁne E (P, φ) as a union ofE (P, C) for C ∈ φ.
4. Deﬁne E (T , Φ) as the union of all E (P, φ) for each root-to-leaf path P in T .
Deﬁnition 3. A proof in ∀Exp+Res of a formula Φ is a pair (T , π) where π is a resolution proof of E (T , Φ).

3

Separation

For a natural number N , construct the following formula3 .
∃e 1 ∀u1 ∃c1 c2 . . . ∃eN ∀uN ∃c2N −1 c2N .
i∈1..N (ēi ∨ c2i−1 ) ∧ (ūi ∨ c2i−1 ) ∧ (ei ∨ c2i ) ∧ (ui ∨ c2i )∧i∈1..2N c̄i(1)

The formula has a Q-resolution
proof comprising linear number of resolution steps.
Starting from the clause i∈1..2N c̄i , the literals c̄i are gradually resolved away from thehighest to the lowest level. Figure 1 shows how the variables c2N −1 , c2N are resolved
away. The other pairs of variables are resolved away in the same fashion resulting in
the empty clause in the end.
Now we show that any ∀Exp+Res proof of the formula is exponential. Let us lookat the expansion of the ﬁrst universal variable, i.e. the variable u1 . We observe that both3

See http://sat.inesc-id.pt/~mikolas/qbfw13 for a generator.

of the values are needed in the expansion. Let us expand u1 , yielding the two following
formulas, one for u1 /1 and one for u1 /0 (for now other variables are left unexpanded).
∃e2 ∀u2 ∃c3 c4 . . . ∃eN ∀uN ∃c2N −1 c2N .
u /1
u /1
u /1
(ē1 ∨ c1 1 ) ∧ (c1 1 ) ∧ (e1 ∨ c2 1 )∧i∈2..N (ēi ∨ c2i−1 ) ∧ (ūi ∨ c2i−1 ) ∧ (ei ∨ c2i ) ∧ (ui ∨ c2i )∧

u /1
u /1
c̄1 1 ∨ c̄2 1 ∨ i∈3..2N c̄i(2)∃e2 ∀u2 ∃c3 c4 . . . ∃eN ∀uN ∃c2N −1 c2N .
u /0
u /0
u /0
(ē1 ∨ c1 1 ) ∧ (c2 1 ) ∧ (e1 ∨ c2 1 )∧i∈2..N (ēi ∨ c2i−1 ) ∧ (ūi ∨ c2i−1 ) ∧ (ei ∨ c2i ) ∧ (ui ∨ c2i )∧

u1 /0
u /0
c̄1
∨ c̄2 1 ∨ i∈3..2N c̄i

(3)

u /1

The formula (2) is satisﬁable because e1 can be set to 1, c2 1 to 0 and the rest of
the existential variables to 1 and similarly for the formula (3). Since both formulas (2)and (3) are satisﬁable, both of them are needed to show unsatisﬁability.
Regardless of how the rest of variables in (2) and (3) are expanded, the only variable they share is e1 because universal variables are expanded away and all existential
variables are labeled with u1 /1 and u1 /0, respectively.
From Craig’s interpolation theorem [6,7], there is an interpolant I using only variables common to (2) and (3), i.e. e1 , and it holds that (2) ⇒ I and (3) ⇒ ¬I. Due tothe structure of the formulas, I must be e1 . Equivalently (2) ∧ ē1 and (3) ∧ e1 are false(unsatisﬁable). The formula (2) ∧ ē1 is equivalent to the following.
u /1

u /1

(c1 1 ) ∧ (c2 1 )∧∃e2 ∀u2 ∃c3 c4 . . . ∃eN ∀uN ∃c2N −1 c2N .
i∈2..N (ēi ∨ c2N −1 ) ∧ (ūi ∨ c2N −1 ) ∧ (ei ∨ c2N ) ∧ (ui ∨ c2N )∧i∈3..2N c̄i
u /1

u /1

Since c1 1 , c2 1 appear in only the ﬁrst part of the formula, the second part of
the formula has to be false (i.e. unsatisﬁable after full expansion). The second part of
the formula is in the same form as the initial formula just with three less variables.
Repeating the same arguments, this formula has to be fully expanded. Following thesame argument for (3) ∧ e0 shows that the proof needs to expand each variable in bothpolarities at all depths. Thus yielding an exponential expansion of the given formula.

4

Conclusion and Future Work

This paper investigates a recently-made conjecture [9] that states that Q-resolution [4]and expansion-based solving (∀Exp+Res) are incomparable proof systems. We investigated half of the conjecture, namely that ∀Exp+Res does not p-simulate Q-resolution.
This observation further complements the result of [9], where it was shown that ∀Exp+Res
can p-simulate tree Q-resolution. The result shown here conﬁrms that this p-simulation
result is “tight”, i.e. non-tree Q-resolution cannot be simulated. To show that that Qresolution cannot simulate ∀Exp+Res is the subject of future work.

References
1. Benedetti, M.: Evaluating QBFs via symbolic Skolemization. In: Baader, F., Voronkov, A.
(eds.) LPAR. pp. 285–300 (2004)
2. Biere, A.: Resolve and expand. In: SAT (2004)
3. Büning, H.K., Bubeck, U.: Theory of quantiﬁed Boolean formulas. In: Handbook of Satisﬁability. IOS Press (2009)
4. Büning, H.K., Karpinski, M., Flögel, A.: Resolution for quantiﬁed Boolean formulas. Inf.
Comput. 117(1) (1995)
5. Cook, S.A., Reckhow, R.A.: The relative efﬁciency of propositional proof systems. J. Symb.
Log. 44(1), 36–50 (1979)
6. Craig, W.: Linear reasoning. a new form of the Herbrand-Gentzen theorem. J. Symb. Log.
22(3), 250–268 (1957)
7. Harrison, J.: Handbook of Practical Logic and Automated Reasoning. Cambridge University
Press (2009)
8. Janota, M., Klieber, W., Marques-Silva, J., Clarke, E.M.: Solving QBF with counterexample
guided reﬁnement. In: Cimatti, A., Sebastiani, R. (eds.) SAT. Lecture Notes in Computer
Science, vol. 7317, pp. 114–128. Springer (2012)
9. Janota, M., Marques-Silva, J.: On propositional QBF expansions and Q-resolution. In: SAT(2013), a preprint available at http://sat.inesc-id.pt/~mikolas/.
10. Urquhart, A.: The complexity of propositional proofs. Bulletin of the EATCS 64 (1998)

Variable Dependencies and Q-Resolution
Friedrich Slivovsky and Stefan Szeider
Institute of Information Systems, Vienna University of Technology, Vienna, Austria
fs@kr.tuwien.ac.at,stefan@szeider.net

Abstract. We propose Q(D)-resolution, a proof system for Quantiﬁed Boolean
Formulas. Q(D)-resolution is a generalization of Q-resolution parameterized bya dependency scheme D. This system is closely related to search-based QCNF
solvers that use dependency schemes to generalize the QDPLL algorithm, suchas DepQBF. We prove that Q(Dstd )-resolution is sound by presenting a transformation of Q(Dstd )-resolution refutations into ordinary Q-resolution refutations,where Dstd denotes the so-called Standard Dependency Scheme.

1

Introduction

Most QBF solvers generate certiﬁcates for the (un)satisﬁability of input formulas. Thesecertiﬁcates can help verify the solver’s correctness or provide additional information
to an application that uses the solver as a subroutine. Search-based QBF (QDPLL)
solvers typically use Q-resolution [2] refutations for certiﬁcates [5]. QDPLL solvers
normally assign variables in the order induced by the quantiﬁer preﬁx of an input QBF(in prenex normal form). In this case, the trace generated by the solver can be used
to construct a Q-resolution refutation or a cube resolution proof of this formula [3].
Since assigning variables in the order given by the quantiﬁer preﬁx can impair solver
performance, it was suggested to use dependency schemes [6, 7] to give solvers more
freedom in choosing the order of variable assignments [1] (informally, a dependency
scheme is a mapping D that associates each formula F with a binary relation DF on its
variables that represents potential variable dependencies). This idea was successfully
implemented in the state-of-the-art solver DepQBF [4, 1]. However, DepQBF’s use of
dependency schemes breaks the immediate correspondence between solver traces andQ-resolution proofs.
In this article, we propose Q(D)-resolution, a proof system for Quantiﬁed Boolean
Formulas in prenex CNF normal form (QCNF). Q(D)-resolution is a generalization of
Q-resolution, parameterized by a dependency scheme D. Q(D)-resolution uses a more
powerful version of the universal reduction rule found in Q-resolution: a universallyquantiﬁed variable x can be removed from a clause as long as that clause contains novariables that may depend on x, according to D [1]. Q(D)-resolution is closely related
to search-based QCNF solvers that use dependency schemes to generalize the QDPLL
algorithm in the spirit of DepQBF.
Our main contribution is an algorithm that transforms a Q(Dstd )-resolution refutation of a formula into an ordinary Q-resolution refutation of the same formula, whereThis research was supported by the ERC (COMPLEX REASON, 239962).

Dstd is the so-called Standard Dependency Scheme [7]. Due to space constraints all
proofs are placed in the appendix.

2

Preliminaries

We consider quantiﬁed boolean formulas in quantiﬁed conjunctive normal form (QCNF).
A QCNF formula consists of a (quantiﬁer) preﬁx and a CNF formula, called the matrix.
A CNF formula is a ﬁnite set of clauses, where each clause is a ﬁnite set of literals.
Literals are negated or unnegated propositional variables. If x is a variable, we put
x = ¬x and ¬x = x, and let var (x) = var (¬x) = x. If X is a set of literals, wewrite X for the set { x : x ∈ X }. For a clause C, we let var (C) be the set of variables occuring (negated or unnegated) in C. For a QCNF formula F with matrix F ,we put var (F) = var (F ) = ∪C∈F var (C), and lit(F) = var (F) ∪ var (F). We
call a clause tautological if it contains the same variable negated as well as unnegated.
Unless otherwise stated, we assume that the matrix of a formula contains only non-tautological clauses. The preﬁx of a QCNF formula F is a sequence Q1 x1 . . . Qn xn ofquantiﬁcations Qi xi , where x1 , . . . , xn is a permutation of var (F) and Qi ∈ {∀, ∃}for 1 ≤ i ≤ n. We deﬁne the depth of variable xp as δF (xp ) = p, and let qF (xp ) = Qp .
The sets of existential and universal variables occurring in F are given by var ∃ (F) ={ x ∈ var (F) : qF (x) = ∃ } and var ∀ (F) = { x ∈ var (F) : qF (x) = ∀ }, respectively. We deﬁne RF = { (x, y) : δF (x) < δF (y) } and write RF (x) = { y ∈var (F) : (x, y) ∈ RF } and LF (x) = { y ∈ var (F) : (y, x) ∈ RF }, wherex ∈ var (F). A proto-dependency scheme is a mapping D that associates each QCNF
formula F with a binary relation DF ⊆ RF . The trivial dependency scheme Dtrv mapstrv
= { (x, y) ∈ RF : qF (x) = qF (y) }.
each QCNF formula F to the relation DF

3

Q(D)-Resolution

Deﬁnition 1 (Q(D)-resolution derivation). Let F be a QCNF formula with matrix
F and let D be a proto-dependency scheme. A (tree-like) Q(D)-resolution derivationfrom F is a pair (T, λ), where T = (V (T ), E(T )) is a rooted binary tree and λ is amapping that associates each t ∈ V (T ) with a non-tautological clause Ct and satisﬁes
the following conditions.
1. If t is a leaf of T then Ct ∈ F .
2. If t has distinct children t1 and t2 , there is an existential variable e ∈ var ∃ (F)such that Ct = (Ct1 ∪ Ct2 ) \ {e, ¬e} and {e, ¬e} ⊆ Ct1 ∪ Ct2 .
3. If t has a single child t , there is a literal  with var () ∈ var ∀ (F) such that  ∈ Ct
and Ct = Ct \ {}. Moreover, there is no existential variable e ∈ var (Ct ) suchthat (var (), e) ∈ DF .
We say π derives Cr , where r denotes the root of T . The derivation π is a Q(D)-resolution refutation of F if it derives the empty clause.
Ordinary (tree-like) Q-resolution [2] corresponds to Q(Dtrv )-resolution (more precisely,
these systems polynomially simulate each other).

Let D be a proto-dependency scheme, and let π = (T, λ) be a Q(D)-resolution
derivation from a QCNF formula F. By the height of π we mean the height of T , while
the size of π is the number of vertices in T . For t ∈ T , let Tt denote the subtree of T
rooted at t, and λt the restriction of λ to Tt . Then πt = (Tt , λt ) is a Q(D)-resolution
derivation. We call πt a subderivation of π.
We implicitly associate with π a function ρπ : E(T ) → lit(F) that maps an edge(t, t ) of T to the (unique) literal in λ(t ) \ λ(t), where t is a child of t . Let e ∈ E(T )and v = var (ρπ (e)). If v is an existential variable of F then e is a resolution step,otherwise e is a universal reduction step. In either case we say e is a derivation step andthat e reduces v. The set of variables reduced by some resolution step of π is denoted
resolved (π). We say π is ordered if the sequence of variables reduced on any branch of
T is in the order of RF . That is, for any pair (e1 , e2 ) ∈ E(T ) × E(T ) such that there isa path from the root of T to an endpoint of e2 passing through e1 we have (x, y) ∈ RF ,where x is the variable reduced by e1 and y is the variable reduced by e2 .
Lemma 2. Let D be a proto-dependency scheme and F a QCNF formula. Any ordered
Q(D)-resolution refutation of F is a Q(Dtrv )-resolution refutation of F.
We now describe two operations on Q(D)-resolution derivations (detailed deﬁnitions are given in the appendix). Let D be a proto-dependency scheme and let F be
a QCNF formula. Let π = (T, λ) and π  = (T  , λ ) be Q(D)-resolution derivations
from F deriving the clauses C and C  , respectively. If u is a universal variable andu ∈ var (C) then red (π, u) is obtained by attaching a new universal reduction step tothe root of π that reduces u. The resulting derivation is a Q(D)-resolution derivationthat derives C \ {u, ¬u} provided there is no existential variable e ∈ var (C) such that(u, e) ∈ DF .
If {e, ¬e} ⊆ C ∪ C  for some e ∈ var ∃ (F), and (C ∪ C  ) \ {e, ¬e} is non-tautological then res(π, π  , e) is constructed by attaching a resolution step to the rootsof π and π  that reduces e. The result is a Q(D)-resolution derivation of the clause(C ∪ C  ) \ {e, ¬e}.
We say π and π  are equivalent and write π ≡ π  if there is a bijection f : V (T ) →V (T  ) such that f is an isomorphism of T and T  , and λ(t) = λ (f (t)) for each t ∈ T .

4Standard Dependencies

Deﬁnition 3 (Connected). Let F be a QCNF formula with matrix F and X ⊆ var (F).
An X-path between clauses C, C  ∈ F is a sequence C1 , . . . , Ck of clauses in F with
C1 = C and C  = Ck such that var (Ci ) ∩ var (Ci+1 ) ∩ X = ∅ for all 1 ≤ i < k.
The clauses C, C  ∈ F are connected with respect to X if there is an X-path between
them. We extend this to variables and say x, y ∈ var (F) are connected with respect to
X if there are clauses C, C  ∈ F such that C and C  are connected with respect to X
and x ∈ var (C), y ∈ var (C  ).
Deﬁnition 4 (Standard Dependency Scheme [7]). Let F be a QCNF formula withmatrix F and let x, y ∈ var (F) such that qF (x) = qF (y). We call {x, y} a dependency
pair with respect to X ⊆ var (F) if and x and y are connected with respect to X. Thestandard dependency scheme Dstd associates each QCNF formula F with the relation
stdDF= { (x, y) ∈ RF : {x, y} is a dependency pair with respect to RF (x)∩var ∃ (F) }.
Observe that the mapping Dstd is a proto-dependency scheme. The next statement is aslightly modiﬁed version of a result from [9].
Lemma 5. Let D be a proto-dependency scheme and let F be a QCNF formula withmatrix F . Let x, y ∈ var (F) be distinct variables. Let π = (T, λ) be a Q(D)-resolution
derivation from F, and let C be the clause derived by π. If x, y ∈ var (C) then x and y
are connected with respect to resolved (π).
Lemma 5 allows us to establish the following corollary, which is used in the proof of
Lemma 8 below to rule out the existence of universal reduction steps of a certain form.
Corollary 6. Let D be a proto-dependency scheme. Let F be a QCNF formula andlet x, y ∈ var (F) such that (x, y) ∈ RF and qF (x) = qF (y). Let π = (T, λ) be a
Q(D)-resolution derivation from F with x, y ∈ var (C), where C is the clause derived
std
by π. If resolved (π) ⊆ RF (x) then (x, y) ∈ DF.

5

Reordering Q(D std )-resolution refutations

The next result shows that universal reduction steps can be inserted into an ordered
Q(D)-resolution derivation to obtain another ordered Q(D)-resolution derivation. This
statement holds for arbitrary proto-dependency schemes D.
Proposition 7. Let D be a proto-dependency scheme. Let F be a QCNF formula withu ∈ var ∀ (F), and let π ≡ red (π  , u) be a Q(D)-resolution derivation from F suchthat π  is ordered. Given π, one can compute an ordered Q(D)-resolution derivationfrom F that derives the same clause as π.
Lemma 8. Let F be a QCNF formula and let e ∈ var ∃ (F). Let π ≡ res(π1 , π2 , e)be a Q(Dstd )-resolution derivation of a clause C from F such that π1 and π2 are ordered. Given π, one can compute an ordered Q(Dstd )-resolution derivation from F thatderives a clause C  ⊆ C.
Proposition 7 and Lemma 8 are instrumental in proving our main result, as stated below.
Recall that Q(Dtrv )-resolution is equivalent to ordinary Q-resolution.
Theorem 9. Given a Q(Dstd )-resolution refutation of a QCNF formula F one cancompute a Q(Dtrv )-resolution refutation of F.

6

Conclusion

A Q(Dtrv )-resolution refutation computed from a Q(Dstd )-resolution refutation using
the algorithm of Theorem 9 can be of size exponential in the size of the input refutation.
It is an open question whether this is an artifact of our approach or whether there is infact an exponential separation between Q(Dstd )-resolution and Q(Dtrv )-resolution. The
resolution-path dependency scheme [8, 9] is a strict generalization of Dstd . We believethat an analogue of Theorem 9 can be proved for a slightly restricted version of theresolution-path dependency scheme.

References
1. Armin Biere and Florian Lonsing. Integrating dependency schemes in search-based QBF
solvers. In Ofer Strichman and Stefan Szeider, editors, Theory and Applications of Satisﬁability Testing - SAT 2010, volume 6175 of LNCS, pages 158–171. Springer, 2010.
2. H. Kleine Büning, M. Karpinski, and A. Flögel. Resolution for quantiﬁed Boolean formulas.
Information and Computation, 117(1):12–18, 1995.
3. Enrico Giunchiglia, Massimo Narizzano, and Armando Tacchella. Clause/term resolution
and learning in the evaluation of quantiﬁed Boolean formulas. J. Artif. Intell. Res. (JAIR),
26:371–416, 2006.
4. Florian Lonsing. Dependency Schemes and Search-Based QBF Solving: Theory and Practice.
PhD thesis, Johannes Kepler University, Linz, Austria, April 2012.
5. Aina Niemetz, Mathias Preiner, Florian Lonsing, Martina Seidl, and Armin Biere. Resolutionbased certiﬁcate extraction for QBF. In Alessandro Cimatti and Roberto Sebastiani, editors,
Theory and Applications of Satisﬁability Testing SAT 2012, volume 7317 of Lecture Notes in
Computer Science, pages 430–435. Springer Berlin Heidelberg, 2012.
6. Marko Samer. Variable dependencies of quantiﬁed CSPs. In Iliano Cervesato, Helmut Veith,and Andrei Voronkov, editors, Proceedings of LPAR 2008, 15th International Conference on
Logic for Programming, Artiﬁcial Intelligence, and Reasoning, November 22-27, 2008 Doha,
Qatar, volume 5330 of LNCS, pages 512–527. Springer, 2008.
7. Marko Samer and Stefan Szeider. Backdoor sets of quantiﬁed Boolean formulas. Journal ofAutomated Reasoning, 42(1):77–97, 2009.
8. Friedrich Slivovsky and Stefan Szeider. Computing resolution-path dependencies in linear
time. In Theory and Applications of Satisﬁability Testing - SAT 2012, volume 7317 of Lecture
Notes in Computer Science, pages 58–71. Springer, 2012.
9. Allen Van Gelder. Variable independence and resolution paths for quantiﬁed boolean formulas. In Jimmy Lee, editor, Principles and Practice of Constraint Programming - CP 2011,
volume 6876 of Lecture Notes in Computer Science, pages 789–803. Springer Verlag, 2011.

Appendix

Proof of Lemma 2
Proof. Let π = (T, λ) be an ordered Q(D)-refutation of F. Towards a contradiction
assume that there is a universal reduction step (t, t ) ∈ E(T ) reducing the variableu ∈ var ∀ (F) such that var (λ(t )) ∩ var ∃ (F) ∩ RF (u) = ∅. Let e ∈ var (λ(t )) ∩var ∃ (F)∩RF (u). Since π is a refutation, on the path from the root of T to t there has tobe a resolution step (s, s ) ∈ E(T ) that reduces e. But (ρπ ((s, s )), ρπ ((t, t ))) = (e, u)and (e, u) ∈/ RF , so π is not ordered.

Deﬁnitions of res(π, π , e) and red (π, u)
Let D be a proto-dependency scheme and let F be a QCNF formula. Let π = (T, λ)and π  = (T  , λ ) be Q(D)-resolution derivations from F deriving the clauses C andC  , respectively. If u is a universal variable and u ∈ var (C) then red (π, u) is deﬁned
as follows. We let red (π, u) = (T  , λ ), where V (T  ) = V (T ) ∪ {r } for somer ∈/ V (T ), E(T  ) = E(T ) ∪ {(r , r)}, and r denotes the root of T . The mapping
λ : V (T  ) → 2lit(F ) is given by

C \ {u, ¬u} if t = r ;λ (t) =λ(t)otherwise.
If {e, ¬e} ⊆ C ∪C  for some e ∈ var ∃ (F), and (C ∪C  )\{e, ¬e} is non-tautological then res(π, π  , e) = (T  , λ ) is deﬁned as follows. We let V (T  ) = V (T )∪V (T  )∪{r } and E(T  ) = E(T ) ∪ E(T  ) ∪ {(r , r), (r , r )}, where r ∈/ V (T ) ∪ V (T  ) andr, r denote the roots of T, T , respectively. (Without loss of generality, we will assume
that T and T  are vertex-disjoint.) The mapping λ : V (T  ) → 2lit(F ) is given by⎧⎪⎨(C1 ∪ C2 ) \ {e, ¬e} if t = r ;λ(t) = λ1 (t)if t ∈ V (T );⎪⎩λ2 (t)
otherwise.

Proof of Lemma 5
Proof. By induction on the height h of π. If h = 0 then C ∈ F and {x, y} is adependency pair with respect to the empty set. Suppose the statement of the lemma
holds for derivations of height up to k and let h = k + 1. Suppose π ≡ red (π  , u)for a suitable derivation π  and a universal variable u. Then x, y ∈ var (C  ), whereC  is the clause derived by π  . Hence {x, y} is a dependency pair with respect toresolved (π  ) = resolved (π) by induction hypothesis. Suppose π ≡ res(π1 , π2 , e) forsuitable derivations π1 , π2 and an existential variable e. Let C1 and C2 be the clausesderived by π1 and π2 , respectively. If x, y ∈ var (C1 ) or x, y ∈ var (C2 ) the statement again follows by induction hypothesis. So assume, without loss of generality, thatx ∈ var (C1 ) and y ∈ var (C2 ). Note that e ∈ var (C1 ) ∩ var (C2 ) and that both π1 andπ2 have height at most k. By induction hypothesis {x, e} is a dependency pair with respect to resolved (π1 ), and {y, e} is a dependency pair with respect to resolved (π2 ). Let
C1 , . . . , Ck 1 be a resolved (π1 )-path with x ∈ C1 and e ∈ Ck 1 , and let C1 , . . . , Ck2 be a
resolved (π2 )-path with e ∈ C1 and y ∈ Ck2 . The sequence C1 , . . . , Ck1 , C1 , . . . , Ck2
is an X-path where X = resolved (π1 ) ∪ resolved (π2 ) ∪ {e} = resolved (π), and so x
and y are connected with respect to resolved (π).

Proof of Proposition 7
Proof. We prove a slightly stronger statement saying that the derivation to be computed
has height bounded by the height of π. The proof is by induction on the height h of π.
The base case h = 1 is immediate. Assume the statement holds for derivations up toheight k and let h = k + 1. Suppose π  ≡ red (π1 , v) for suitable π1 and v ∈ var ∀ (F),and let C  be the clause derived by π  . If v ∈ RF (u) then π is already ordered, so
suppose v ∈ LF (u). Let C1 be the clause derived by π1 . We must have u, v ∈ var (C1 ),so π2 = red (π1 , u) is a Q(D)-resolution derivation of the clause C2 = C1 \ {u, ¬u}.
The height of π2 is at most k, so by induction hypothesis one can compute an orderedderivation π3 of height at most k that derives C2 . Moreover, v ∈ var (C2 ) so red (π3 , v)
is an ordered Q(D)-resolution derivation of the clause C3 = C2 \ {v, ¬v} with heightat most h. Note that C = (C1 \ {v, ¬v}) \ {u, ¬u} = (C1 \ {u, ¬u}) \ {v, ¬v} = C3 .
Suppose π  ≡ res(π1 , π2 , e) where π1 and π2 derive C1 and C2 , respectively, ande ∈ var ∃ (F). For i ∈ {1, 2}, let πi = red (πi , u) if u ∈ var (Ci ) and πi = πi otherwise.
Both π1 and π2 are Q(D)-resolution derivations of height at most k. Moreover, π1 andπ2 are ordered because π  is. For i ∈ {1, 2}, let πi be a derivation given by applying
the induction hypothesis to πi . It is straightforward to check that π ∗ = res(π1 , π2 , e)
is an ordered Q(D)-resolution derivation of C and that π ∗ has height at most h.

Proof of Lemma 8
Proof. The proof is by induction on the size s of π. The base case where π1 and π2
are of size 1 is immediate. Assume the statement of the lemma holds for derivations ofsize less than k > 3 and let s = k. Without loss of generality, we make the following
assumptions.
1. If the sizes of π1 and π2 are both greater than 1, and y and y  are the variables
reduced by the ﬁnal reduction steps of π1 and π2 , respectively, then y ∈ LF (y  ) ∪{y  }.
2. The size of π1 is greater than 1.
Let y be the variable reduced by the ﬁnal reduction step of π1 (y is well deﬁned byassumption 2). If e ∈ LF (y) the derivation π is already ordered, so let e ∈ RF (y).
Suppose y ∈ var ∀ (F). Then π1 ≡ red (π1 , y) for a suitable π1 deriving a clause C1 .

Note that y, e ∈ var (C1 ). Because π1 is ordered and y is reduced in its ﬁnal reduction
std
step we must have resolved (π1 ) ⊆ RF (y). By Corollary 6 we get (y, e) ∈ DF
, whichstd
contradicts π’s being a Q(D )-resolution derivation.
Thus y ∈ var ∃ (F) and π1 ≡ res(π1 , π1 , y) for suitable derivations π1 and π1 .
Suppose π1 , π1 , and π2 derive the clauses C1 , C1 , and C2 , respectively. We distinguishthree cases.
1. Suppose y ∈ var (C2 ) and let y ∈ C2 such that var (y ) = y. Either C1 orC1 must contain y . Without loss of generality assume y ∈ C1 . Since the ﬁnal
resolution step of π reduces e, there is an e ∈ C2 such that var (e ) = e, ande ∈ C1 ∪ C1 . If e ∈ C1 we let π ∗ = res(π1 , π2 , e). It is straightforward to verify
that π ∗ is a Q(Dstd )-resolution derivation of size less than k that derives a clauseC  ⊆ C. Moreover, both π1 and π2 are ordered. Applying the induction hypothesis,
we obtain an ordered Q(Dstd )-resolution derivation of a clause C  ⊆ C  ⊆ C. Ife ∈/ C1 then C1 ⊆ C and π1 yields the desired derivation.
2. Suppose y ∈/ var (C2 ) and e ∈ var (C1 ) ∩ var (C1 ). Then πa = res(π1 , π2 , e)and πb = res(π1 , π2 , e) are well deﬁned Q(Dstd )-resolution derivations of clauses
Ca and Cb , respectively, and res(πa , πb , y) is a Q(Dstd )-resolution derivation of C.
Both πa and πb have size less than k, and π1 , π1 , and π2 are ordered. By induction
hypothesis, we can compute ordered Q(Dstd )-resolution derivations πa and πb suchthat πa derives Ca ⊆ Ca and πb derives Cb ⊆ Cb . If y ∈/ var (Ca ) or y ∈/ var (Cb )then Ca ⊆ C or Cb ⊆ C, and so πa or πb provides the desired derivation. Otherwise, we let π ∗ = res(πa , πb , y). The derivation π ∗ is ordered by assumption 1 in
combination with the fact that both πa and πb are ordered. Moreover, π ∗ derives aclause C  ⊆ C.
/ var (C1 ) ∩ var (C1 ). Without loss of generality
3. Suppose y ∈/ var (C2 ) and e ∈assume e ∈ var (C1 ) \ var (C1 ). Then πa = res(π1 , π2 , e) is a Q(Dstd )-resolution
derivation of a clause Ca , and res(πa , π1 , y) is a Q(Dstd )-resolution derivation of
C. The derivation πa has size less than k and both π1 and π2 are ordered. By induction hypothesis, we can compute an ordered Q(Dstd )-resolution derivation πa of aclause Ca ⊆ Ca . If y ∈/ var (Ca ) then Ca ⊆ C and πa yields the desired derivation. Otherwise, let π ∗ = res(πa , π1 , y). The derivation π ∗ is Q(Dstd )-resolution
derivation of a clause C  ⊆ C, and it is ordered by assumption 1.

Proof of Theorem 9
Proof. Let π be a Q(Dstd )-resolution refutation of F. We claim that we can computean ordered Q(Dstd )-resolution refutation π  of F. By Lemma 2 the derivation π  is a
Q(Dtrv )-resolution refutation of F. We prove the claim by induction on the numberof unordered subderivations of π. If π contains no unordered subderivations, then inparticular π itself is ordered. Otherwise, let πu be an unordered subderivation of π suchthat πu contains no unordered subderivations, and let C be the clause derived by πu .
We can apply either Proposition 7 or Lemma 8 to obtain an ordered Q(Dstd )-resolution
derivation πo that derives a clause C  ⊆ C. We construct a new Q(Dstd )-resolution
refutation π  of F by replacing πu with πo in π and (possibly) removing redundant
derivation steps. The number of unordered subderivations of π  is strictly smaller than
the number of unordered subderivations of π, so we can apply the induction hypothesis
to get an ordered Q(Dstd )-resolution refutation of F.

Extending DPLL-Based QBF Solvers
to Handle Free Variables
William Klieber1, Mikoláš Janota2, Joao Marques-Silva2,3, and Edmund Clarke1
1

1

Carnegie Mellon University, Pittsburgh, PA, USA
2
IST/INESC-ID, Lisbon, Portugal
3
University College Dublin, Ireland

Introduction

In a number of interesting applications (such as automatic synthesis of a reactive
system from a formal speciﬁcation [1]), one needs to consider open formulas,i.e., formulas with free (unquantiﬁed) variables. A solution to such a QBF is aformula equivalent to the given one but containing no quantiﬁers and using only
those variables that appear free in the given formula. For example, a solution
to the open QBF formula (∃x. (x ∧ y) ∨ z) is the formula y ∨ z.
In [10], it was shown how clause/cube learning for DPLL-based CDCL QBF
solvers can be reformulated in terms of sequents and extended to non-CNF,
non-prenex formulas. This technique uses ghost variables to handle non-CNF
formulas in a manner that is symmetric between the existential and universal
quantiﬁers. We show that this sequent-based technique can be naturally extended to handle QBFs with free variables.
A naı̈ve way to recursively solve an open QBF Φ is shown in Figure 1.
Roughly, we Shannon-expand on the free variables until we’re left with only
closed-QBF problems, which are then handed to a closed-QBF solver. If the freevariables are always branched on in the same order, then the algorithm eﬀectively builds an ordered BDD [6], assuming that the ite function is memoizedand performs appropriate simpliﬁcation. The naı̈ve algorithm suﬀers from many
ineﬃciencies. In terms of branching behavior, it is similar to the DPLL algorithm, but it lacks non-chronological bracktracking and an equivalent of clauselearning. The main contribution of this extended abstract is to show how an existing closed-QBF algorithm can be modiﬁed to directly consider formulas withfree variables. A more detailed treatment will be published at CP 2013.

function solve(Φ) {if (Φ has no free variables) {return closed_qbf_solve(Φ);}
x := (a free variable in Φ);
return ite(x, solve(Φ with x substituted with True),solve(Φ with x substituted with False));}Fig. 1. Naive algorithm. The notation “ite(x, φ1 , φ2 )” denotes a formula with an
if-then-else construct that is logically equivalent to (x ∧ φ1 ) ∨ (¬x ∧ φ2 ).

In related work, various approaches [11,5,7] have been proposed for open
QBFs of the form ∃X. φ. For QBFs with arbitrary quantiﬁer preﬁxes, the only
other work of which we are aware is that of Becker, Ehlers, Lewis, and Marin [1],which uses computational learning to generate CNF, DNF, or CDNF formulas,and that of Benedetti and Mangassarian [3], which adapts sKizzo [2] for open
QBF. The use of SAT solvers to build BDDs [13,9] has also been investigated.
1.1

Preliminaries

Input Formulas. We consider prenex formulas of the form (Q1 X1 ...Qn Xn . φ),where Qi ∈ {∃, ∀} and φ is quantiﬁer-free and represented as a DAG. The logicalconnectives allowed in φ are conjunction, disjunction, and negation.
Quantiﬁer Order. In a formula such as ∀x.∃y. φ, where the quantiﬁer of yoccurs inside the scope of the quantiﬁer of x, we say that y is downstream ofx. All quantiﬁed variables in are considered downstream of all free variables.
Substitution. Given a partial assignment π, we deﬁne “Φ|π ” to be the resultof the following: For every assigned variable x, we replace all occurrences of xin Φ with the assigned value of x (and delete the quantiﬁer of x, if any).

2

TheoryWe employ ghost variables to provide a modiﬁcation of the Tseitin transformation that is symmetric between the two quantifer types. The idea of using asymmetric transformation was ﬁrst explored in [14]. Similar ideas have beenused to handle non-prenex formulas in [10] and “don’t care” propagation in [8].
Where the Tseitin transform would introduce a Tseitin variable g to represent
a subformula, we instead introduce two ghost variables: an existential variable g ∃and a universal variable g ∀ . Two new innermost quantiﬁcation blocks are added
to the formula for the ghost variables. For example, if the original quantiﬁer
preﬁx was ∃e ∀u, then the new preﬁx would be ∃e ∀u ∃g ∃ ∀g ∀ .
Deﬁnition 1 (Consistent assignment to ghost variable). Given a quantiﬁer type Q ∈ {∃, ∀} and an assignment π, we say that a ghost literal g Q is
assigned consistently under π iﬀ g Q |π = (the formula represented by g Q )|π .
To deﬁne the semantics of QBF with ghost variables, we use a three-valued logic
with a third value dontcare. We call it “don’t care” because we need to deal withassignments with inconsistently assigned ghost variables, but we don’t really careabout such assignments. In our three-valued logic, a conjunction (or respectively
disjunction) of boolean values evaluates to false (resp. true) if any conjunct isfalse (resp. if any disjunct is true), and otherwise it evaluates to dontcare if any
conjunct (resp. disjunct) is dontcare. The negation of dontcare is dontcare.
Deﬁnition 2 (Semantics with Ghost Vars). Given an assignment π to all
non-ghost variables and a subset of the ghost variables, we deﬁne Φπ as follows:
if every ghost variable in π is assigned consistently
Φ|πΦπ :=
dontcare otherwiseFor convenience in deﬁning Φπ for a partial assignment π, we assume that theformula is prepended with a dummy “quantiﬁer” block for free variables. For
example, (∃e. e ∧ z) becomes (Fz. ∃e. e ∧ z), where F denotes the dummy blockfor free variables. We deﬁne Φπ for a partial assignment π as follows:Qx. Φπ = Φπ if x ∈ vars(π)
∃x. Φπ = Φ(π ∪ {x}) ∨ Φ(π ∪ {¬x}) if x ∈ vars(π)
∀x. Φπ = Φ(π ∪ {x}) ∧ Φ(π ∪ {¬x}) if x ∈ vars(π)
Fx. Φπ = x ? Φ(π ∪ {x}) : Φ(π ∪ {¬x}) if x ∈ vars(π)
The notation “x ? φ1 : φ2 ” denotes a formula with an if-then-else construct thatis logically equivalent to (x∧φ1 )∨(¬x∧φ2 ). Note that if Φ contains free variables
unassigned by π, then Φπ is a formula in terms of these free variables.
Deﬁnition 3 (Sometimes-Dontcare). A formula φ is said to be sometimesdontcare iﬀ there is an assignment π under which φ evaluates to dontcare.
Deﬁnition 4 (Game-State Speciﬁer, Match). A game-state speciﬁer isa pair Lnow , Lfut consisting of two sets of literals, Lnow and Lfut . We say that
Lnow , Lfut matches an assignment π iﬀ:
1. for every literal  in Lnow , |π = true, and
2. for every literal  in Lfut , either |π = true or  ∈ vars(π).
For example, {e}, {u} matches the assignments {e} and {e, u}, but does notmatch {} or {e, ¬u}. Note that, for any literal , if {, ¬} ⊆ Lfut , then
Lnow , Lfut matches an assignment π only if π doesn’t assign .
Deﬁnition 5 (Sequent). The sequent “ Lnow , Lfut |= Φ ⇔ ψ” means “for all
assignments π that match Lnow , Lfut , if Φπ is not sometimes-dontcare, thenΦπ is logically equivalent to ψ|π ”.

3Algorithm

The top-level algorithm is based on the well-known DPLL algorithm, exceptthat sequents are used instead of clauses. Similar to how SAT solvers maintaina clause database, our solver maintains a sequent database. A SAT solver’s
clause database is initialized to contain exactly the set of clauses produced by
the Tseitin transformation of the input formula Φin into CNF. Each clause in
the Tseitin transformation corresponds to two sequents in our initial sequent
database (one with existential ghost variables, and one with universal). Literals
are placed in Lfut if allowed by Proposition 2 of [10]; otherwise, in Lnow .
When the current assignment matches a sequent in the database, the solver
performs learning to add a new sequent of the form Lnow , Lfut |= (Φin ⇔ ψ)
to the database. If Lnow is empty, then the solver returns ψ as the ﬁnal answer.
Otherwise, it backtracks to the earliest decision level at which the newly learned
sequent will trigger a forced literal in propagation.
Propagation. Propagation is similar to that of closed-QBF solvers. Consider
a sequent Lnow , Lfut |= (Φin ⇔ ψ) in the sequent database. If, under πcur ,1. there is exactly one unassigned literal  in Lnow , and2. no literals in Lnow ∪ Lfut are assigned false, and3.  is not downstream of any unassigned literals in Lfut ,then ¬ is forced — it is added to the current assignment πcur . Propagation
ensures that the solver never re-explores areas of the search space for which it
already knows the answer, ensuring progress and eventual termination.
Learning. The solver performs learning after the current assignment πcurmatches a sequent in the database. The learning procedure is based on theclause learning introduced for SAT in [12] and adapted for QBF in [15] andadapted for sequents in [10]. We use resolution-like inference rules to infer new
sequents by ‘resolving’ two sequents: (1) a sequent containing a forced literalr and (2) the sequent that forced r (i.e., the antecedent of r). The rules forresolving on free variables and existential variables are shown below; the rule foruniversal variables is similar.
Resolving on a literal r that is existentially quantiﬁed:
Lnow∪ {r}, Lfut|= (Φin ⇔ false)1
1
Lnow∪ {¬r}, Lfut|= (Φin ⇔ ψ)
2
2
fut
fut
r is not downstream of any  such that  ∈ Lfut
1 and ¬ ∈ (L1 ∪ L2 )
fut
fut
Lnow
∪ Lnow
1
2 , L1 ∪ L2 ∪ {¬r} |= (Φin ⇔ ψ)

Resolving on a literal r that is free in Φin :Lnow∪ {r}, Lfut|= (Φin ⇔ ψ1 )1
1Lnow
∪ {¬r}, Lfut|= (Φin ⇔ ψ2 )
2
2
fut
fut
Lnow
∪ Lnow
1
2 , L1 ∪ L2 ∪ {r, ¬r} |= (Φin ⇔ (r ? ψ1 : ψ2 ))4

Experimental Results

800
700

learnerlearner-d

CPU time (s)learner-c
We extended the existing closed-QBF
600
GQ
solver GhostQ [10] to implement the
500
400
techniques described in this paper.
300
For comparison, we used the solvers
200
and load-balancer benchmarks from100[1]. With a time limit of 800 sec0
onds, GhostQ solved 189 instances
0 200 400 600 800 1000 1200 1400 1600 1800
that none of the three solvers frominstances[1] solved, whereas there were 18 instances solved by at least one solver from [1] but not by GhostQ. The graph to
the right shows the number of non-trivial instances solved by GhostQ (about1600) and the three “learner” solvers (about 1400 and 1200) from [1]. As future
work, it may be useful to adapt closed-QBF preprocessing techniques such as
blocked-clause elimination [4] to open QBF.



References
1. B. Becker, R. Ehlers, M. D. T. Lewis, and P. Marin. ALLQBF Solving by Computational Learning. In S. Chakraborty and M. Mukund, editors, ATVA, volume
7561 of Lecture Notes in Computer Science, pages 370–384. Springer, 2012.
2. M. Benedetti. sKizzo: A Suite to Evaluate and Certify QBFs. In CADE, 2005.
3. M. Benedetti and H. Mangassarian. QBF-Based Formal Veriﬁcation: Experienceand Perspectives. JSAT, 2008.
4. A. Biere, F. Lonsing, and M. Seidl. Blocked Clause Elimination for QBF. In
CADE, 2011.
5. J. Brauer, A. King, and J. Kriener. Existential Quantiﬁcation as Incremental SAT.
In G. Gopalakrishnan and S. Qadeer, editors, CAV, volume 6806 of Lecture Notes
in Computer Science, pages 191–207. Springer, 2011.
6. R. E. Bryant. Graph-based algorithms for boolean function manipulation. Computers, IEEE Transactions on, 100(8):677–691, 1986.
7. E. Goldberg and P. Manolios. Quantiﬁer elimination by Dependency Sequents. In
G. Cabodi and S. Singh, editors, FMCAD, pages 34–43. IEEE, 2012.
8. A. Goultiaeva and F. Bacchus. Exploiting QBF Duality on a Circuit Representation. In AAAI, 2010.
9. J. Huang and A. Darwiche. Using DPLL for Eﬃcient OBDD Construction. In
SAT, 2004.
10. W. Klieber, S. Sapra, S. Gao, and E. M. Clarke. A Non-prenex, Non-clausal QBF
Solver with Game-State Learning. In SAT, 2010.
11. K. L. McMillan. Applying SAT Methods in Unbounded Symbolic Model Checking.
In E. Brinksma and K. G. Larsen, editors, CAV, volume 2404 of Lecture Notes in
Computer Science, pages 250–264. Springer, 2002.
12. J. P. M. Silva and K. A. Sakallah. GRASP - a new search algorithm for satisﬁability.
In ICCAD, pages 220–227, 1996.
13. R. Wille, G. Fey, and R. Drechsler. Building free binary decision diagrams using
SAT solvers. Facta universitatis-series: Electronics and Energetics, 20(3):381–394,
2007.
14. L. Zhang. Solving QBF by Combining Conjunctive and Disjunctive Normal Forms.
In AAAI 2006.
15. L. Zhang and S. Malik. Towards a Symmetric Treatment of Satisfaction and Conﬂicts in Quantiﬁed Boolean Formula Evaluation. In CP 2002.



Certiﬁcate Extraction from Variable-Elimination
QBF Preprocessors
Allen Van Gelder
University of California, Santa Cruz http://www.cse.ucsc.edu/~avg

Abstract. Recent solvers for quantiﬁed boolean formulas have the ability to produce a certiﬁcate for their conclusion, in the form of a Qresolution proof that the input QBF is either true of false. However, inmany cases the solver does not receive the original QBF, so the produced certiﬁcate does not verify the truth value of that original QBF.
This paper addresses some aspects of the question of how to extend thecertiﬁcate produced by the QBF solver for the preprocessed QBF so thatit serves as a certiﬁcate for the original QBF.

1

Introduction

Solvers for Quantiﬁed Boolean Formulas (QBFs) are rapidly increasing in strength,
and are now at the point that they are capable of solving signiﬁcant problems
and also producing certiﬁcates so that their conclusions can be checked during
post-processing. [BJ12,NPL+ 12].
It is starting to be recognized that simply delivering a 0 or 1 answer is notgood enough, for a solver. There has to be some formal proof system to back up
claimed answers. More than just verifying a claimed answer, users want additional information relevant to their applications. While this is a very open-ended
topic, this short paper concentrates on producing certiﬁcates that can verify theconclusions of the combined work of a preprocessor and a solver. More precisely
it shows what records may be kept by a variable-elimination preprocessor thatare suﬃcient to transform a satisfying assignment of the preprocessed formula
into a satisfying assignment of the original formula.

2

Preliminaries

In general, quantiﬁed boolean formulas (QBFs) generalize propositional formulas by adding universal and existential quantiﬁcation of boolean variables. See[KBL99] for a thorough introduction. This paper uses notation and deﬁnitions
found in recent QBF papers by the same author. PCNF denotes a formula inprenex conjunctive normal form. Clauses are enclosed in [ ]. Disjoint union of sets
is denoted by “+”. Lowercase roman letters denote literals or variables, where
the context calls for such. They are existential for letters near the beginning of
the alphabet (e.g., d, e, f ), universal for letters near the end of the alphabet(e.g., u, v, w), and of indeterminate quantiﬁer type near the middle of the alphabet (e.g., p, q). Lowercase greek letters, such as α, τ , etc., denote sequencesof literals (or sets where order is immaterial). Exceptions are stated where theyoccur.
Deﬁnition 1 An assignment is a partial function from variables to truth values, and is usually represented as the set of literals that it maps to true. (Thisis sometimes called a partial assignment.) A total assignment assigns a truth
value to every variable in the quantiﬁer-free formula. Assignments are denotedby σ, τ , etc.
Applications of an assignment σ to a logical expression are denoted by qσ ,Cσ , Fσ , etc. If σ assigns variables that are quantiﬁed in Ψ , those quantiﬁers
are deleted in Ψ σ , and their variables receive the assignment speciﬁed by σ.

3

Variable-Elimination Preprocessors

We use bloqqer [BSL11] as an example of the type of preprocessor from which
we wish to draw certiﬁcates. Although the pure-literal rule, unit-clause rule, andvariable-elimination resolution rule are usually considered to be distinct actions
on existential variables, they can all be characterized as the variable-elimination
resolution rule (VER). The matrix is partitioned into three sets of clauses afteran existential literal, say q, is chosen:(A) clauses containing q,(B) clauses containing q ,(C) remaining clauses.
Recall that propositional VER forms all resolvents of a clause in set (A) and aclause in set (B), then discards tautologous resolvents and discards the sets (A)and (B). Finally, for QBF all resolvents are universally reduced.
If the set (B) is empty and (A) is nonempty, q is a pure literal, and the set ofresolvents is empty. If the set (A) contains the unit clause [q], this is a case of theunit-clause rule, and the set of resolvents consists of the clauses in set (B) withthe literal q deleted. If the set (B) contains [ q ], the situation is symmetrical.
We formalize the actions of a variable-elimination (VE) preprocessor as asequence of rounds, numbered by r for 1 ≤ r ≤ R. In each round, one variable iseliminated and records are kept to permit a certiﬁcate to be constructed later.
At this stage we are not interested in optimizations.
Variable-Elimination Resolution If the operation for round r is VER, record
the existential variable q that is eliminated, the set of clauses containing q andthe set of clauses containing q ; these two sets are deleted during round r. The
non-tautologous resolvents are given fresh clause IDs and added to the formula;these do not need to be recorded in connection with round r but their derivations
should be recorded (one resolution each).
The critical situation for generating a certiﬁcate is when the formula is true
and a hitting set needs to be found to seed an “initial-reason cube”. The hittingset (technically consistent hitting set) τr must be a partial assignment such thatevery clause in the formula at the beginning of round r has a true literal. But
the formula is a moving target, as it changes every round. So the precondition
for extending the hitting set from the end of round r to the beginning of roundr is that every clause in the formula at the end of round r is made true by τr+1 .
To extend τr+1 to τr , all clauses deleted during round r must be made true.
The procedure to accomplish the extension from τr+1 to τr in the propositional case is known from antiquity, but possibly not published archivally. However, Dechter and Rish give a closely related procedure [DR94]. Check each clausethat was deleted during round r (due to VER) and if one is found that contains
q (resp. q ) and all its other literals are false in τr+1 , then add q (resp. q ) to
τr+1 giving τr . Call this clause C0 . Assume it contains q, as the case for q issimilar. The precondition in the preceding paragraph ensures that clauses withboth q and with q cannot be chosen.
If no clause qualiﬁes for C0 in the preceding paragraph, then choose any
clause that is not made true by τr+1 as C0 . Again, assume w.l.o.g. that q ∈ C0 .
Now add q and the negation of every other literal in C0 to τr+1 , giving τr .
(Some of these literals may already be in τr+1 .) Heuristics may be used to try
to improve the choice, but any choice works.
In both cases for C0 it has no true literal in τr+1 . So every clause containing q
whose resolvent with C0 is non-tautologous is hit (made true) by τr+1 . Also every
clause containing q whose resolvent with C0 is tautologous is hit by τr . Finally
all clauses containing q are hit by τr . So the postcondition at the beginning ofround r is that every clause in the formula at the beginning of round r is hit byτr .
Universal-Variable Expansion If the operation for round r is universalvariable expansion (UVE), record the universal variable u that is eliminated,
as well as the set of round-r clauses containing u, called Γ0 (u), and the set ofround-r clauses containing u . called Γ1 (u).
The details and notation of the UVE operation are now described. Note that
there is no propositional analog of this operation. Deﬁne γ0 (u) (resp. γ1 (u)), thecompanion set for u (resp. u ) to be the set of existential variables that occur(with either polarity) in Γ0 (u) (resp. Γ1 (u)) and are later than u in the prenex.1
Next, deﬁne γ0∗ (u) inductively as follows: γ0 (u) ⊆ γ0∗ (u). If variable e ∈ γ0∗ (u)and variable f is existential and later in the prenex than u and some clausecontains both e and f (with either polarity), then f ∈ γ0∗ (u). The inductive
deﬁnition of γ1∗ (u) is similar. Correctness of this construction can be shown withstandard identities for quantiﬁers, such as

1∀u (F (u) ∧ G()) ≡ ((∀u (F (u)) ∧ G())

where u does not occur in G(),∃e (F (e) ∧ H()) ≡ ((∃e (F (e)) ∧ H())

where e does not occur in H(),

Relaxing the condition to “e depends on u” based on a dependency scheme is future
work.



as well as associativity and commutativity of “∧”.
Supersets of γ0∗ (u) and γ1∗ (u) may be used soundly. In practice the setof all existential variables later in the prenex than u provides a simple overapproximation for γ0∗ (u) and γ1∗ (u).
Further, deﬁne Γc (u) to be the set of round-r clauses not in Γ0 (u) or Γ1 (u),but which have a variable (with either polarity) in (γ0∗ (u) ∪ γ1∗ (u)), and deﬁneΓd (u) to be the remaining round-r clauses that are not in any of Γ0 (u), Γ1 (u), orΓc (u). The clauses in Γd (u) will persist into round r + 1, while all other round-r
clauses will be deleted during round r.2
The UVE step both deletes variables and clauses and inserts fresh variables
and clauses, as follows. For each (existential) variable e ∈ γ0∗ (u) create a fresh
variable, say e0u , and record that e0u evolved from e by instantiating u = 1. For
each (existential) variable e ∈ γ1∗ (u) create a fresh variable, say e1u , and recordthat e1u evolved from e by instantiating u = 1. For each clause C ∈ (Γ0 (u)+Γc (u))
create a fresh clause Cu0 by deleting u if present and replacing each variablef ∈ γ0∗ (u) by fu0 . For each clause C ∈ (Γ1 (u) + Γc (u)) create a fresh clause Cu1
by deleting u if present and replacing each variable f ∈ γ1∗ (u) by fu1 . Record
how each Cu0 and Cu1 evolved, similarly to e0u and e1u . Note that each clause inΓc (u) evolves into two fresh clauses.
The critical situation for generating a certiﬁcate is when the formula is true
and a set of hitting sets needs to be found to seed a set of “initial-reason cubes”.
Each hitting set (technically, consistent hitting set) must be a partial assignment
such that every clause in the formula has a true literal. The key requirement on
the set, following [VGWL12], is that if a hitting set in prenex order has a preﬁx
α, u, then there must also be a hitting set with preﬁx α, u , and vice versa.
So the precondition for updating each hitting set τr+1 from the end of roundr to a pair of hitting sets for the beginning of round r is that every clause in theformula at the end of round r is made true by τr+1 . To update to τr0 (possibly
containing u ) and τr1 (possibly containing u), all clauses deleted during roundr must be made true using variables that exist at the beginning of round r.
The idea has some similarities to the VER extraction. Recall that u was
expanded in round r. Partition the round (r + 1) clauses as follows:
1. Δ0u consists of clauses with some existential variable of the form fu0 (which
evolved from f during round r);
2. Δ1u consists of clauses with some existential variable of the form fu1 (which
evolved from f during round r);
3. Δdu consists of the remaining clauses.
The hitting set for Δdu in τr+1 can be transferred directly into each of τr0 andτr1 . Also, add u to τr0 and add u to τr1 .
First we describe how to complete τr0 . For each clause Cu0 ∈ Δ0u , let C be theround-r clause that evolved into Cu0 . If some literal q ∈ C already is true in τr0 ,there is nothing to do. If this case does not apply, choose any existential literal2

The usual descriptions include several “optimizations” that are unrelated to correctness, and complicate certiﬁcate extraction.

of the form e0u ∈ Cu0 that is true in τr+1 and add e to τr0 . This must be possible
because u ∈ Cu0 and τr+1 intersects Cu0 . For each clause Cu1 ∈ Δ1u , let C be theround-r clause that evolved into Cu1 . If u ∈ C, Cu1 does not exist. If u ∈ C, there
is nothing to do. Otherwise, C already intersects τr0 at some existential literal,and again there is nothing to do.
The completion of τr1 is similar, except that Δ1u is processed ﬁrst. Thus eachof τr0 and τr1 is a hitting set for the set of round-r clauses.
In the middle of the rounds a variable may have a sequence of tags, suchas (((e0w )1v )0u )1t , where t, u, v and w are universal variables in the reverse orderof their expansions. In the beginning of the round in which u was expanded
this variable was (e0w )1v . Clause identiﬁers can similarly consist of an integer ID
for the clause derived by resolution or in the original formula, modiﬁed by asequence of tags to show where it was duplicated by some universal expansion.

4

Conclusion

A method to extend hitting sets backward through the rounds of a VE preprocessor (such as bloqqer) is described and the argument for correctness is
sketched. The ﬁnal result at the beginning of round 0 is required to contain only
variables in the original formula (fed to the VE preprocessor) and to support a
Q-refutation by cube resolution (AKA term resolution). The data that needs tobe recorded to facilitate this extension is speciﬁed abstractly.
To realize the scope of the problem, it is perfectly possible that the initial
set of hitting sets presented to the VE post-processor consists of one hitting set
consisting of existential literals, none of which occur in the original formula.
Acknowledgment We thank the anonymous reviewer who pointed out errors
in an earlier version.

References[BJ12]

V. Balabanov and J. R. Jiang. Uniﬁed QBF certiﬁcation and its applications. Formal Methods in System Design, 41:45–65, 2012.
[BSL11]
A. Biere, M. Seidl, and F. Lonsing. Blocked clause elimination for QBF. In
Proc. CADE, 2011.
[DR94]
R. Dechter and I. Rish. Directional resolution: the davis-putnam procedure, revisited. In Proc. 4th Int’l Conf. on Principles of Knowledge Representation and Reasoning (KR’94), pages 134–145. Morgan Kaufmann, San
Francisco, 1994.
[KBL99] H. Kleine Büning and T. Lettmann. Propositional Logic: Deduction and
Algorithms. Cambridge University Press, 1999.
[NPL+ 12] A. Niemetz, M. Preiner, F. Lonsing, M. Seidl, and A. Biere. Resolutionbased certiﬁcate extraction for QBF (tool presentation). In Proc. SAT,
2012.
[VGWL12] A. Van Gelder, S. B. Wood, and F. Lonsing. Extended failed literal detection for QBF. In Proc. SAT, 2012.

Benchmarks from Reduction Finding
Charles Jordan1 and L ukasz Kaiser2
1

ERATO Minato Project, JST & Hokkaido University
2
LIAFA, CNRS & Université Paris Diderot
skip@ist.hokudai.ac.jp, kaiser@liafa.univ-paris-diderot.fr

1

Introduction

Consider the problem of searching for a complexity-theoretic reduction between
two decision problems, P and Q. Such a reduction is a function r satisfyingx ∈ P ⇐⇒ r(x) ∈ Q for all structures x for which it makes sense to consider
P . It is not diﬃcult to show that determining the existence of reductions is
undecidable in general. However, suﬃciently restricting the class of reductions
and structures considered results in a simpler, decidable variant that is still
meaningful from a complexity-theory perspective.
Once we can encode these reductions and structures in a ﬁnite number of bits,
the problem becomes a QBF instance with one quantiﬁer alternation (2QBF):∃r ∀x (x ∈ P ⇐⇒ r(x) ∈ Q) .

(1)

Therefore, reduction ﬁnding in this setting is essentially a Σ2p problem and it
is possible to apply QBF solvers and ASP solvers supporting disjunctive logic
programs. In this paper, we introduce various reduction-ﬁnding instances intended for benchmarking QBF solvers. For additional background, details andcomparisons with other approaches, see [4]. Automatic reduction ﬁnding was
ﬁrst considered by [1]. More generally, reduction ﬁnding is a form of program
synthesis, and similar approaches can be used more widely, see [3].

2Background

Although polynomial-time reductions are perhaps the most traditional, we focus
on a weaker class of quantiﬁer-free logical reductions used in descriptive complexity. We do not introduce descriptive complexity and the full motivation forthis class here, see [4] for the deﬁnitions we use and [2] for additional material.
The weaker class of logical reduction we consider has a number of advantages.
First, the logical formulas deﬁning the reduction make the explicit constructionof (1) reasonable. Although the class of reductions we consider is extremely limited, it still suﬃces to characterize complexity classes and complete problems
generally remain complete under these reductions. Proving that a computation
Supported in part by KAKENHI No. 25106501.

cannot be done in polynomial-time is notoriously diﬃcult, while there are techniques for proving that something cannot be done in, e.g., ﬁrst-order logic. So
our reductions are strong enough that they suﬃce to determine the relationshipbetween complexity classes, but weak enough to hope for progress.
2.1

Parameters

An instance of a reduction-ﬁnding problem is determined by several parameters,
which thus determine the diﬃculty of the underlying problem. First, we mustﬁx the two decision problems of interest: P and Q in (1). Our system supports
deﬁning these problems in ﬁrst-order logic with equality extended by a reﬂexive
transitive-closure (TC) operator, corresponding to the complexity class NL.
The choice of properties is important: choosing, e.g., the trivial properties
always true and always false results in an easy instance that is not interesting.
From the complexity-theoretic perspective, the hardness of properties deﬁned
in ﬁrst-order logic (without TC) is fairly well-understood. Therefore, formulas
using TC are most interesting and seem to be signiﬁcantly harder.
Next, there are several parameters that determine the class of reductions
being considered. Several parameters determine which atomic formulas are allowed to occur in the reduction. In particular, these parameters control whether
successor is allowed between variables (x = y + 1), and whether certain numeric constants (min, max) are available. Then, there is a parameter k ﬁxing
the dimension of the reduction (informally, the dimension determines how muchlarger the output of a reduction can be compared to the original structure). Our
reductions are deﬁned by tuples of formulas in DNF – there is also a parameterc determining how many conjunctions may occur in the DNF.
Finally, there is a parameter n determining the size of structure consideredin (1); we search only3 for reductions that are correct on structures of size n.
Given these parameters, our generator constructs the corresponding QBF
instance of (1) in several formats: qdimacs, negated qdimacs (to avoid an additional quantiﬁer alternation from CNF conversion), qpro and lparse. Increasing cprovides additional power to the class of reductions (instances become more positive), and increasing k is similar. Increasing n usually places more restrictions
on the reduction (instances become more negative). A balance between parameters is important: large c with small n is unlikely to be meaningful because thereduction is too powerful for the small class of structures.

3

Instances

Let us describe how we instantiate the parameters described above in practice,and present some experimental results on a few parameter sets.
For the two decision problems of interest, P and Q in (1), we use one of48 properties that were translated from the ﬁrst paper on automatic reduction
3

We support searching for reductions correct on a range of sizes n1 ≤ n2 when using
CEGAR, see [4].

ﬁnding [1] to allow to compare performance to their system (cf. [4]). The names
we use for the problems correspond to the names used in the system from [1], andare always 6 characters long. Below, we give a list describing these 48 problems,
to give an overview what is included.
– trivial, ntrivil, trueque, falsequ, query15, query30 (trivial or almost
trivial problems that we include for correctness testing)– reachqu (reachability, NL-complete), nreachq (negated reachability, coNLcomplete), query10 (symmetric reachability, SL-complete),– query06, query31, query33, query34, query36 (L-complete), and query71(negated query06, coL-complete),– query42, query44 (non-reﬂexive reachqu/nreachq, NL/coNL-complete),– query48, query49 (non-reﬂexive SL/coSL-complete),– query54 (strongly connected, NL-complete), query55 (symmetric query54),– query57, query58, query60, query64 (minor variations of the above),– the others4 are deﬁned in plain FO and thus correspond to AC 0 problems.
Above, we mention the classes coNL, coL, SL and coSL, however, NL=coNL
and L=coL=SL=coSL. Instances corresponding to discovering these famous collapses are interesting and appear hardest among the instances we consider.
We use the largest class of reductions supported: we allow min and max andsuccessor in the atoms (-min -max -succ) and also the use of numbers when
deﬁning constants (-nbrs). As for the dimension k (-dim), number of conjunctions c (-cls), and structure size n (-elems), the most basic set of parameters
we used was k = 1, c = 1, n = 3. Our generator is ReductionTest.native4 andthe following command can be used to generate the qdimacs ﬁle for the above
parameters and P = nreachq, Q = reachqu.
./ReductionTest.native -min -max -succ -nbrs-from nreachq -to reachqu -dim 1 -cls 1 -elems 3 -qdimacs
The formula generated by the above command has 1731 variables and 18645
clauses, but most of the variables come from CNF conversion – only 66 areunder the ﬁrst existential quantiﬁer (describing in r from eq. 1) and only 9 under
the second universal one (describing A). Instances that don’t use TC result insmaller formulas, but already setting -elems 5 above returns 29878 variables
and 530903 clauses. It is also possible to directly generate ﬁles for all problems
we consider for a given parameter set using the -gen [directory] option.
./ReductionTest.native -min -max -succ -nbrs-dim 1 -cls 1 -elems 3 -gen .
In addition to generating ﬁles, the generator can test the existence of a reduction. This is done with CEGAR using a speciﬁed SAT-solver (at present-minisat, -glueminisat or the standard solver from Intel’s Decision Procedure
Toolkit). For example, one can check the existence of a reduction from P =nreachq to Q = reachqu with the speciﬁed parameters as follows.
4

The generator with instructions, all instance names, and the collection of generated
ﬁles we used for testing are available from http://toss.sf.net/reductGen.html.

./ReductionTest.native -min -max -succ -nbrs-from nreachq -to reachqu -dim 1 -cls 1 -elems 3 -glueminisat
From the 48 properties included, the method above can generate 48 × 48 =2304 qdimacs ﬁles for each parameter set. To avoid an extra quantiﬁer alternation due to CNF conversion in qdimacs, we also tested negating the QBF
formula before CNF conversion – but results were worse than with the added
alternation (cf. [4]). To give an intuition about the hardness of the generated
QBF instances, we present below the results from [4] showing the number oftimeouts on these 2304 instances for 5 QBF solvers. The tests were performedon an Opteron 1385 (using 1 core) and with a timeout of 120s.

rareqsdepqbfqube
cirqitskizzoc=1n=3c=2n=3c=3n=3 c=1n=4c=2n=4c=3n=4
0
0
16
19
65
204
0
142
547
16
297
711
10
536
949
82
760
1082
58
673
1138
511
1092
1357
522
1058
1156
975
1327
1434

On our instances, rareqs, a recently introduced CEGAR solver, performed
best. For non-CEGAR solvers, depqbf and qube outperform skizzo and cirqit.
Between depqbf and qube the situation is less clear, some instances work muchbetter with one of these solvers, others with the other. The comparison between
skizzo and cirqit is diﬃcult as well. As to the dominance of depqbf andqube over skizzo and cirqit, it holds for almost all queries. Still, there are a
few outliers such as the reduction from query26 to query01, on which depqbf
and qube time out, but skizzo answers almost immediately.
Of course, our generator is not restricted to these problems – any problem in
NL can be deﬁned in ﬁrst-order logic with transitive closure, and these formulas
can be directly used with the -from and -to options.
Although some interesting reductions can be expressed with dimension 1,
usually this does not suﬃce. However, even parameters such as k = 2, c = 1, n =4 or k = 3, c = 1, n = 3 seem to produce very hard instances. Instances with k >1 where the properties use transitive-closure are often hard, but achieving better
performance on such instances is an important step to ﬁnding new reductions
and hopefully new complexity-theoretic knowledge.

References
1. Crouch, M., Immerman, N., Moss, J.E.B.: Finding reductions automatically. In:
Fields of Logic and Computation – Essays Dedicated to Yuri Gurevich on the Occasion of His 70th Birthday. LNCS, vol. 6300, pp. 181–200. Springer (2010)
2. Immerman, N.: Descriptive Complexity. Springer-Verlag (1999)
3. Jordan, C., Kaiser, L .: Learning programs as logical queries. In: LTC 2013
4. Jordan, C., Kaiser, L .: Experiments with reduction ﬁnding. In: Proc. SAT 2013.
LNCS, vol. 7962, pp. 192–207. Springer (2013)