DepQBF 6.0: A Search-Based QBF Solver Beyond Traditional QCDCL
Florian Lonsing Uwe Egly







Supported by the Austrian Science Fund (FWF) under grant
S11409-N23. This article will appear in the proceedings of the
26th International Conference on Automated Deduction (CADE-26), LNCS,
Springer, 2017.
    Amrit Singh Bedi, Student Member, IEEE and Ketan Rajawat, Member, IEEE The	authors are with the Department of Electrical Engineering, IIT Kanpur, Kanpur
			(UP), India 208016 (email: amritbd, ketan@iitk.ac.in).

    
=======================================================================================================================================================================================================================




We present the latest major release 
version 6.0 of the quantified Boolean formula (QBF) solver , which is
based on QCDCL. QCDCL is an extension of the conflict-driven
clause learning (CDCL) paradigm implemented in state of the art propositional
satisfiability (SAT) solvers.  The Q-resolution calculus () is
a QBF proof system which underlies QCDCL.  QCDCL solvers can produce proofs of QBFs in prenex conjunctive normal form (PCNF) as a byproduct of the
solving process.  In contrast to traditional QCDCL based on ,
implements a variant of QCDCL which is based on a
generalization of . This generalization is due to a set of additional
axioms and leaves the original Q-resolution rules unchanged. The
generalization of enables QCDCL to potentially produce exponentially
shorter proofs than the traditional variant.  We present an overview of the features
implemented in and report on experimental results which demonstrate
the effectiveness of generalized in QCDCL.







§ INTRODUCTION



Propositional satisfiability (SAT) solvers based on conflict-driven
clause learning
(CDCL) <cit.>
implement 
a combination of the DPLL algorithm <cit.> and
propositional resolution <cit.> to derive
learned clauses from a CNF to be solved.

CDCL has been extended to solve quantified Boolean formulas
(QBFs) <cit.>, resulting in the QCDCL
approach <cit.>. The
logic of QBFs allows for explicit universal and existential quantification of
propositional variables. As a consequence, the satisfiability problem of QBFs
is PSPACE-complete.

In contrast to SAT solving, where CDCL is the dominant solving paradigm in
practice, QCDCL is complemented by variable
expansion <cit.>. This
approach successively eliminates variables from a QBF until it reduces to
either true or false. Many modern solvers
(e.g. <cit.>)
implement expansion by counter-example guided abstraction refinement
(CEGAR) <cit.>.

The Q-resolution calculus
() <cit.>
is a QBF proof system that underlies QCDCL in a way that is analogous
to propositional resolution in CDCL. The empty clause is derivable
from a PCNF  by iff  is
unsatisfiable. According to QBF proof complexity, there is an
exponential separation between the sizes of proofs that variable expansion
and Q-resolution can
produce for certain QBFs <cit.>.
This
theoretical result suggests to combine such orthogonal proof systems in QBF
solvers to leverage their individual strengths.

As a first step towards a solver framework that allows for the combination of QBF
proof systems in a systematic way, we present the latest major release version 6.0 of the QCDCL solver
.[is licensed under GPLv3:
<http://lonsing.github.io/depqbf/>] In contrast to traditional
QCDCL based on
 <cit.>,
implements a variant of QCDCL that relies on a generalization of
. This generalization is due to a set of new axioms added to
 <cit.>. In practice, derivations made
by the added axioms in QCDCL are based on arbitrary QBF proof
systems. As a consequence, when applying proof systems that are orthogonal to
Q-resolution, the generalization of via the new axioms enables QCDCL as
implemented in to potentially produce exponentially shorter
proofs than traditional QCDCL. 

We report on experiments where we compare
to state of the art QBF solvers. Experimental results
demonstrate the effectiveness of generalized in QCDCL. 
Additionally, we briefly summarize the evolution of since the first 
version 0.1 <cit.>. We relate the features that
were added to the different versions of over time to the enhanced variant of QCDCL
implemented in . 







§ PRELIMINARIES



A QBF := . in prenex conjunctive normal form (PCNF) 
consists of a quantifier prefix := Q_1X_1 … Q_nX_n and a
CNF  not containing tautological clauses. 
The CNF  is defined over the propositional variables X_1 ∪…∪ X_n  
that appear in . The variable sets X_i are pairwise disjoint and Q_i
≠ Q_i+1 for 
Q_i ∈{∀, ∃}. 
QBFs := . in prenex disjunctive normal
  form (PDNF) are defined analogously to PCNFs, where  is a DNF
consisting of cubes. A cube is a conjunction of literals.
 The quantifier
l of  a literal l is  Q_i if the variable l of l appears in
X_i. If l = Q_i
and k = Q_j,
then ⁠l ≤_ k ⁠iff ⁠i ≤ j.

An assignment A maps variables  
of a QBF . to truth values true (⊤) and
false (). We
represent A = {l_1,…,l_n} 
as a set of literals such that if a variable x is
assigned true (false) then l_i ∈ A with l_i = x (l_i =
x̅), where x̅ is the negation of x.  
Further, l_i≠l_j for any l_i, l_j ∈ A with i ≠ j. 

The PCNF  under assignment A, 
written as 
[A], is the PCNF
obtained from  in which 
for all l ∈ A, all clauses containing l are removed, 
all occurrences of l̅ are deleted, and l is 
removed from the prefix. 
If the CNF of [A] is empty (respectively, contains the empty clause ∅), then 
it is satisfied (falsified) by A and 
A is a satisfying (falsifying) assignment, written as [A] = ⊤ ([A] =).
A PDNF  under an assignment
A and an empty cube are defined in a way dual to PCNFs and empty clauses. 
A QBF . 
with Q_1 = ∃ (Q_1 = ∀) 
is satisfiable iff, for x ∈ X_1, 
.[{x}] or (and)
.[{x̅}] is satisfiable. 
Two QBFs  and ' are satisfiability-equivalent 
('), iff
 is satisfiable whenever ' is
satisfiable. 






§ QCDCL AND THE GENERALIZED Q-RESOLUTION CALCULUS



In the following, we present the variant of QCDCL implemented in
that relies on a generalization of the Q-resolution calculus
(). We
illustrate the workflow of that variant in Fig. <ref>.

In general, QCDCL is based on the successive generation of assignments that
guide the application of the inference rules of to derive
learned clauses and cubes from a
given input PCNF = .. Learned cubes are dual to 
clauses. While learned clauses represent assignments that falsify the CNF
 of ψ, learned cubes represent assignments that satisfy
. 
The empty cube is derivable
from a PCNF  by iff  is
satisfiable. 
Based on our presentation of the rules of we illustrate the differences between traditional
QCDCL and the variant implemented in
.

A QCDCL solver maintains a PCNF = .' (PDNF =
.') consisting of a CNF ' (DNF ') of learned clauses
(cubes).  The clauses in  are added conjunctively to  to
obtain _ = .(∧ (⋀_C
∈' C)), and the cubes in  are added disjunctively to 
to obtain _ = .(∨ (⋁_C ∈'
C)).  It holds that _ and _.  Initially the current assignment A, the PCNF
, and PDNF  are empty.  We use the notation C, C', and C_L
for both clauses and cubes.



During propagation, the formulas _ and
_ are first simplified under the current assignment A by
computing _[A] and _[A].  Then
universal and existential reduction is applied to
_[A] and to _[A] based on the following
inference rule.

Let = . be a PCNF.


    𝑟𝑒𝑑C ∪{l}C  0.7625
    (1) C is a
    clause, l = ∀, 
    l' <_ l 
    for all l' ∈ C with l' = ∃
    or 
     
    (2) C is a
    cube, l = ∃, 
    l' <_ l 
    for all l' ∈ C with l' = ∀



Universal (existential) reduction of clauses (cubes) by rule <ref>
eliminates trailing universal (existential) literals from a
clause (cube)  with respect to the linear quantifier ordering in the prefix of the PCNF .  We
write (C) = C' ((C) = C') to denote the clause (cube) C' resulting
from clause (cube) C by fully reducing universal (existential) literals.

Let _' and _' denote the formulas obtained
by applying universal (existential) reduction to all the clauses (cubes) in
_[A] (_[A]) until saturation.  New
assignments are generated by unit literal detection with respect to
_' and _'.  If a PCNF
(PDNF)  contains a unit clause (cube) C = (l), where
l = ∃ (l = ∀), then literal
l is unit and [A'] where A' = {l}
(A' = {l̅}). 
Assignment A is extended by assignments A' derived from unit clauses
(cubes) in _' (_').
For every unit clause (cube)
C' ∈_' (C' ∈_') with C' = (l), 
the corresponding assignment A' := {l} (A' := {l̅}) is recorded.

After propagation, in conflict/solution detection it is checked whether
_' is unsatisfiable or whether _' is
satisfiable (only one of the two cases can occur). To this end, incomplete methods are applied. In traditional
QCDCL, for example, it is syntactically checked if the current
assignment A is falsifying or satisfying, i.e., whether _' contains the empty clause (i.e., _' =) or whether _' contains the empty cube (i.e., _' = ⊤).  In , we extend these
incomplete syntactic checks to incomplete semantic checks based on arbitrary QBF decision procedures
(proof systems) 
that are applied to _' and _' in a resource bounded ⁠way. 

 If neither _' is found unsatisfiable nor _'
 is found satisfiable by the incomplete satisfiability checks, then in decision
  making A is extended by heuristically assigning some decision variable x from the leftmost
quantifier block of [A] (A := A ∪{l} where
l = x), 
and propagation continues. Assignments by decision
making must follow the prefix ordering of , in contrast to assignments by
propagation (unit literals), which results in assignments of the following kind. 

Assignments generated by decision making and
propagation in QCDCL are called QCDCL assignments.


If _' (_') is found unsatisfiable
(satisfiable) in conflict/solution detection then a
learned clause
(cube) is derived using depending on the incomplete
satisfiability checks. 
In traditional QCDCL, conflict/solution detection relies only on 
falsifying or satisfying assignments. If _' = then
_' contains an empty clause C' = ∅ such that there
is a clause C ∈_ with C' = (C[A]).  Clause C is the
falsified clause with respect to assignment A. If C
appears in the given PCNF  then in traditional it is
derived trivially by the following axiom.

 
Let = . be a PCNF. 


    cl-initAC  0.79C is a clause and C ∈



If _' ≠ but _' = ⊤ then either
(1) _' contains an empty learned cube C' = ∅ 
such that there is a cube C ∈_ with
C' = (C[A]), or (2) A is a satisfying assignment that satisfies all clauses in
_'. For case (2), a cube C is derived by the
following axiom of traditional (in either case (1) or (2) cube C is the satisfied
cube with respect to A).

 
Let = . be a PCNF. 


    cu-initAC  0.79A is an assignment,  
    [A] = ⊤, 
    and C = (⋀_l ∈ A l) is a cube



supports the application of arbitrary (incomplete)
QBF decision procedures (proof systems) in conflict/solution detection and thus generalizes
the syntactic checks for falsifying and satisfying assignments  in
traditional QCDCL. 

To check the satisfiability of _', in we apply a
dynamic variant of blocked clause elimination
(QBCE) <cit.>. This approach was
introduced in version 5.0 of .  
QBCE has been presented as a
preprocessing technique to eliminate redundant blocked clauses
<cit.> from a
PCNF. If all clauses in _' are satisfied under A or
identified as blocked, then _' is determined
satisfiable. In our implementation applications of QBCE are tightly integrated in the propagation
phase via efficient data structures. Clauses that are blocked are
temporarily considered as removed from the formula. Hence such clauses
cannot be used to detect unit clauses or empty clauses during
propagation.

In addition to dynamic QBCE, we implemented incomplete QBF satisfiability
checks based on propositional abstractions of _' and
_' <cit.>, which are solved using
an integrated SAT solver. These abstractions are constructed by treating
universally quantified literals in the given PCNF  in a special
way. Propositional abstractions and SAT solving leverage the benefits of
techniques like trivial truth and trivial
falsity presented already in early search-based QBF
solvers <cit.>. Additionally, the power of
QU-resolution <cit.>, which is exponentially
stronger than Q-resolution <cit.> but has not
been applied systematically in QCDCL, is harnessed to a certain extent (cf. Example 3 in <cit.>).

As a simple way of applying a QBF decision procedure that is incomplete by its
nature we integrated the preprocessor
 <cit.> in . 
Preprocessing aims at simplifying a formula within a restricted
amount of time but might already solve certain formulas 
(cf. <cit.>). Among several techniques, applies bounded
expansion of universally quantified
variables <cit.>. Hence by
integrating in QCDCL we in fact integrate expansion, a QBF proof
system that is orthogonal to Q-resolution <cit.>. 
Due to usability issues, in the follow-up release version 6.02 of we replaced by the
expansion based QBF solver
,[<https://github.com/lonsing/nenofex>] which is applied
in a resource bounded way.

If _' (_') is found unsatisfiable
(satisfiable) by an incomplete decision procedure but, unlike above, A is neither falsifying nor satisfying, then a clause
(cube) is derived by the following generalized axioms of
. These axioms are added to and applied in addition to the traditional
axioms <ref> and <ref>.

 
Let = . be a PCNF. 


    gen-cl-initAC  0.7A is a QCDCL assignment, 
    [A] is unsatisfiable, 
    
    and C = (⋁_l ∈ Al̅) is a clause




    gen-cu-initAC  0.7A is a QCDCL assignment, 
    [A] is satisfiable, 
    
    and C = (⋀_l ∈ A l) is a cube


Note that the generalized axioms allow to derive clauses and cubes that cannot be
derived by the traditional axioms <ref>
and <ref> in general. This is due to the application of
arbitrary QBF decision procedures (proof systems) for satisfiability checking
in conflict/solution detection or in the side conditions of the axioms, respectively. In the side conditions the satisfiability of the PCNF [A] is checked, in contrast to formulas _' and _' as in conflict/solution detection. This is possible since _' [A] and _' [A].
The clause (cube) C derived by applying the generalized clause
axiom <ref> (<ref>) is the falsified
clause (satisfied cube) with respect to A.

During clause (cube) learning, a new learned clause (cube)
C_L is derived by . The falsified clause (satisfied cube) C is
the start clause (cube) of a derivation of C_L. Given A, 
clauses (cubes) which became unit during propagation are systematically resolved
based on the following Q-resolution rule.
 Let = . be a PCNF.  


    𝑟𝑒𝑠C_1 ∪{p}C_2 ∪{p̅}C_1 ∪ C_2  0.57
    For all x ∈{x, x̅}⊈(C_1 ∪ C_2), 
    
    p̅∉C_1, p
    ∉C_2, and either
     (1) C_1, C_2 are
    clauses and p = ∃or
      (2) C_1, C_2 are cubes and p = ∀


Rule <ref> does not allow the resolvent (C_1 ∪ C_2) to be a tautological clause (contradictory cube) and requires existential (universal) variables as pivots p.  In
general, learning produces a nonempty clause (cube) C_L≠∅,
which is added to the PCNF  (PDNF ) of learned clauses (cubes),
and hence  also  to  _ (_).

In backtracking, a certain subassignment A' ⊂ A is
retracted such that C_L becomes unit in propagation. C_L is called an
asserting clause (cube) <cit.>. 
Clauses (cubes) derived by rules <ref>
and <ref> (<ref>
and <ref>) are used in exactly the same way in
learning to produce asserting clauses (cubes).

QCDCL terminates (“UNSAT” or “SAT” in
Fig. <ref>) by deriving the empty learned clause (cube)
C_L = ∅. A clause (cube) resolution proof of the
unsatisfiability (satisfiability) of  can be
obtained from the derivations of the learned clauses (cubes) up to
the empty clause (cube).

By applying the generalized axioms using a complete QBF decision
procedure, the empty assignment A, and an unlimited amount of time, 
the empty clause (cube) can  
be derived right away from any given unsatisfiable (satisfiable) PCNF
. 
In practice it is crucial to apply incomplete polynomial time procedures  
to limit the time spent on the satisfiability checks.  
However,  
the costs of frequent checks may outweigh the benefits. Hence
in , satisfiability checks for applications of
the generalized axioms are dynamically disabled if they turn out to be too
costly, and the traditional axioms are used instead. We refer to
related work for implementation details <cit.>.






§ FEATURES OF 
 

We briefly summarize the general features of that have been
incorporated since its initial version 0.1 <cit.>. Most features were described
in related publications. Additionally, we comment on the
compatibility of the features with the implementation of with generalized axioms (Fig. <ref>) in
.



  
Dependency Schemes. 
Since the initial version 0.1, has been equipped with the
standard dependency scheme <cit.> to
relax the linear quantifier ordering in the prefix of a given PCNF
. In general, dependency
  schemes are used to compute
dependency relations D, which are binary relations over the
set of variables in . If (x,y) ∉D for two
variables x and y then the ordering of x and y in 
can safely be swapped. Otherwise, if (x,y) ∈ D then y is
considered to depend on x. The integration of dependency schemes in
QCDCL results in the following reduction rule, which is added to
and implemented in .

 Let = . be a PCNF and D be a dependency relation computed using a dependency scheme.

    dep-redC ∪{l}C  0.70
    (1) C is a
    clause, l = ∀, 
    (l,l') ∉D  
    for all l' ∈ C with l' = ∃
    or 
     
    (2) C is a
    cube, l = ∃, 
    (l,l') ∉D  
    for all l' ∈ C with l' = ∀


Rule <ref> generalizes the traditional reduction
rule <ref> by the use of dependency relation instead of the
linear ordering of variables (≤_) in the prefix of PCNF
. This way, it might be possible to reduce literals by
rule <ref> which cannot be reduced by
rule <ref>. The soundness of with
rule <ref> has been proved for a dependency relation that
is even more general (and thus allows for additional reductions) than
the one implemented in
 <cit.>. The
generalized axioms <ref> and <ref>
of implemented in are naturally compatible
with rule <ref>. Additionally, dependency schemes enable a
relaxed variant of QCDCL assignments (Definition <ref>)
based on the respective dependency relation rather than the prefix ordering of
a PCNF .



  
Long-Distance Resolution.
The Q-resolution
rule <ref> <cit.> explicitly
disallows to generate clauses (cubes) that are tautological
(contradictory). This restriction is relaxed under certain
side conditions in long-distance (LD)
  Q-resolution <cit.>. LDQ-resolution
was first implemented in the QCDCL solver
 <cit.> and was incorporated in
version 3.0 of . Compared to with traditional
Q-resolution <ref> <cit.>,
with LDQ-resolution is exponentially more powerful in terms
of proof sizes <cit.>. The generalized
axioms <ref> and <ref> implemented
in are not only compatible with the LDQ-resolution
rule, but with any variants of Q-resolution
(cf. <cit.>). Recently, the soundness of
the combination of LDQ-resolution of clauses and dependency schemes in
has been
proved <cit.>,
leaving the soundness of cube resolutions as an open
problem. Therefore, the combination of LDQ-resolution and dependency
schemes is not supported in .




  
Incremental Solving.
Since version 3.0, has been equipped with an API in C and Java
for incremental solving of sequences S := ⟨_0,
…, _n ⟩ of syntactically related PCNFs
_i <cit.>.
Incremental solving aims at reusing the clauses and cubes that were
learned when solving PCNF _i when it comes to solve the
PCNFs _j with i < j.  The API of allows to modify
the PCNFs in S by manipulating the quantifier prefix and adding or
removing sets of clauses in a stack-based way. Since version 4.0, it
is possible to add or remove sets of clauses
arbitrarily <cit.> 
and to extract unsatisfiable cores, 
i.e., unsatisfiable subformulas of the PCNF _i.   
At any time
when solving _i ∈ S, the soundness property of QCDCL
(Section <ref>) that _
and _, where =
_i, must hold. To guarantee that property
when using the generalized axioms for incremental solving,
currently only applies the generalized cube
axiom <ref> with dynamic QBCE used to check
satisfiability of _' in conflict/solution detection
(Fig. <ref>). Although this configuration restricts the power of the
generalized axioms, it has improved incremental solving in the context
of QBF-based conformant planning <cit.>. As it is unclear
how to use dependency schemes effectively in incremental solving,
their application is disabled in .



  
Generation of Proofs and Certificates.
QCDCL solvers can produce clause (cube) resolution proofs of
the unsatisfiability (satisfiability) of PCNFs as a byproduct of
clause (cube) learning. Since
version 1.0 <cit.>, is capable of
producing proofs without employing dependency schemes by
rule <ref>. Given a proof P of a PCNF , a
certificate of  can be extracted from P by
inspecting the reduction steps by rule <ref> in
P <cit.>. A certificate of an
unsatisfiable (satisfiable) PCNF  is given by a set of
Herbrand (Skolem) functions which represent the universal
(existential) variables in . Applications of the
generalized axioms in QCDCL in general impose considerable
restrictions on the certificate extraction process. The
workflow <cit.> to extract a
certificate from P was originally presented for traditional
proofs. If proof P contains clauses (cubes) derived by
rule <ref> (rule <ref>), then P
may lack information needed to extract correct certificates. As a
result, does not support cube resolution proof
generation combined with the generalized cube
axiom <ref>. However, it supports clause resolution
proof generation with the generalized clause
axiom <ref> provided that only propositional
abstractions and SAT solving are used for satisfiability checking in
the side condition of this axiom.



  
Advanced Generation of Learned Clauses and Cubes.
The derivation of a single asserting clause (cube) starting from a falsified
clause (satisfied cube) as implemented in traditional
QCDCL <cit.>
has an exponential worst case <cit.>. Since version 2.0
comes with an approach that avoids this exponential
case <cit.> by a revised selection of clauses
(cubes) to be resolved in learning. This advanced approach is compatible with
all the techniques presented above.






§ EXPERIMENTS
 

We compare variants of , which is the latest
follow-up release of
, to top performing solvers of 
QBFEVAL'16 <cit.>. As benchmarks we consider
all 825 instances from the PCNF track, both in original form
(Table <ref>) and preprocessed by
version 37
(Table <ref>). 
We take preprocessing into account as it might have a positive impact
on certain solvers while a negative on
others (cf. <cit.>). 
Experiments were run on an AMD Opteron
6238 processor (2.6 GHz) under 64-bit Ubuntu Linux 12.04 with time and
memory limits of 1800 seconds and seven GB. Exceeding the memory limit
is counted as a time out.[We refer to the appendix of this paper with
  additional experimental results.]







To assess the impact of
the generalized axioms <ref> and <ref> on the performance, we consider using
both <ref> and <ref> (variant in the
tables), without <ref> (), without  
<ref> (), and using no generalized
axioms at all (). 

On original instances (Table <ref>),
outperforms variants ,
, and with restricted or without 
generalized axioms, respectively. Variant
without axiom <ref> outperforms
variant without <ref>. We
attribute this effect to the use of dynamic
QBCE (among other techniques) for applications of the cube axiom
<ref> in . 
Compared to , disabling
only dynamic QBCE in variant severely impacts performance.  

On preprocessed instances (Table <ref>),
we make similar observations regarding the impact of the generalized
axioms like in Table <ref>.  However,
variant without the clause axiom
<ref> is on par with  
. Preprocessing may blur the structure of an instance. We
conjecture that this blurring
hinders the success of the QBF decision procedures in
, on which applications of the generalized axioms are based. 
In general the performance
difference between the variants of
is smaller than on original instances. The rankings of the
solvers  <cit.>,  <cit.>, and  <cit.> are
improved substantially by preprocessing, whereas those of  <cit.>
and  <cit.> become worse. The best variant in Table <ref> ranks fourth behind  <cit.>,
, and
. However, the lag to the
solver ranked third is 19 instances compared to 120 instances
for the best variant in
Table <ref> that also ranks fourth.

To analyze the effects of preprocessing in more detail, we filtered the 825
PCNFs from QBFEVAL'16 by discarding 354 PCNFs that are already solved by
and 69 PCNFs where eliminated all universally quantified
variables, resulting in a set of 402 PCNFs. Further, we considered the 402
PCNFs in their original form and preprocessed by and partitioned them
into subsets containing PCNFs with at most two and with three or more
quantifier alternations. Such partitioning is motivated by a related
experimental study <cit.> where a large
diversity of solver performance was observed on instance classes defined by
alternations. Tables <ref>
and <ref> show solver performance on these
subsets without and with preprocessing, respectively. Notably, variants of
outperform the other solvers on the subsets with three or more
alternations, both without and with preprocessing
(Tables <ref>
and <ref>). 

All variants of reported above apply dependency-aware reduction by
rule <ref>.  Variant is the same as
(including generalized axioms) but uses the traditional reduction
rule <ref> based on the linear quantifier ordering of PCNFs.  Variant
outperforms in all tables
except Table <ref>, where is on par, which illustrates the benefits of dependency schemes in
QCDCL. Variant differs from in the
use of LDQ-resolution in learning instead of traditional Q-resolution by
rule <ref>. The results with LDQ-resolution are mixed, despite being
a stronger proof system than Q-resolution. Variant
outperforms in all tables
except Tables <ref>
and <ref>, i.e., on instances with at
most two quantifier alternations.






§ CONCLUSION


We presented the latest major release 
version 6.0 of the QCDCL solver . implements a
variant of QCDCL that is based on a generalization of the Q-resolution
calculus (). The generalization is achieved by equipping
with generalized clause and cube axioms to be used in 
clause and cube learning <cit.>. The generalized
axioms provide an extensible framework of 
interfaces for the integration of arbitrary QBF proof systems in
, and hence in QCDCL. The integration of proof systems
orthogonal to Q-resolution, such as variable expansion, enables QCDCL
to potentially produce proofs that are exponentially shorter than
proofs produced by traditional QCDCL. This way, the state of the art 
of QCDCL solving can be further advanced. A related open
problem is the inability of plain QCDCL to exploit the full power of
Q-resolution <cit.>.

The workflow of QCDCL with generalized axioms is not tailored towards
but can be implemented in any QCDCL
solver. Furthermore, it is compatible with dependency
schemes <cit.>
and any Q-resolution variant <cit.>,
which offers potential for further improvements.

Experiments with variants of showed considerable
performance gains due to the application of generalized axioms. However,
frequent applications are hindered by computationally expensive QBF
satisfiability checks in the side conditions of the axioms. To limit the
checking overhead, axiom applications must be carefully scheduled.
In this respect, there is room for improvements in fine tuning
. Further, it may be beneficial 
to integrate the QBF decision procedures that are
applied to satisfiability checking more tightly in the QCDCL workflow, like
with dynamic blocked clause elimination (QBCE) <cit.>.



10



DBLP:conf/fmcad/AyariB02
Ayari, A., Basin, D.A.: QUBOS: Deciding Quantified Boolean Logic Using
  Propositional Satisfiability Solvers. In: FMCAD. LNCS, vol. 2517, pp.
  187–201. Springer (2002)

DBLP:journals/fmsd/BalabanovJ12
Balabanov, V., Jiang, J.R.: Unified QBF Certification and its Applications.
  Formal Methods in System Design  41(1),  45–65 (2012)

DBLP:conf/sat/BalabanovWJ14
Balabanov, V., Widl, M., Jiang, J.R.: QBF Resolution Systems and Their Proof
  Complexities. In: SAT. LNCS, vol. 8561, pp. 154–169. Springer (2014)

DBLP:conf/cp/BeyersdorffB16
Beyersdorff, O., Blinkhorn, J.: Dependency Schemes in QBF Calculi: Semantics
  and Soundness. In: CP. LNCS, vol. 9892, pp. 96–112. Springer (2016)

beyersdorff_et_al:LIPIcs:2015:4905
Beyersdorff, O., Chew, L., Janota, M.: Proof Complexity of Resolution-based
  QBF Calculi. In: STACS. LIPIcs, vol. 30, pp. 76–89. Schloss
  Dagstuhl–Leibniz-Zentrum fuer Informatik (2015)

DBLP:conf/sat/Biere04a
Biere, A.: Resolve and Expand. In: SAT. LNCS, vol. 3542, pp. 59–70. Springer
  (2004)

DBLP:conf/sat/0001JT16
Bogaerts, B., Janhunen, T., Tasharrofi, S.: SAT-to-SAT in QBFEval 2016. In:
  QBF Workshop. CEUR Workshop Proceedings, vol. 1719, pp. 63–70.
  CEUR-WS.org (2016)

DBLP:conf/sat/BubeckB07
Bubeck, U., Kleine Büning, H.: Bounded Universal Expansion for
  Preprocessing QBF. In: SAT. LNCS, vol. 4501, pp. 244–257. Springer (2007)

DBLP:conf/aaai/CadoliGS98
Cadoli, M., Giovanardi, A., Schaerf, M.: An Algorithm to Evaluate Quantified
  Boolean Formulae. In: AAAI. pp. 262–267. AAAI Press / The MIT Press
  (1998)

DBLP:journals/jacm/ClarkeGJLV03
Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-Guided
  Abstraction Refinement for Symbolic Model Checking. J. ACM  50(5),
  752–794 (2003)

DBLP:journals/cacm/DavisLL62
Davis, M., Logemann, G., Loveland, D.W.: A Machine Program for
  Theorem-Proving. Commun. ACM  5(7),  394–397 (1962)

DBLP:journals/amai/EglyKLP17
Egly, U., Kronegger, M., Lonsing, F., Pfandler, A.: Conformant Planning as a
  Case Study of Incremental QBF Solving. Ann. Math. Artif. Intell.  80(1),
  21–45 (2017)

DBLP:conf/lpar/EglyLW13
Egly, U., Lonsing, F., Widl, M.: Long-Distance Resolution: Proof Generation
  and Strategy Extraction in Search-Based QBF Solving. In: LPAR. LNCS,
  vol. 8312, pp. 291–308. Springer (2013)

DBLP:journals/jair/GiunchigliaNT06
Giunchiglia, E., Narizzano, M., Tacchella, A.: Clause/Term Resolution and
  Learning in the Evaluation of Quantified Boolean Formulas. JAIR  26,
  371–416 (2006)

DBLP:journals/jair/HeuleJLSB15
Heule, M., Järvisalo, M., Lonsing, F., Seidl, M., Biere, A.: Clause
  Elimination for SAT and QSAT. JAIR  53,  127–168 (2015)

DBLP:conf/sat/Janota16
Janota, M.: On Q-Resolution and CDCL QBF Solving. In: SAT. LNCS, vol.
  9710, pp. 402–418. Springer (2016)

Janota20161
Janota, M., Klieber, W., Marques-Silva, J., Clarke, E.: Solving QBF with
  Counterexample Guided Refinement. Artif. Intell.  234,  1–25 (2016)

DBLP:journals/tcs/JanotaM15
Janota, M., Marques-Silva, J.: Expansion-Based QBF Solving versus
  Q-Resolution. Theor. Comput. Sci.  577,  25–42 (2015)

DBLP:conf/ijcai/JanotaM15
Janota, M., Marques-Silva, J.: Solving QBF by Clause Selection. In:
  IJCAI. pp. 325–331. AAAI Press (2015)

DBLP:series/faia/BuningB09
Kleine Büning, H., Bubeck, U.: Theory of Quantified Boolean Formulas.
  In: Handbook of Satisfiability, FAIA, vol. 185, pp. 735–760. IOS Press
  (2009)

DBLP:journals/iandc/BuningKF95
Kleine Büning, H., Karpinski, M., Flögel, A.: Resolution for
  Quantified Boolean Formulas. Inf. Comput.  117(1),  12–18 (1995)

DBLP:conf/sat/KlieberSGC10
Klieber, W., Sapra, S., Gao, S., Clarke, E.M.: A Non-Prenex, Non-Clausal QBF
  Solver with Game-State Learning. In: SAT. LNCS, vol. 6175, pp. 128–142.
  Springer (2010)

DBLP:journals/dam/Kullmann99
Kullmann, O.: On a Generalization of Extended Resolution. Discrete Applied
  Mathematics  96-97,  149–176 (1999)

DBLP:conf/tableaux/Letz02
Letz, R.: Lemma and Model Caching in Decision Procedures for Quantified
  Boolean Formulas. In: TABLEAUX. LNCS, vol. 2381, pp. 160–175. Springer
  (2002)

DBLP:conf/lpar/LonsingBBES15
Lonsing, F., Bacchus, F., Biere, A., Egly, U., Seidl, M.: Enhancing
  Search-Based QBF Solving by Dynamic Blocked Clause Elimination. In: LPAR.
  LNCS, vol. 9450, pp. 418–433. Springer (2015)

DBLP:journals/jsat/LonsingB10
Lonsing, F., Biere, A.: DepQBF: A Dependency-Aware QBF Solver. JSAT
  7(2-3),  71–76 (2010)

DBLP:conf/sat/LonsingB10
Lonsing, F., Biere, A.: Integrating Dependency Schemes in Search-Based QBF
  Solvers. In: SAT. LNCS, vol. 6175, pp. 158–171. Springer (2010)

DBLP:conf/cp/LonsingE14
Lonsing, F., Egly, U.: Incremental QBF Solving. In: CP. LNCS, vol. 8656,
  pp. 514–530. Springer (2014)

DBLP:conf/sat/LonsingE15
Lonsing, F., Egly, U.: Incrementally Computing Minimal Unsatisfiable Cores of
  QBFs via a Clause Group Solver API. In: SAT. LNCS, vol. 9340, pp.
  191–198. Springer (2015)

DBLP:journals/corr/LonsingE17
Lonsing, F., Egly, U.: Evaluating QBF Solvers: Quantifier Alternations
  Matter. CoRR  abs/1701.06612 (2017), <http://arxiv.org/abs/1701.06612>,
  technical report

DBLP:conf/sat/LonsingES16
Lonsing, F., Egly, U., Seidl, M.: Q-Resolution with Generalized Axioms. In:
  SAT. LNCS, vol. 9710, pp. 435–452. Springer (2016)

DBLP:conf/sat/LonsingEG13
Lonsing, F., Egly, U., Van Gelder, A.: Efficient Clause Learning for
  Quantified Boolean Formulas via QBF Pseudo Unit Propagation. In: SAT.
  LNCS, vol. 7962, pp. 100–115. Springer (2013)

Lonsing201692
Lonsing, F., Seidl, M., Van Gelder, A.: The QBF Gallery: Behind the Scenes.
  Artif. Intell.  237,  92–114 (2016)

DBLP:conf/date/MarinMLB12
Marin, P., Miller, C., Lewis, M.D.T., Becker, B.: Verification of Partial
  Designs Using Incremental QBF Solving. In: DATE. pp. 623–628. IEEE
  (2012)

DBLP:journals/fuin/MarinNPTG16
Marin, P., Narizzano, M., Pulina, L., Tacchella, A., Giunchiglia, E.: Twelve
  Years of QBF Evaluations: QSAT Is PSPACE-Hard and It Shows. Fundam. Inform.
  149(1-2),  133–158 (2016)

DBLP:conf/sat/NiemetzPLSB12
Niemetz, A., Preiner, M., Lonsing, F., Seidl, M., Biere, A.: Resolution-Based
  Certificate Extraction for QBF - (Tool Presentation). In: SAT. LNCS,
  vol. 7317, pp. 430–435. Springer (2012)

DBLP:conf/sat/PeitlSS16
Peitl, T., Slivovsky, F., Szeider, S.: Long Distance Q-Resolution with
  Dependency Schemes. In: SAT. LNCS, vol. 9710, pp. 500–518. Springer
  (2016)

DBLP:conf/sat/Pulina16
Pulina, L.: The Ninth QBF Solvers Evaluation - Preliminary Report. In:
  Proceedings of the 4th International Workshop on Quantified Boolean Formulas
  QBF 2016. CEUR Workshop Proceedings, vol. 1719, pp. 1–13. CEUR-WS.org
  (2016)

DBLP:conf/fmcad/RabeT15
Rabe, M.N., Tentrup, L.: CAQE: A Certifying QBF Solver. In: FMCAD. pp.
  136–143. IEEE (2015)

DBLP:journals/jacm/Robinson65
Robinson, J.A.: A Machine-Oriented Logic Based on the Resolution Principle.
  J. ACM  12(1),  23–41 (1965)

DBLP:journals/jar/SamerS09
Samer, M., Szeider, S.: Backdoor Sets of Quantified Boolean Formulas. JAR
  42(1),  77–97 (2009)

DBLP:conf/sat/SchollP16
Scholl, C., Pigorsch, F.: The QBF Solver AIGSolve. In: QBF Workshop. CEUR
  Workshop Proceedings, vol. 1719, pp. 55–62. CEUR-WS.org (2016)

DBLP:series/faia/SilvaLM09
Silva, J.P.M., Lynce, I., Malik, S.: Conflict-Driven Clause Learning SAT
  Solvers. In: Handbook of Satisfiability, FAIA, vol. 185, pp. 131–153. IOS
  Press (2009)

DBLP:conf/sat/SlivovskyS12
Slivovsky, F., Szeider, S.: Computing Resolution-Path Dependencies in Linear
  Time. In: SAT. LNCS, vol. 7317, pp. 58–71. Springer (2012)

DBLP:journals/tcs/SlivovskyS16
Slivovsky, F., Szeider, S.: Soundness of Q-Resolution with Dependency
  Schemes. Theor. Comput. Sci.  612,  83–101 (2016)

DBLP:conf/cp/Gelder11
Van Gelder, A.: Variable Independence and Resolution Paths for Quantified
  Boolean Formulas. In: CP. LNCS, vol. 6876, pp. 789–803. Springer (2011)

DBLP:conf/cp/Gelder12
Van Gelder, A.: Contributions to the Theory of Practical Quantified Boolean
  Formula Solving. In: CP. LNCS, vol. 7514, pp. 647–663. Springer (2012)

DBLP:conf/iccad/ZhangM02
Zhang, L., Malik, S.: Conflict Driven Learning in a Quantified Boolean
  Satisfiability Solver. In: ICCAD. pp. 442–449. ACM / IEEE Computer
  Society (2002)

DBLP:conf/cp/ZhangM02
Zhang, L., Malik, S.: Towards a Symmetric Treatment of Satisfaction and
  Conflicts in Quantified Boolean Formula Evaluation. In: CP. LNCS, vol. 2470,
  pp. 200–215. Springer (2002)











§ ADDITIONAL EXPERIMENTAL DATA








