On Expansion and Resolution in CEGAR Based QBF Solving
Leander Tentrup

 




Saarland University, Saarbrücken, Germany
tentrup@react.uni-saarland.de

On Expansion and Resolution in CEGAR Based QBF SolvingSupported by the European Research Council (ERC) Grant OSARES (No. 683300).
    Leander Tentrup
    Accepted, Received
=================================================================================================================================




A quantified Boolean formula (QBF) is a propositional formula extended with universal and existential quantification over propositions.
There are two methodologies in CEGAR based QBF solving techniques, one that is based on a refinement loop that builds partial expansions and a more recent one that is based on the communication of satisfied clauses.
Despite their algorithmic similarity, their performance characteristics in experimental evaluations are very different and in many cases orthogonal.
We compare those CEGAR approaches using proof theory developed around QBF solving and present a unified calculus that combines the strength of both approaches.
Lastly, we implement the new calculus and confirm experimentally that the theoretical improvements lead to improved performance.




§ INTRODUCTION


Efficient solving techniques for Boolean theories are an integral part of modern verification and synthesis methods.
Especially in synthesis, the amount of choice in the solution space leads to propositional problems of enormous size.
Quantified Boolean formulas (QBFs) have repeatedly been considered as a candidate theory for synthesis approaches <cit.> and recent advances in QBF solvers give rise to hope that QBF may help to increase the scalability of those approaches.

Solving quantified Boolean formulas (QBF) using partial expansions in a counterexample guided abstraction and refinement (CEGAR) loop <cit.> has proven to be very successful.
From its introduction, the corresponding solver  won several QBF competitions.
In recent work, a different kind of CEGAR algorithms have been proposed <cit.>, implemented in the solvers  and .
All those CEGAR approaches share algorithmic similarities like working recursively over the structure of the quantifier prefix and using SAT solver to enumerate candidate solutions.
However, instead of using partial expansions of the QBF as  does, newer approaches base their refinements on whether a set of clauses is satisfied or not.
Despite those algorithmic similarities, the performance characteristics of the resulting solver in experimental evaluations are very different and in many cases orthogonal: While  tends to perform best on instances with a low number of quantifier alternations,  and  have an advantage in instances with many alternations <cit.>.

Proof theory has been repeatedly used to improve the understanding of different solving techniques.
For example, the proof calculus  <cit.> has been developed to characterize aspects of expansion-based solving.
In this paper, we introduce a new calculus  that corresponds to the clausal-based CEGAR approaches <cit.>.
The levelized nature of those algorithms are reflected by the rules of this calculus, universal reduction and propositional resolution, which are applied to blocks of quantifiers.
We show that this calculus is inherently different to  explaining the empirical performance results.
In detail, we show that  polynomial simulates level-ordered .
We also discuss an extension to  that was already proposed as solving optimizations <cit.> and show that this extension makes the resulting calculus exponential more concise.

Further, we integrate the  calculus as a rule that can be used within the  calculus, leading to a unified proof calculus for all current CEGAR approaches.
We show that the unified calculus is exponential stronger than both  and , as well as just applying both simultaneously.
This unified calculus serves as a base for implementing an expansion refinement in the QBF solver .
On standard benchmark sets, the combined approach leads to a significant empirical improvement over the previous implementation.




§ PRELIMINARIES




 §.§ Quantified Boolean Formulas


We consider quantified Boolean formulas in prenex conjunctive normal form (PCNF), that is a formula consisting of a linear and consecutive quantifier prefix as well as a propositional matrix.
A matrix is a set of clauses, and a clause is a disjunctive combination of literals l, that is either a variable or its negation.

Given a clause C = (l_1  l_2 … l_n), we use set notation interchangeably, that is C is also represented by the set l_1,l_2,…,l_n.
Furthermore, we use standard set operations, such as union and intersection, to work with clauses.

For readability, we lift the quantification over variables to the quantification over sets of variables and denote a maximal consecutive block of quantifiers of the same type ∀ x_1∀ x_2⋯∀ x_nφ by ∀ Xφ and ∃ x_1∃ x_2⋯∃ x_nφ by ∃ Xφ, accordingly, where X=x_1,…,x_n. 

Given a set of variables X, an assignment of X is a function α : X → that maps each variable x ∈ X to either true () or false ().
When the domain of α is not clear from context, we write α_X.
We use the instantiation of a QBF Φ by assignment α, written Φ[α] which removes quantification over variables in (α) and replaces occurrences of x ∈(α) by α(x).
We write αφ if the assignment α satisfies a propositional formula φ, i.e., φ[α] ≡.




 §.§ Resolution


Propositional resolution is a well-known method for refuting propositional formulas in conjunctive normal form (CNF).
The resolution rule allows to merge two clauses that contain the same variable, but in opposite signs.

    [res]C ∪ C'C ∪l    C' ∪l

A resolution proof π is a series of applications of the resolution rule.
A propositional formula is unsatisfiable if there is a resolution proof that derives the empty clause.
We visualize resolution proofs by a graph where the nodes with indegree 0 are called the leaves and the unique node with outdegree 0 is called the root.
We depict the graph representation of a resolution proof in Fig. <ref>fig:resolution-example.
The size of a resolution proof is the number of nodes in the graph.





 §.§ Proof Systems


We consider proof systems that are able to refute quantified Boolean formulas.
To enable comparison between proof systems, one uses the concept of polynomial simulation.
A proof system P polynomially simulates (p-simulates) P' if there is a polynomial p such that for every number n and every formula Φ it holds that if there is a proof of Φ in P' of size n, then there is a proof of Φ in P whose size is less than p(n).
We call P and P' polynomial equivalent, if P' additionally p-simulates P.

A refutation based calculus (such as resolution) is regarded as a proof system because it can refute the negation of a formula.

Figure <ref> gives an overview over the proof systems introduced in this paper and their relation.
An edge P → P' means that P p-simulates P' (transitive edges are omitted).
A dashed line indicates incomparability results.






§ PROOF CALCULI


Given a PCNF formula X_1 … X_n ⋀_1 ≤ i ≤ m C_i.
We define a function (i, k) that returns the literals of clause C_i that are bound at quantifier level k (1 ≤ k ≤ n).
Further, we generalize this definition to (i, > k) and (i, < k) that return the literals bound after (before) level k.
We define (i, 0) = (i, n+1) = ∅ for every 1 ≤ i ≤ m.
We use 𝒞 to denote a set of clauses and Q_k ∈∃,∀ to denote the quantification type of level k.



 §.§ A Proof System for Clausal Abstractions


We start by defining the object on which our proof system  is based on.
A proof object ^k consists of a set of indices  where an index i ∈ represents the i-th clause in the original matrix and k denotes the k-th level of the quantifier hierarchy.
We define an operation (^k) = ⋃_i ∈(i, k), that gives access to the literals of clauses contained in ^k.
The leaves in our proof system are singleton sets i^z where z is the maximum quantification level of all literals in clause C_i.
The root of a refutation proof is the proof object ^0 that represents the empty set, i.e., (^0) = ∅.

The rules of the proof system is given in Fig. <ref>.
It consists of three rules, an axiom rule () that generates leaves, a resolution rule (), and a universal reduction rule ().
The latter two rules enable to transform a premise that is related to quantifier level k into a conclusion that is related to quantifier level k-1.
The universal reduction rule and the resolution rule are used for universal and existential quantifier blocks, respectively.





  
Resolution rule.
There is a close connection between () and the propositional resolution as () merges a number of proof objects _i^k of level k into a single proof object of level k-1.
It does so by using a resolution proof for a propositional formula that is constructed from the premises _i^k.
This propositional formula ⋀_1 ≤ i ≤ j(_i^k) contains only literals of level k.
Intuitively, this rule can be interpreted as follows: a resolution proof over those clauses rules out any possible existential assignment at quantifier level k, thus, one of those clauses has to be satisfied at an earlier level.



  
Universal reduction rule.
In contrast to (), () works on single proof objects.
It can be applied if level k is universal and the premise does not encode a universal tautology, i.e., for every literal l ∈(^k), the negated literal l is not contained in (^k).



  
Graph representation.
A proof in the  calculus can be represented as a directed acyclic graph (DAG).
The nodes in the DAG are proof objects ^k and the edges represent applications of () and ().
The rule () is represented by a hyper-edge that is labeled with the propositional resolution proof π.
Edges representing the universal reduction can thus remain unlabeled without introducing ambiguity.
The size of a  proof is the number of nodes in the graph together with the number of inner (non-leaf, non-root) nodes of the containing propositional resolution proofs.


A refutation in the  calculus is a proof that derives a proof object ^0 at level 0.
A proof for some ^k is a  proof with root ^k.
Thus, a proof for ^k can be also viewed as a refutation for the formula X_k+1… X_n ⋀_i ∈(i,>k) starting with quantifier level k+1 and containing clauses represented by .

 
  Consider the following QBF
  
    ∃ e_1_1 ∀ u_1_2 ∃ c_1, c_2_3 
        ( e_1  c_1_C_1 )
        ( u_1  c_1_C_2 )
        ( e_1  c_2_C_3 )
        ( u_1  c_2_C_4 )
        ( c_1 c_2_C_5 ) .

  
  The refutation in the  calculus is given in Fig. <ref>.
  In the nodes, we represent the proof objects ^k in the first component and the represented clause in the second component.
  The proof follows the structure of the quantifier prefix, i.e., it needs four levels to derive a refutation.
  The resolution proof π_1 for propositional formula
  
    (1^3) (4^3) (5^3)
        ≡ (c_1)(c_2)(c_1 c_2)

  is depicted in Fig. <ref>fig:resolution-example.
  
  


In the following, we give a formal correctness argument and compare our calculus to established proof systems.
A QBF proof system is sound if deriving a proof implies that the QBF is false and it is refutational complete if every false QBF has a proof.

 
   is sound and refutational complete for QBF.


  
  The completeness proof is carried out by induction over the quantifier prefix.
  
  Induction base.
  Let ∃ X φ be a false QBF and φ be propositional.
  Then () derives some ^0 because resolution is complete for propositional formulas.
  Let ∀ X φ be a false QBF and φ be propositional.
  Picking an arbitrary (non-tautological) clause C_i and applying () leads to i^0.
  
  Induction step.
  Let ∃ X Φ be a false QBF, i.e., for all assignments _X the QBF Φ[_X] is false.
  Hence, by induction hypothesis, there exists a  proof for every Φ[_X].
  We transform those proofs in a way that they can be used to build a proof for Φ.
  Let P be a proof of Φ[_X].
  P has a distinct root node (representing the empty set), that was derived using () as Φ[_X] starts with a universal quantifier.
  To embed P in Φ, we increment every level in P by one, as Φ has one additional (existential) quantifier level.
  Then, instead of deriving the empty set, the former root node derives a proof object of the form ^1.
  Let N be the set of those former root nodes.
  By construction, there exists a resolution proof π such that the empty set can be derived by () using N (or a subset thereof).
  Assuming otherwise leads to the contradiction that some Φ[_X] is true.
  
  Let ∀ X Φ be a false QBF, i.e., there is an assignment _X such that the QBF Φ[_X] is false.
  Hence, by induction hypothesis, there exists a  proof for Φ[_X].
  Applying () using _X is a  proof for Φ.
  
  
  For soundness it is enough to show that one cannot derive a clause using this calculus that changes the satisfiability.
  Let Φ =  X_1 … X_n ⋀_1 ≤ i ≤ m C_i be an arbitrary QBF.
  For every level k and every ^k generated by the application of the  calculus, it holds that Φ and X_1 … X_n ⋀_1 ≤ i ≤ m C_i  (⋁_i ∈⋁_l ∈(i, ≤ k) l) are equisatisfiable.
  Assume otherwise, then either () or () have derived a ^k that would make Φ false.
  Again, by induction, one can show that if () derived a ^k that makes Φ false, the original premise ^k+1 would have made Φ false; likewise, if () derived a ^k that makes Φ false, the conjunction of the premises have made Φ false.
  




  
Comparison to  calculus.
 <cit.> is an extension of the (propositional) resolution rule to handle universal quantification.
The universal reduction rule allows the removal of universal literal u from a clause C if no existential literal l ∈ C depends on u.
There are also additional rules on when the resolution rule can be applied, i.e., it is not allowed to produce tautology clauses using the resolution rule.
The definitions of Q-resolution proof and refutation are analogous to the propositional case.

There are two restricted classes of  that are commonly considered, that is level-ordered and tree-like .
A  proof is level-ordered if resolution of an existential literal l at level k happens before every other existential literal with level < k.
A  proof is tree-like if the graph representing the proof has a tree shape.

As a first result, we show that  is polynomially equivalent to level-ordered , i.e., a proof in our calculus can be polynomially simulated in level-ordered  and vice versa.
While this is straightforward from the definitions of both calculi, this is much less obvious if one looks at the underlying algorithms of the CEGAR approaches <cit.> and QCDCL <cit.>.

 
   and level-ordered  are p-sim. equivalent.


  A  proof can be transformed into a Q-resolution proof by replacing every node ^k by the clause (⋁_i ∈⋁_l ∈(i, ≤ k) l) and by replacing the hyper-edge labeled with π by a graph representing the applications of the resolution rule.
  Similarly, a level-ordered Q-resolution proof can be transformed into a  proof by a step-wise transformation from leaves to the root.
  This way, one can track the clauses needed for constructing the proof objects ^k at every level k.
  

Despite being equally powerful, the differences are important and enable the expansion based extension that we will introduce in the next section.
One difference is that our calculus only reasons about literals of one quantifier level, which allows us to use plain resolution without any changes (as are needed in ).
Further, the proof rules capture the fact that only proof obligations are communicated between the quantifier levels of the QBF.
An immediate consequence is that every refutation in the proof system is DAG-like and has exactly depth k+1.

Since the level-ordering constraint imposes an order on the resolution, the size of the refutation proof may be exponentially larger for some formulas <cit.>.
Hence, also  is in general exponentially weaker than unrestricted .
In practice, and already noted by Janota and Marques-Silva <cit.>, solvers that are based on  proofs produce level-ordered .

In the initial version of  <cit.> an optimization that can generate new resolvents at level k without recursion into deeper levels was described.
We model this optimization as a new rule extending the  calculus and show that this rule leads to an exponential separation.



  
Strong UNSAT Rule.

In the implementation of , we used an optimization which we called strong UNSAT refinement <cit.>, that allowed the solver to strengthen a certain type of refinements.
The basic idea behind this optimization is that if the solver determines that, at an existential level k, a certain set of clauses 𝒞 cannot be satisfied at the same time, then every alternative set of clauses 𝒞', that is equivalent with respect to the literals in levels >k, cannot be satisfied as well.
We introduce the following proof rule that formalizes this intuition.
We extend proof objects ^k such that they can additionally contain fresh literals, i.e., literals that were not part of the original QBF.
Those literals are treated as they were bound at level k, i.e., they are contained in (^k) and can thus be used in the premise of the rule (), but are not contained in the conclusion ^k-1.


0.7
  [strengthen]
    (a∪)^k   a, j_1^k   ⋯  a, j_n^k(∪ i )^k

0.3
    Q_k = ∃,

    (j,>k) ⊆(i,>k) for all j ∈j_1,…,j_n,

    a fresh var.





  The strengthening rule is sound.


  In a resolution proof at level k, one can derive the proof objects (∪j)^k for j ∈j_1,…,j_n using the conclusion of the strengthening rule.
  Assume we have a proof for (∪i)^k (premise), then the quantified formula ∀ X_k+1… X_n ⋀_i^* ∈(i^*,>k) (i,>k) is false.
  Thus, the QBF with the same quantifier prefix and matrix, extended by some clause (j,>k) for j ∈j_1,…,j_n, is still false.
  Since every C_j subsumes C_i with respect to quantifier level greater than k ((j,>k) ⊆(i,>k)), the clause (i,>k) can be eliminated without changing satisfiability.
  Thus, the resulting quantified formula ∀ X_k+1… X_n ⋀_i^* ∈(i^*,>k) (j,>k) is false and there exists a  proof for (∪j)^k.
  

 
  The proof system without strengthening rule does not p-simulate the proof system with strengthening rule.


  We use the family of formulas  that was used to show that level-ordered  cannot p-simulate  <cit.>.
  We show that  has a polynomial refutation in the  calculus with strengthening rule, but has only exponential refutations without it.
  The latter follows from Theorem <ref> and the results by Janota and Marques-Silva <cit.>.
  
  The formula  has the quantifier prefix ∃ x_11… x_nn∀ z ∃ a_1 … a_n b_1 … b_n and the matrix is given by
  
    ( ⋁_i ∈ 1..na_i ) ( ⋁_i ∈ 1..nb_i ) ⋀_i,j ∈ 1..n(x_ij z  a_i)_C_ij(x_ijz b_j)_C_ij

  
  One can interpret the constraints as selecting rows and columns in a matrix where i selects the row and j selects the column, e.g., for n=3 it can be visualized as follows:
  
    [ x_11 z  a_1   x_11z b_1 x_12 z  a_1   x_12z b_2 x_13 z  a_1   x_13z b_3; x_21 z  a_2   x_21z b_1 x_22 z  a_2   x_22z b_2 x_23 z  a_2   x_23z b_3; x_31 z  a_3   x_31z b_1 x_32 z  a_3   x_32z b_2 x_33 z  a_3   x_33z b_3;             ]

  Assume z → 0, then we derive the proof object ^1 = i1 | i ∈ 1..n^1 ((^1) = ⋁_i ∈ 1..n x_i1) by applying the resolution and reduction rule.
  Likewise, for z → 1, we derive the proof object _0^1 = 1j| j ∈ 1..n ^1 ((_0^1) = ⋁_j ∈ 1..nx_1j).

  Applying the strengthening rule on _0^1 results in _1^1 = (c_1∪1j| j ∈ 2..n)^1 and c_1, 11^1, c_1, 21^1, …, c_1, n1^1 where c_1 is a fresh variable.
  Further n-1 applications of the strengthening rule starting on _1^1 lead to _n^1 =  c_j | j ∈ 1..n ^1 and the proof objects c_j, ij| i,j ∈ 1..n^1,
  where c_j are fresh variables, as all clauses in a column are equivalent with respect to the inner quantifiers (contain z b_j).
  
  Using ^1 and c_1, 11^1, c_1, 21^1, …, c_1, n1^1 from the first strengthening application, we derive the singleton set c_1 using n resolution steps ((^1) = ⋁_i ∈ 1..n x_i1 and (c_1, i1^1) = c_1, x_i1).
  Analogously, one derives the singletons c_2…c_n and together with _n^1 =  c_j | j ∈ 1..n the empty set is derived.
  Thus, there exists a polyonomial resolution proof leading to a proof object ^0 and the size of the overall proof is polynomial, too.
  

We note that despite being stronger than plain , the extended calculus is still incomparable to .
 
   with strengthening rule does not p-simulate .


  We use a modification of formula  (<ref>), which we call ' in the following.
  The single universal variable z is replaced by a number of variables z_ij for every pair i,j ∈ 1..N.
  It follows that the strengthening rule is never applicable and hence, the proof system is as strong as level-ordered  which has an exponential refutation of  while  has a polynomial refutation since the expansion tree has still only two branches <cit.>.
  

When compared to , the strengthening rule can be interpreted as a step towards breaking the level-ordered constraint inherent to .
The calculus, however, is not as strong as .
 
   with strengthening rule does not p-sim. .


	The formula ' from the previous proof has a polynomial (tree-like)  proof.
	The proof for  given by Mahajan and Shukla <cit.> can be modified for '.
	
Both results follow from the fact that the strengthening rule as presented is not applicable to the formula '.
Where in , the clauses C_ij are equal with respect to the inner quantifier when j is fixed (z b_j), in ' they are all different (z_ij b_j).
This difference is only due to the universal variables z_ij.
Thus, we propose a stronger version of the strengthening rule that does the subset check only on the existential variables.
For the universal literals, one additionally has to make sure that no resolvent produces a tautology (as it is the case in ').
We leave the formalization to future work.




 §.§ Expansion
 

The levelized nature of the proof system allows us to introduce additional rules that can reason about quantified subformulas.
In the following, we introduce such a rule that allows us to use the  calculus <cit.> within a  proof.

We start by giving necessary notations used to define .
We refer the reader to <cit.> for further information.


  
  * A ∀-expansion tree for QBF Φ with u universal quantifier blocks is a rooted tree  such that every path p_0  p_1 ⋯ p_u in  from the root p_0 to some leaf p_u has exactly u edges and each edge p_i-1 p_i is labeled with a total assignment α_u to the universal variables at universal level u. Each path in  is uniquely defined by its labeling.
  
  * Let  be a ∀-expansion tree and P = p_0  p_1 ⋯ p_u be a path from the root p_0 to some leaf p_u.
    
      
  * For an existential variable x we define (P,x) = x^ where x^ is a fresh variable and  is the universal assignment of the dependencies of x.
      
  * For a propositional formula φ define (P,φ) as instantiating φ with α_1,…,α_u and replacing every existential variable x by (P,x).
      
  * Define (,Φ) as the conjunction of all (P,φ) for each root-to-leaf P in .
    


In contrast to previous work, we allow to use the expansion rule on quantified subformulas of Φ additionally to applying it to Φ directly.
By 𝒞^≥ k we denote a set of clauses that only contain literals bound at level ≥ k.

    []
      ^k-1   𝒞^≥ k   π       [c]0.8Q_k = ∃, π is a resolution refutation of the expansion
    
      formula (, ∃ X_k ∀ X_k+1…∃ X_m 𝒞^≥ k)
    ^k-1 = i | C_i ∈𝒞^k-1

The rule states that if there is a universal expansion of the quantified Boolean formula ∃ X_k ∀ X_k+1…∃ X_m 𝒞^≥ k and a resolution refutation π for this expansion, then there is no existential assignment that satisfies clauses 𝒞 from level k.
The size of the expansion rule is the sum of the size of the expansion tree and resolution proof <cit.>.

 
  We demonstrate the interplay between () and the  calculus on the following formula
  
    ∃ e_1 ^1 ∀ u_1 ^2 ∃ c_1, c_2 ^3 ∀ a ^4 ∃ b ∃ x ^5 ∀ z ^6 ∃ t ^7 
     (e_1  c_1) _1
         (u_1  c_1) _2
         (e_1  c_2) _3
         (u_1  c_2) _4
         (c_1 c_2 ba) _5
         (z  t  b)  _6
         (zt)  _7
         (x t)  _8
         (x t)  _9

  
  To apply (), we use the clauses 5–9 from quantifier level 5, i.e., 𝒞^≥ 5 = 
    (b)
    (z  t  b)
    (zt)
    (x t)
    (x t).
  The corresponding quantifier prefix is ∃ b ∃ x ∀ z ∃ t.
  Using the complete expansion of z (z → 0, z → 1) as the expansion tree , we get the following expansion formula
  
    (b)
        (t^z → 0 b)
        (x t^z → 0)
        (x t^z → 0)
        (t^z → 1)
        (x t^z → 1)
        (x t^z → 1) ,

  which has a simple resolution proof π.
  The conclusion of () leads to the proof object 5,6,7,8,9 ^4, but only clause 5 contains literals bound before quantification level 5.
  After a universal reduction, the proof continues as described in Example <ref>.




  The ∀exp-res rule is sound.


  Assume otherwise, then one would be able to derive a proof object ^k-1 that is part of a  refutation proof for true QBF Φ.
  Thus, the clause corresponding to ^k-1 (cf. proof of Theorem <ref>) (⋁_i ∈⋁_l ∈(i, < k) l) made Φ false.
  However, the same clause can be derived directly by applying the expansion  to the original QBF, i.e., expanding universal variables beginning with quantification level k+1, and propositional resolution on the resulting expansion formula.
  Thus, this clause can be conjunctively added to the matrix without changing satisfiability, leading to a contradiction.
  

The resulting proof system can be viewed as a unification of the currently known CEGAR approaches for solving quantified Boolean formulas <cit.>.
 
   does not p-simulate .


   does not p-simulate level-ordered Q-resolution <cit.>.
  
The combination of both rules makes the proof system stronger than merely choosing between expansion and resolution proof upfront.
 
  There is a family of quantified Boolean formulas that have polynomial refutation in , but have only exponential refutations in  and .


  For this proof, we take two formulas that are hard for  and , respectively.
  We build a new family of formulas that has a polynomial refutation in , but only exponential refutations in  and .
  
  The first formula we consider is formula (2) form <cit.>, that we call  in the following:
  
    ∃ e_1 ∀ u_1 ∃ c_1 c_2 …∃ e_n ∀ u_n ∃ c_2n-1 c_2n
        (⋁_i ∈ 1 … 2nc_i) ⋀_i ∈ 1 … n (e_i  c_2i-1)  (u_i  c_2i-1)  (e_i  c_2i)  (u_i  c_2i)

  It is known that  has a polynomial level-ordered  proof and only exponential  proofs <cit.>.
  As a second formula, we use the _n formula <cit.>
  
    ∃ x_1 … x_n ∀ z ∃ t_2 … t_n (x_1,x_2,t_2) ⋀_i ∈ 3 … n(t_i-1, x_i, t_i)  (z  t_n)  (zt_n)

  where (o_1, o_2, o) = (o_1 o_2 o)  (o_1  o_2 o)  (o_1  o_2  o)  (o_1 o_2  o) defines o to be equal to o_1 ⊕ o_2.
  _n has a polynomial  refutation but only exponential  refutations <cit.>.

  We construct the following formula
  
    ∃ e_1 ∀ u_1 ∃ c_1 c_2 …∃ e_n ∀ u_n ∃ c_2n-1 c_2n∀ a ∃ b ∃ x_1 … x_n ∀ z ∃ t_2 … t_n 
       ⋀_i ∈ 1 … n (e_i  c_2i-1)
         (u_i  c_2i-1)
         (e_i  c_2i)
         (u_i  c_2i) 
       
        (ab⋁_i ∈ 1 … 2nc_i) (x_1,x_2,t_2)
        ⋀_i ∈ 3 … n(t_i-1, x_i, t_i)
         (z  t_n  b)
         (zt_n)

  We argue in the following that this formula has a polynomial refutation in .
  First, using () we can derive the proof object containing the clause (a⋁_i ∈1 … 2nc_i) using the expansion tree = z → 0, z → 1 and the clauses from the last row (analogue to Example <ref>).
  After applying universal reduction, the proof object representing clause (⋁_i ∈1 … 2nc_i) can be derived.
  For the remaining formula, there is a polynomial and level-ordered resolution proof <cit.>, thus, the formula has a polynomial  proof.
  
  There is no polynomial  proof, because deriving (⋁_i ∈1 … 2nc_i) is exponential in .
  Likewise, there is no polynomial  proof as the formula after deriving this clause has only exponential  refutations.
  

One question that remains open, is how the new proof system compares to unrestricted .
We already know that the new proof system polynomially simulates both tree-like  as well as level-ordered .

 
   does not p-simulate .


  We construct a formula that is hard for expansion and level-ordered , but easy for (unrestricted) .
  We have already seen in the proof of Theorem <ref> that  is hard for  but easy for .
  However, the  proof of  is level-ordered.
  Hence, we need an additional formula that is hard to refute for level-ordered .
  We use the modified pigeon hole formula from <cit.> where unrestricted resolution has polynomial proofs and resolution proofs that are restricted to a certain variable ordering are exponential.
  Using universal quantification, one can impose an arbitrary order on a level-ordered  proof, thus, there is a quantified Boolean formula which has only exponential level-ordered  but has a polynomial  proof.
  The disjunction of those two formulas gives the required witness.
  This formula is easy to refute for , but the first one is hard for  and the second is hard for level-ordered .
  



 §.§ Comparison Between Extensions

We conclude this section by comparing the two extensions of the  calculus introduced in this paper.

 
	 and  with strengthening rule are incomparable.


The family of formulas ' from proof of Corollary <ref> separates  and  with strengthening rule.
Since the strengthening rule is not applicable, all  proofs are exponential while there is a polynomial proof in .

The other direction is shown by using a similar construction as the one used in the proof of Theorem <ref>.
We use a combination of  and  to construct a formula that has only exponential refutations in , but a polynomial refutation using the strengthening rule.
The formula  is used to generate the premise for the application of the strengthening rule to solve .
To generate this premise using the rule () one needs an exponential proof.
There is a polynomial proof for  in , but there is none for , thus,  has only exponential refutations.
  

 
	 with strengthening rule and  are incomparable.


	Follows from the proof of Theorem <ref> as the witnessing formula can be constructed such that the strengthening rule is not applicable.
	The other direction follows from the separation of  and  by Beyersdorff et al. <cit.>.
	




§ EXPERIMENTAL EVALUATION




 §.§ Implementation


We extended the implementation of  with the possibility to use the rule () as introduced in Sec. <ref>[ is available online at <https://react.uni-saarland.de/tools/caqe/>.].
While the rule is applicable at every level in the QBF in principle, the effectiveness decreases when applying it to deeply nested formulas where  tends to perform better <cit.> than .
We aim to strike a balance between expansion and clausal-abstraction, i.e., keeping the best performance characteristics of both solving methods.
Thus, in our implementation, we apply the expansion refinement (additional to the clausal-abstraction refinement) to the innermost universal quantifier.



An overview of the CEGAR algorithm is given in Algorithm <ref>.
There is a close connection between the rules of the  calculus and the presented algorithm.
Especially, we use a SAT solver to prove the refutation needed in the rule ().
We refer to <cit.> for algorithmic details.
Changes to the original algorithm are written in bold text.



  
Abstraction.
The abstraction for quantifier ∃ X_k, written φ_k is the projection of the clauses of the matrix to variables in X_k, i.e., ⋀_1 ≤ i ≤ m(i,k).
We assume that there is a operation to “disable” clauses in φ_k which corresponds to the situation where a clause C_i is satisfied by some variable bound before k.
Likewise, for every clause we allow the assumption that this clause will be satisfied by a some variable bound after k.
This is used to generate candidate proof objects _*^k+1 for inner levels.
In the refinement step, this assumption can be invalidated, i.e., there is a way to force satisfaction of a clause at level k.
Those operations can be implemented by an incremental SAT solver and two additional literals controlling the satisfaction of clauses <cit.>.




  
Algorithm.
The algorithm recurses on the structure of the quantifier prefix and communicates proof objects , which indicate the clauses of the matrix that are satisfied.
At an existential quantifier, the abstraction generates a candidate solution (line <ref>) and checks recursively whether the candidate is correct (line <ref>).
If not, the counterexample originally consists of a set of clauses (which could not be satisfied from the inner existential quantifiers).
We extend this counterexample to also include an expansion tree  from the levels below.
Additionally to the original refinement, we also build the expansion of the QBF with respect to the expansion tree , resulting in a QBF with the same quantifier prefix as the current level (with additional existential variables due to expansion).
This QBF is then translated into a propositional formula in the same way as the original QBF.
Lastly, the abstraction φ_k is then conjunctively combined with this propositional formula.
Note that if the function returns UNSAT (line <ref>), the corresponding resolution proof from the SAT solver can be used to apply the rule () form the  calculus.

As the underlying SAT solver in the implementation, we use  <cit.>,  <cit.>,  <cit.>, or Lingeling <cit.>.



 §.§ Evaluation


In our evaluation, we show that the established theoretical separations shown in the last section translate to a significant empirical improvement.
The evaluation is structured by the following three hypothesizes:
First, the strengthen and expansion refinement give a significant improvement over the plain version of .
Combining both refinements is overall better than only applying one of them.
Second, we show that the improvement provided by the those refinements is independently of the underlying SAT solver.
Third, when comparing on a per instance basis, the combined refinement effects the runtime mostly positively.
We show that the improvement is up to three orders of magnitude.



We compare our implementation against  <cit.>,  <cit.>,  in version 5.0 <cit.>, and  <cit.>.
For every solver except , we use  <cit.> in version 031 as preprocessor.
For our experiments, we used a machine with a 3.6 GHz quad-core Intel Xeon processor and 32 GB of memory.
The timeout and memout were set to 10 minutes and 8 GB, respectively.
Table <ref> shows number of solved instances on the QBFGallery 2014 benchmark set, broken down by benchmark family, as well as the more recent QBFEval 2016 benchmark set.
For , we only report on the best performing version, that is the one using  as a backend solver.


The table shows that the strengthen and expansion refinement individually improve over the plain version of  in the number of solved instances.
Further, the combination of both refinements is the overall best solver, followed by .

In the following, we refer to the combination of strengthen and expansion refinement as extended refinements.
We want to detail the improvements due to the extended refinements and show their independence of the backend solver.
The plot in Fig. <ref> depicts the effect of the extended refinements with respect to the solved instances.
The improvements in the number of solved instances are independent from the choice of the underlying SAT solver and range between 100 to 150 more instances solved compared to the plain version of .




The scatter plot depicted in Fig. <ref> compares the running times of plain  to the one using extended refinements (both using ) on a per instance basis.
Marks below the diagonal means that the variant using extended refinements is faster.
It is remarkable that the extended refinements have mostly positive effect on the solving times.
Only a few instances saw a significant increase in solving time and even less timed out with extended refinements while being solved before.
On the other hand, we see improvements in solving time that exceed three orders of magnitude.
This is an empirical confirmation of our goal stated before that our implementation of expansion-refinement adds performance characteristic of expansion-based solvers while keeping the characteristics of the clausal-abstraction algorithm.







§ RELATED WORK


 <cit.> is a variant of propositional refutation that is sound and refutation complete for QBF.
There have been extensions proposed to , like long-distance resolution <cit.> and universal resolution <cit.>, some which are implemented in the QCDCL solver  <cit.>.
Recently, there has also been extensions proposed that extend  by more generalized axioms <cit.>.
In some sense, the () rule presented in this paper can be viewed as an new axiom rule for the  calculus.

The  calculus <cit.> was introduced to allow reasoning over expansion-based QBF solving, exemplified by the QBF solver  <cit.>.
The work on  was motivated by the same desire, namely understanding the performance of the recently introduced QBF solvers  <cit.> and  <cit.>.
The incomparability of  and  <cit.> lead to the creation of stronger proof systems that unify those calculi, like  <cit.>.
Further separation results, between variants of  and variants of , were given in <cit.>.
Those extensions, however, do not have accompanying implementations.
This also applies to recent work that is based on first-order resolution <cit.>.

There are two well-known restrictions to , that is level-ordered and tree-like .
Those restricted calculi were shown to be incomparable <cit.>.
QCDCL based solver exhibit level-ordered proofs <cit.> and it was shown that  p-simulates tree-like  <cit.>.
We showed that  is polynomial simulation equivalent to level-ordered , which explains similar performance characteristics of the underlying solvers.
Further, the strengthening rule presented in this paper can be viewed as a first step towards breaking the level-ordered restriction.
The  calculus p-simulates level-ordered and tree-like .




§ CONCLUSION


In this paper, we have introduced a new QBF proof calculus  and showed that it is suitable for describing CEGAR based solving algorithms.
We defined two extensions of the  calculus and showed that there is a theoretical advantage over the basic calculus.
Based on this foundation, we implemented an expansion refinement in the solver  and evaluated it on standard QBF benchmark sets.
Our experiments show that our new implementation significantly outperforms the previous one, with little to no negative impact, making it one of the most competitive QBF solver available.
We have also shown that our theoretical considerations and the consequent algorithmic change explains those practical gains.

In future work, we want to improve the implementation by exploring heuristics for the application of the different refinements and we want to explore alternative versions of the strengthening rule presented in this paper.



  
Acknowledgments.
I thank Christopher Hahn and the anonymous reviewers for their comments on earlier versions of this paper.


splncs03



