In this paper we present sQueezeBF, an effective preprocessor for QBFs that combines various techniques for eliminating variables and/or clauses. In particular sQueezeBF combines (i) variable elimination by Q-resolution and equality reduction, and (ii) clause simplification via subsumption and self-subsumption resolution. The experimental analysis shows that sQueezeBF can produce significant reductions in the number of clauses and/or variables - up to the point that some instances are solved directly by sQueezeBF - and that it can significantly improve the efficiency of a range of state-of-the-art QBF solvers - up to the point that some instances cannot be solved without sQueezeBF preprocessing.
Quantified Boolean Formulas are a powerful extension of the Satisfiability
(SAT) problem in which the variables are universally as well as
existentially quantified. Adding the quantification makes QBF a more expressively
compact language with respect to SAT, but this comes with a price: QBF
are believed to be in practice much harder to solve than SAT formulas.
Many different problems can be efficiently encoded as QBF instances, and
recently there has been a great interest and progress in solving such
instances efficiently, such as in Verification [
Preprocessing formulas has been proven to be very effective for solving
SAT instances since it can reduce their size considerably and decrease the
solving time substantially, even taking into account the time required to
perform the preprocessing. Recently two preprocessors have been presented
in the QBF literature. preQuel [
In this paper we present sQueezeBF, an effective preprocessor for QBFs
that combines various techniques for eliminating variables and/or clauses.
In particular sQueezeBF combines variable elimination by Q-resolution and
equality reduction, and clause simplification via subsumption and
self-subsumption resolution. Some of the techniques implemented in sQueezeBF
have been first proposed in SAT (see for example [
This paper is organised as follows. First we review the basics of QBF satisfiability. Then we discuss the algorithm of sQueezeBF. We end the paper with the experimental analysis and the conclusions. 2
Consider a set P of propositional letters. A variable is an element of P. A literal is a variable or the negation of a variable. In the following, for any literal l, • |l| is the variable occurring in l; and • l is l if l is a variable, and is |l| otherwise.
A clause C is an n-ary (n ≥ 0) disjunction of literals such that, for any two distinct disjuncts l, l0 in C, it is not the case that |l| = |l0|. A propositional formula is a k-ary (k ≥ 0) conjunction of clauses.
A QBF is an expression of the form
Q1z1 . . . QnznΦ (n ≥ 0) (1) where • every Qi (1 ≤ i ≤ n) is a quantifier, either existential ∃ or universal ∀, • z1, . . . , zn are distinct variables in P, and • Φ is a propositional formula in the variables z1, . . . , zn.
In (1), Q1z1 . . . Qnzn is the prefix, Φ is the matrix, and Qi is the bounding quantifier of zi. Further, we say that a literal l is existential if ∃|l| belongs to the prefix, and is universal otherwise. In the following, we use true and false as abbreviations for the empty conjunction and the empty disjunction respectively.
We define • the level of a variable zi, to be 1 + the number of expressions Qj zj Qj+1zj+1 in the prefix with j ≥ i and Qj 6= Qj+1; • the level of a literal l, to be the level of |l|; • the level of the formula (1), to be the level of z1.
If ϕ is a QBF and l is a literal, ϕl is the QBF 1. whose matrix Φ is obtained from the matrix of ϕ by deleting the clauses
C such that l ∈ C, and removing l from the others, and 2. whose prefix is obtained from the prefix of ϕ by deleting each variable and corresponding bounding quantifier not occurring in Φ.
The semantics of a QBF ϕ can be defined recursively as follows. If the prefix is empty, then ϕ’s satisfiability is defined according to the truth tables of propositional logic. If ϕ is ∃xψ (respectively ∀xψ), ϕ is satisfiable if and only if ϕx or (respectively and) ϕx are satisfiable. If ϕ = Qxψ is a QBF and l is a literal, ϕl is the QBF obtained from ψ by substituting l with true and l with false . It is easy to see that if ϕ is a QBF without universal quantifiers, the problem of deciding the satisfiability of ϕ reduces to SAT.
In (1), a literal l is • Unit if l is existential, and, for some m ≥ 0, – a clause (l ∨ l1 ∨ . . . ∨ lm) belongs to Φ, and – each literal li (1 ≤ i ≤ m) is universal and has a lower level than l. • Monotone or pure if – either l is existential, l does not belong to any clause in Φ, and l occurs in Φ; – or l is universal, l does not belong to any clause in Φ, and l occurs in Φ. 0 function sQueezeBF(ϕ) 1 do 2 3 4 5 6 7 8 9 ϕ’ = ϕ ϕ = Simplify(ϕ) ϕ = EquivalenceCheck(ϕ) ϕ = Q-resolution(ϕ) if ϕ ≡ true return ϕ if ϕ ≡ false return ϕ while ϕ’ 6= ϕ return ϕ
Given a set of clauses S we define |S| (size of S) as the number of literals contained in S. Finally given a QBF ϕ, a literal l and a set of clauses α, ϕ(l/α) is the QBF obtained from ϕ by substituting each occurrence of l with alpha 1. 3
sQueezeBF In Figure 1 is presented the main algorithm of sQueezeBF. The algorithm takes in input a QBF, and it returns a simplified QBF, that can either be empty (true) or contain an empty clause (false formula). It starts saving the current state of the formula at line 2, and then it applies three operations sequentially: • Simplify(line 3) gets in input the formula and simplifies the formula propagating all the unit and pure literals. Given a formula ϕ and a literal l unit or pure in ϕ, ϕ is equivalent to ϕl. • EquivalenceCheck (line 4) first discovers all the equivalences of the type
l ⇔ l1 ◦ l2 ... ln−1 ◦ ln where ◦ ∈ {∨, ∧} and n ≥ 1, or ◦ ∈ {⇔} and n = 2. Notice that if n = 1 we obtain a binary equivalence. Once the equivalence is found, then it substitutes every occurrences of l with its definition, if and only if the substitution does not increase the size of the formula in terms of literals. • Q-resolution(line 5) can eliminate the variable by Q-resolution. The algorithm for each variable z checks if it is possible to eliminate z 1strictly speaking the result is not a QBF. We assume that the resulting expression is suitably converted to a QBF without introducing additional variables. For instance, each clause C ∨ l gets substituted by the clauses in {C ∨ C0 : C0 ∈ α} by Q-resolving all the clauses where z occurs positively with all the clauses where z occurs negatively. If the formula does not increase in size then the variable is eliminated.
If the formula is neither satisfiable (line 7) nor unsatisfiable (line 6) then the algorithm iterates the operations until no further simplification is possible (line 8). 3.1
The variable elimination via equivalence checking was introduced for SAT
in [
(l ∨ l2... ∨ ln−1 ∨ ln) ∧ (l ∨ l1) ∧ ... ∧ (l ∨ ln) (l ∨ l1 ∨ l2) ∧ (l ∨ l1 ∨ l2) ∧ (l ∨ l1 ∨ l2) ∧ (l ∨ l1 ∨ l2) where in both the formulas (4) and (5) the level of |l| is the lowest among the level of each |li| occurring in the equivalence. Notice that the set (2) corresponds to the definition: l ⇔ l1 ◦ l2... ◦ ln−1 ◦ ln
where ◦ ∈ {∨, ∧} and n ≥ 1 and the set (3) corresponds to the definition:
Once that EquivalenceCheck finds the equivalences, then it substitutes each variable with its definition in the formula. Notice that after a substitution of a variable z with its definition α in a formula ϕ, the new formula ϕ(z/α) is not guaranteed to be in CNF, so a conversion step may be necessary. In order to avoid the introduction of new variables with the commonly used translation techniques, we apply DeM organ rules. It is well known l ⇔ l1 ⇔ l2 that DeM organ rules can increase the size of the resulting QBF. However, by eliminating redundant literals or clauses in the produced set of clauses, such increase often does not happen. In the cases in which it does, we discard the changes and substitution does not take place. This ensures that the formula never increases in size.
Finally, notice that not all the defined variables can be substituted. Take for example:
ϕ = α ∧ (l1 ⇔ l2 ∨ l4) ∧ (l2 ⇔ l3 ∨ l4) ∧ (l3 ⇔ l1 ∨ l5) if l1 is eliminated first, then when l3 is substituted in the formula, l1 is reintroduced, and this is true no matter which variable is substituted first. This problem arises since at least a variable occurs in the definitions of the others. In order to solve the problem of circularity, EquivalenceCheck constructs a dependency graph where each node represents a defined variable, and each edge, connecting the defined variables, represents the dependency between the definitions. So for example, the Figure 2:A represents the dependencies graph of the example above, where the edge from the node l3 and the node l1 represents the fact that l1 occurs in the definition of l3. Notice that the edges have a direction, representing the fact that the pointed node is in the definition of the non pointed one. In Figure 2:A, l1 occurs in the definition of l3. After the graph is created then the algorithm looks for circular path and if any is found then the path is cut eliminating one of the definition. Looking at Figure 2:A in order to eliminate the circular path the algorithm deletes one of the three definitions, for example l2 (Figure 2:B). At this point we can substitute first l3 and then l1 and the formula is simplified eliminating 2 variables. Notice that the order matters, since if we substitute l1 first, then once l3 is substituted l1 is reintroduced. 3.2
Variable elimination via resolution is a technique used in many
state-of-theart SAT solvers, first introduced in [
Given two clauses C1 = {z, l1, ..., ln} and C2 = {z, l10, ..., lm0} the implied clause C = {l1, ..., ln, l10, ..., lm0} is called the resolvent of the two original clauses by performing resolution on the variable z. We write C = C1 ⊗ C2. We can also define the Q-resolution on set of clauses: given a set of clauses Sz, meaning that all contain z and a set of clauses Sz (all containing z) we define the resolvent between set of clauses as:
Sz ⊗ Sz : {Cz ⊗ Cz|Cz ∈ Sz, Cz ∈ Sz} (6) The elimination of a variable z from a QBF can be computed by pairwise resolving each clause in Sz with every clause in Sz. The produced resolvent S0 = Sz ⊗ Sz replaces the original clauses containing z and z resulting in an equivalent problem.
As an example of how the algorithm works, take the formula ϕ containing a variable x and two set of clauses
Sx = {{x ∨ a}, {x ∨ a ∨ c}, {x ∨ d}} and Sx = {{x ∨ a}, {x ∨ b ∨ d}}. then the resolvent between the two set of clauses is
Sx ⊗ Sx = {{a ∨ b}, {a ∨ b ∨ d}, {a ∨ c ∨ b}, {a ∨ c ∨ b ∨ d}, {b ∨ d}}. In order to eliminate the variable x from ϕ, all the clauses in Sx ∪ Sx have to be deleted from ϕ, adding all the clauses in Sx ⊗ Sx and obtaining the formula ϕ0. Notice that in the example, the size of ϕ0 is greater then the size of ϕ, since |Sx ∪ Sx| = 12, and |Sx ⊗ Sx| = 14. In order to avoid an increase in the size of the formula, Q-resolution does not eliminate all the variables, but only the ones that don’t increase the size. In particular a variable z is eliminated from a formula ϕ if and only if |Sz ∪ Sz| ≥ |Sz ⊗ Sz| (7) Notice that the dimension of the resolvent can not be calculated in advance since many trivial clauses, that have to be discarded, can be generated during the Q-resolution process. For this reason the algorithm first calculates the dimension of the original set of clauses, and then it computes the resolvent, discarding it if (7) is not satisfied, and the variable is not deleted. 3.3
A clause C1 is said to subsume a clause C2 if the literals contained in C1 are a subset of the literals contained in C2, and abusing with notation we write that C1 ⊆ C2. A subsumed clause is redundant and can be discarded without changing the QBF it represents. Since redundant clauses are memory consuming, and slow down the search process, it is desirable to make a QBF subsumption free, by detecting and removing the subsumed clauses.
Whenever a new clause is added to the formula, for example as
consequence of a variable elimination, sQueezeBF checks all the existing clauses
in the database to see whether they are subsumed. This check is usually
called as backward subsumption [
Moreover the subsumption algorithm can be expanded: suppose to have
a clause C1 = α ∨ l and a clause C2 = β ∨ l, where the sub-clause α ⊆ β.
We could say that C2 almost subsumes C1 except for the literal l. Applying
resolution on the two clauses we obtain a new clause C = α ∨ β, but since
α subsume β the derived clause becomes C = β, that subsume C2. Thus
after adding C to the database we can delete C2, in essence eliminating one
literal. In this case we say that C2 is self subsumed by C and we call this
technique self-subsuming resolution (see for more details [
Even if eliminating clauses may reduce the size of the formula, the
common perception seems to be that subsumption and removal are expensive,
especially for solvers based on search. However, subsumption removal is
important for solvers or preprocessors based on resolution like for
example the solver Quantor [
sQueezeBF implements subsumption removal based on the occurrences
of the literals. For each clause we define a counter indicating how many
times the clause is visited, always initialised to zero. When a new clause C
is introduced, then all the occurrences of each literal of C are visited and
the corresponding counter is incremented. If in any time a counter reach
the size of the clause visited, then it subsumes C, and C is not learned
(forward subsumption). On the other hand, if a clause counter reach the
size of C, then C subsumes the one checked. The new clause is learned and
the one subsumed is eliminated (backward subsumption). The following
example explains better the algorithm: suppose that we want to introduce
the following clause C = l1 ∨ l2 ∨ l3, into a database containing 3 clauses :
C1 = l1 ∨ l2, C2 = l3 ∨ l4, C1 = l2 ∨ l3. Starting from l1 we visit C1 and we
increment its counter from 0 to 1, then we check l2 visiting again C1 and
incrementing its counter from 1 to 2. Since the counter associated to C1 is
equal to its size, this means that C1 subsumes C, and thus sQueezeBF does
not learn C.
To evaluate the effectiveness of our preprocessor, we compare sQueezeBF
with preQuel and proverbox on a selected pool of fixed-structure QBF
instances taken from QBFLIB [
in average. This is probably due to the fact that the problems are already written in a compact CNF, and applying preprocessor without size bound can only increase the size.
It can also be observed how some families have an average reduction, in terms of number of clauses and variables, equal to 100%: all the instances of these families have been solved by the preprocessor.
Overall, • proverbox has solved 20 instances (10 DFlipFlop, 1 wmiforward, 3
SzymanskiP, and 6 VonNeumann), • preQuel has solved 20 instances (10 DFlipFlop and 10 VonNeumann), and • sQueezeBF has solved 29 instances (10 DFlipFlop, 9 wmiforward and 10 VonNeumann).
However, sQueezeBF is a mix of different techniques and, in order to evaluate the impact that each one has on the preprocessor, sQueezeBF has been run disabling each technique one at a time. In Table 2 we show the results, organised as the Table 1, where in each column, instead of a preprocessor, is presented sQueezeBF with a technique disabled. In particular, the first column (sQueezeBF) represents the full-featured preprocessor (i.e. no technique disabled); the suffixes “– Eq”, “– Qr” and “– Ss” represent a version of sQueezeBF featuring all the techniques but variable elimination via Equivalence Checking, variable elimination by Q-Resolution or clause simplification via Self-Subsumption respectively. For example taking the row Blocks and the column sQueezeBF, the three values (C,V,L/C) = (3211,287,3.01) represent respectively the number of clauses in average (3211), the number of variables in average (287), and the literal per clause in average (3.01). The other columns state the variation with the first one, i.e. looking to the first row (Blocks), the column Eq shows the values (C%,V%,L/C) =(+28,+21,3.01) representing the fact that running the preprocessor without variable elimination via equivalence checking makes the formula larger, having 28% more clauses (i.e. almost 4110 clauses on average) and 21% more variables (i.e. almost 347 variables on average).
Table 2 shows that disabling a technique always leads to a bigger formula, i.e. that all the techniques are necessary to obtain the formula with the lowest size. In the table this is highlighted from the absence of negative numbers. Then, we see that the reduction of clauses is mostly affected by disabling Equivalence Checking, the reduction of variables is mostly affected by Equivalence Checking and Q-Resolution, and the reduction of literals per clause is mostly affected by Self-Subsumption.
In the table, the limit case, in which sQueezeBF solves an instance and another preprocessor doesn’t, is indicated with the symbol “- -”: the family DFlipFlop hasn’t been solved by sQueezeBF disabling the Q-Resolution technique. On average, the number of clauses and variables of the instances of this family has been reduced to 77135 and 57940 respectively.
It can be noticed that, even disabling Equivalence Checking, some of the variables that were eliminated because of a definition of equivalence are still eliminated by Q-Resolution, as witnessed from the numbers in the table.
In order to evaluate the behaviour of the different preprocessors
coupled with a QBF solver, we have run QuBE 3[
4Version 021006. 5Version sSolveC from QBFEVAL 08. 6Version 3.0. 7Version sKizzo-0.10-qck from QBFEVAL 07. Family sQueezeBF – Eq – Qr – Ss
C V L/C C% V% L/C C% V% L/C C% V% L/C Blocks (13) 3211 287 3.01 +28 +21 3.01 +15 +10 2.88 +27 +18 3.08 comp (8) 428 124 2.76 +34 +51 2.57 +5 +3 2.80 +7 +8 2.85 DFlipFlop (10) 1 0 0.00 0 0 0.00 - - - - 2.32 0 0 0.00 EvPr4x4lg (7) 9984 1452 3.83 0 +1 3.83 +5 +16 3.86 +7 0 3.83 EvPr4x4s (7) 42121 5676 3.53 0 0 3.53 +27 +26 3.40 +14 0 3.52 FPFF (5) 645 68 5.83 0 0 5.95 0 0 5.83 +2 0 6.39 FPFS (3) 518 71 6.06 0 0 6.06 0 0 6.06 +1 0 6.52 s499 (6) 9451 3567 2.76 +112 +114 2.79 0 0 2.76 +39 +44 2.87 SN (84) 5070 2212 2.72 +1 +1 2.69 +12 +24 2.62 0 0 2.74 SzymanskiP (12) 45738 29781 3.17 0 0 3.17 +97 +150 2.60 0 0 3.17 VN (10) 1 0 0.00 0 0 0.00 0 0 0.00 0 0 0.00 wmiforward (72) 1364 339 2.82 +78 +101 2.60 +21 +25 2.77 +46 +55 2.89 and the cumulative solving time, for each solver (on the rows) when coupled with a particular preprocessor (on the columns). Notice that in the column original are presented the results for each solver without any preprocessing applied, while the last three columns represent the different versions of sQueezeBF. Table 3 witnesses that sQueezeBF is the only one able to constantly improve the efficiency of a range of state-of-the-art QBF Solvers. In particular the column “–” shows that the use of sQueezeBF improves of a factor two the number of problems solved by a given solver. Using sQueezeBF as preprocessor affects also the solving time of each solver, decreasing it substantially. Moreover, the Table 3 also shows which technique has more impact on which solver. For example, it looks like that disabling the variable elimination via equivalence checking, QuBE can not longer solve many problems, while the self subsumption is the least effective. Instead, looking at the other solvers, disabling both equivalence checking and clause elimination via self subsumption decrease the performance of the solver. For all the solvers the least effective technique seems to be variable elimination via Q-resolution. This is not so surprising since the bound limitation for the Q-resolution is very tight, and sQueezeBF spends a lot of time because there are many variables which are not eliminated because the size of the formula would increase. Notice that the combination of the three techniques always leads to the best performances for some solvers (QuBE, sKizzo and Quantor), but this is not true for others (sSolve and yQuaffle) that are able to solve more problems when Q-resolution is disabled. Finally it is interestSolver original proverbox preQuel –Eq – QuBE 98 (87k) 87 (111k) 111 (78k) 118 (79k) 138 (72k) 148 (70k) 156 (55k) sSolve 95 (88k) 80 (112k) 114 (77k) 115 (77k) 135 (64k) 120 (77k) 133 (66k) yQuaffle 82 (95k) 85 (109k) 88 (92k) 88 (86k) 104 (75k) 96 (81k) 101 (79k) sKizzo 111 (78k) 110 (93k) 120 (73k) 116 (70k) 143 (56k) 120 (69k) 147 (53k) Quantor 104 (80k) 106 (95k) 128 (67k) 106 (74k) 123 (64k) 106 (76k) 136 (58k) sQueezeBF –Qr –Ss ing to see in table 3 that the preprocessor, on this set of benchmarks, makes QuBE a better solver than sKizzo.
About the time needed by the different preprocessors, these are cumulatively presented in Table 3, where it is shown also the effect of the different preprocessors (sQueezeBF, proverbox, preQuel) when coupled with different solvers (QuBE, sSolve, yQuaffle, sKizzo and Quantor). In general, the preprocessing time is negligible wrt the whole task of preprocess and solve, but for some large instances it can be more onerous trying to simplify it rather than solving it by a solver. The cumulative preprocessing times are approximately 410s for preQuel, 1470s for sQueezeBF, and 15500s for proverbox. 5
In this paper we present sQueezeBF, a very effective preprocessor for QBF reasoning. We took into account many benchmarks from different families and two other different preprocessing tools, preQuel and proverbox. We have shown that sQueezeBF is much more effective in terms of formula reduction, since most of the times decreases the size of the formula preprocessed, and never increases the size of the formula, and this is not always true for preQuel and proverbox. We also compare five different state-of-theart solvers: the proposed techniques offer robust improvements across the different solvers among all the tested benchmark families. To the best of our knowledge thanks to sQueezeBF the solvers are able to solve 34 problems that have never been resolved before. Finally, as future work, we would like to implement new techniques such as, for example, variable expansion and binary clause resolution.