Symmetry Breaking in Quantified Boolean Formulae

1 Introduction

Solving Quantified Boolean Formulae (QBF) has become an attractive and important research area over the last years. Such increasing interest might be related to different factors, including the fact that many important artificial intelligence (AI) problems (planning, non monotonic reasoning, formal verification, etc.) can be reduced to QBF which is considered as the canonical problem of the PSPACE complexity class. Another important reason comes from the recent impressive progress achieved in the practical resolution of the satisfiability problem. Many solvers for QBFs have been proposed recently (e.g. [Giunchiglia et al., 2001b; Zhang and Malik, 2002; Letz, 2002; Benedetti, 2005]), most of them are obtained by extending satisfiability results. This is not surprising, since QBFs is a natural extension of the satisfiability problem (deciding whether a boolean formula in conjunctive normal form is satisfiable or not), where the variables are universally or existentially quantified.

Some classes of QBFs encoding real-world application and/or AI problems contain many symmetries. Exploiting such structures might lead to dramatically reducing the search space. Symmetries are widely investigated and considered as an important task to deal with the intractability of many combinatorial problems such as constraint satisfaction problems (CSP) and satisfiability of boolean formula (SAT).

∗supported by ANR "Planevo" project no JC05 41940.

A previous work on symmetry breaking predicates for QBF was proposed by [Audemard et al., 2004]. The authors use an hybrid QBF-SAT approach where the set of generated breaking predicates is separated from the QBF formula. Consequently, this approach is solver dependent. Indeed, to solve the hybrid QBF-SAT formula, DPLL-based QBF solvers need to be adapted, whereas, other kind of solvers (e.g. Skizzo) can not be used in this context.

In this paper, we propose a preprocessing approach which is solver independent. Taking as input a QBF with symmetries, we generate a new QBF formula without symmetries equivalent to the original one wrt. validity. To break such symmetries we extend the SAT approach proposed by Crawford [Crawford, 1992; Aloul et al., 2002].

The paper is organized as follows. After some preliminary definitions on quantified boolean formulae, symmetry framework in QBFs is presented. Then a symmetry breaking approach for QBF is described. An experimental validation of our approach is given, showing significant improvements over a wide range of QBF instances. Finally, promising paths for future research are discussed in the conclusion.

2 Technical Background

2.1 Quantified boolean formulae

Let P be a finite set of propositional variables. Then, LP is the language of quantified Boolean formulae built over P using ordinary boolean formulae (including propositional constants ⊤ and ⊥) plus the additional quantification (∃ and ∀) over propositional variables.

In this paper, we consider quantified boolean formula Φ in the prenex clausal form Φ = QkXk, . . . , Q1X1Ψ (in short QXΨ, QX is called a prefix and Ψ a matrix) where Qi ∈ {∃, ∀}, Xk, . . . ,X1 are disjoint sets of variables and Ψ a boolean formula in conjunctive normal form. Consecutive variables with the same quantifier are grouped. We define V ar(Φ) = ⋃i∈{1,...,k} Xi the set of variables of Φ and V arU(Φ) = {x|x ∈ V ar(Φ), x is universal}. A literal is the occurrence of propositional variable in either positive (l) or negative form (¬l). Lit(Φ) = ⋃i∈{1,...,k} Lit(Xi) the set of complete literals of Φ, where Lit(Xi) = {xi, ¬xi|xi ∈ Xi}. The set of literals are encoded using integer numbers i.e. the positive (resp. negative) literal l (resp. ¬l) is associated to a positive number α (resp. -α). Then, we define |l| as the absolute value of l.

For a given variable x ∈ V ar(Φ) st. x ∈ Xk, we define rank(x) = k. Variables appearing in the same quantifier group are equally ranked.

2.2 Symmetries in Quantified Boolean Formulae

Let Φ = Q1X1, . . . ,QmXmΨ be a QBF and σ a permutation over the literals of Φ i.e. σ : Lit(Φ) ↦→ Lit(Φ). The permutation σ on Φ is then defined as follows: σ(Φ) = Q1σ(X1), . . . ,Qmσ(Xm)σ(Ψ). For example, if Ψ is in clausal form then σ(Ψ) = {σ(c)|c ∈ Ψ} and σ(c) = {σ(l)|l ∈ c}.

Definition 1 Let Φ = Q1X1, . . . ,QmXmΨ be a quantified boolean formula and σ a permutation over the literals of Φ. σ is a symmetry of Φ iff

Let us note that each symmetry σ of a QBF Φ is also a symmetry of the boolean formula Ψ. The converse is not true. So the set of symmetries of Φ is a subset of the set of symmetries of Ψ.

A symmetry σ can be seen as a list of cycles (c1 . . . cn) where each cycle ci is a list of literals (li1 . . . lini ) st. ∀1 ≤ k < ni, σi(lik ) = lik+1 and σi(lini ) = li1 . We define |σ| = ∑ci∈σ |ci| where |ci| is the number of literals in ci.

It is well known that breaking all symmetries might lead in the general case to an exponential number of clauses [Crawford et al., 1996]. In this paper, for efficiency and clarity reasons, we only consider symmetries with binary cycles. Our approach can be extended to symmetries with cycles of arbitrary size.

Detecting symmetries of a boolean formula is equivalent to the graph isomorphism problem [Crawford, 1992; Crawford et al., 1996] (i.e. problem of finding a one to one mapping between two graphs G and H). This problem is not yet proved to be NP-Complete, and no polynomial algorithm is known. In our context, we deal with graph automorphism problem (i.e. finding a one to one mapping between G and G) which is a particular case of graph isomorphism. Many programs have been proposed to compute graph automorphism. Let us mention NAUTY [McKay, 1990], one of the most efficient in practice.

Recently, Aloul et al. [Aloul et al., 2002] proposed an interesting technique that transforms CNF formula Ψ into a graph GΨ where vertices are labeled with colors. Such colored vertices are considered when searching for automorphism on the graph (i.e. vertices with different colors can not be mapped with each others).

In [Audemard et al., 2004], a simple extension to QBFs formulae is given. Such extension is simply obtained by introducing a different color for each set of vertices whose literals belong to the same quantifier group. In this way, literals from different quantifier groups can not be mapped with each others (see the second condition of the definition 1). Then, to detect such symmetries, NAUTY is applied on the graph representation of the QBF.

3 Breaking symmetries in QBFs

Symmetry breaking has been extensively investigated in the context of constraint satisfaction and satisfiability problems. The different approaches proposed to break symmetries can be conveniently classified as dynamic and static schemes. Dynamic breaking generally search and break symmetries using breaking predicates or not [Benhamou and Sais, 1994; Gent and Smith, 2000]. Static breaking schemes refer to techniques that detect and break symmetries in a preprocessing step. For SAT, symmetries are generally broken by generating additional constraints, called symmetry breaking predicates (SBP) [Crawford, 1992; Aloul et al., 2002]. Such SBP eliminates all models from each equivalence class of symmetric models, except one. However, in the general case, the set of symmetry predicates might be of exponential size. In [Aloul et al., 2002], Aloul et al extend the approach of Crawford [Crawford, 1992] by using group theory and the concept of non-redundant generators, leading to a considerable reduction in the SBP size.

We briefly recall the symmetry breaking technique introduced by Crawford in [Crawford et al., 1996]. Let Ψ be a CNF formula and σ = {(x1, y1) . . . (xn, yn)} a symmetry of Ψ. The SBP associated to σ is defined as follows:

The SBP defined above expresses that, when for all i ∈ {1 . . . k - 1} xi and yi are equivalent (get the same truth value) and xk is true, then yk must be assigned to true. This reasoning can be extended to QBF provided that the symmetry follows the prefix ordering.

3.1 Motivation

In the following example, we show the main difficulty behind the extension of SAT symmetry breaking predicates (SBP) to QBFs.

Example 1 Let Φ = ∀x1y1∃x2y2 Ψ1 be a QBF where Ψ = (x1 ∨¬x2)∧(y1 ∨¬y2)∧(¬x1 ∨¬y1 ∨x2 ∨y2). The permutation σ1 = {(x1, y1)(x2, y2)} is a symmetry of Φ. Breaking the symmetry σ1 using the traditional approach, induces the following SBP : (¬x1 ∨ y1) ∧ (¬x1 ∨ ¬x2 ∨ y2) ∧ (y1 ∨ ¬x2 ∨y2). As the clause (¬x1 ∨y1) is universally quantified, the new obtained QBF by adding the SBP to the original QBF leads to an invalid QBF formula.

To overcome this main drawback, in addition to the classical SBP, new breaking predicates (called QSBP) are generated for symmetries containing at least one universal cycle (see definition 3). In such a case, some variables become existentially quantified. These variables will be associated to new additional universally quantified variables. There relationships are expressed in the generated QSBP. To safely add such QSBP to the original QBF formula, a new prefix ordering is computed.

After a formal presentation of our approach for a single symmetry, a generalization to arbitrary set of symmetries is then described.

3.2 Breaking a single symmetry

Now, we formally introduce our approach for breaking symmetries in QBF.

Definition 2 Let Φ = Q1X1 . . .QiXi . . .QmXm Ψ be a QBF and σ a symmetry of Φ. We define σ ↑ Xi as the subsequence of the symmetry σ restricted to the cycles involving variables from Xi. Then, the symmetry σ can be rewriten following the prefix ordering as {σ1 . . . σi . . . σm} such that σi = σ ↑ Xi. When σ respect the prefix ordering, it is called p-ordered.

In the sequel, symmetries are considered to be p-ordered.

Example 2 Let Φ = ∃x2y2∀x1y1∃x3y3 (¬x1 ∨ y1 ∨ x3) ∧ (x1 ∨¬x2 ∨y3)(x1 ∨x2 ∨x3) ∧ (¬x3 ∨¬y3) ∧ (x1 ∨x2)(x1 ∨ y2) ∧ (¬x1 ∨ ¬y1 ∨ ¬x2 ∨ ¬y2) Φ has a symmetry σ = {(x1, y1)(x2, y2)(x3, y3)}. Reordering σ with respect to the prefix leads to σ = {σ1, σ2, σ3} st. σ1 = σ ↑ X1 = (x2, y2), σ2 = σ ↑ X2 = (x1, y1), σ3 = σ ↑ X3 = (x3, y3).

Definition 3 Let Φ be a QBF, σ a symmetry of Φ and c = (x, y) is a cycle of σ. We define x (resp. y) as an in-literal (resp. out-literal). A cycle c is called universal if x and y are universally quantified. A symmetry σ is called universal if it contains at least one universal cycle, otherwise it is called existential.

For existential symmetries of a QBF, classical SBP [Crawford et al., 1996] can be translated linearly to a CNF formula thanks to new additional variables. The obtained set of clauses can be added to the QBF matrix while preserving its validity. The main problem arises when breaking universal symmetries (see example 1). Indeed, to safely break universal symmetries while keeping the classical SBP, we first reorder the symmetry variables belonging to the same universal quantifier group. This new ordering allows us to determine literals to be likely implied from the SBP. Secondly, as implied universal literals lead to the invalidity of the QBF, an original approach is then proposed to deal with such literals. In the following, the problem behind universal implied literals is illustrated and our approach is then motivated.

Let σ = {(x1, y1), . . . , (xk, yk), . . . } be a universal symmetry of a given QBF Φ where (xk, yk) is a universal cycle. As mentioned above, σ is ordered according to the prefix of Φ. Suppose xi and yi for 1 ≤ i ≤ k - 1 are assigned the same truth value, if xk is assigned to true then the universal literal yk is implied from the SBP. To avoid such a case, the universal quantifier of yk is substituted with an existential quantifier. However, when xi and yi are assigned to different truth values or xk is assigned to false, yk must remain universally quantified. To manage these two cases, a new universal variable y′k is then introduced. This variable plays the same role as yk in the second case whereas in the first case it becomes useless. The relation between the two variables is expressed using new predicates (called qsbp(σ(yk))).

Definition 4 Let σ = {c1 . . . ck . . . cn} st. ck = (xk, yk), 1 ≤ k ≤ n be a universal symmetry. We define QSBP (σ) = ∪{qsbp(σ(yk)), 1 ≤ k ≤ n st. yk is universal} as the QSBP associated to σ. QSBP(σ) is built using the two following steps:

1. Adding auxiliary variables : For each universal cycle ck = (xk, yk) ∈ σ, we associate a new universal variable y′k to the out-literal yk and the universal quantifier of yk is substituted with an existential quantifier.
2. Generating new predicates :
3. if (x1, y1) is a universal cycle st. |x1| ̸= |y1| then qsb(σ(y1)) = {¬x1 → (y1 ↔ y′1 )}
4. ∀k > 1, if (xk, yk) is a universal cycle then qsbp(σ(yk)) is made of the following constraints
5. ¬xk → (yk ↔ y′k ) when |xk| ̸= |yk|
6. ((¬xj ∧ yj) → (yk ↔ y′k )), ∀j st. 1 ≤ j < k

Example 3 Let us consider the QBF Φ given in example 1. The symmetry σ of Φ contains one universal cycle (x1, y1). Using definition 4, a new variable y′1 is associated to the variable y1 which becomes existentially quantified. Then QSBP(σ)= qsbp(σ(y1))= (¬x1 → (y1 ↔ y′1 ))

As described above, to generate the QSBP new variables are introduced. In the sequel, we describe how such variables are integrated in the QBF prefix.

Definition 5 Let Φ = Q1X1 . . .QmXm Ψ be a QBF, and σ = {σ1 . . . σj . . . σm} be a universal symmetry. Let j st. Qj = ∀ and σj = σ ↑ Xj = {(x1, y1) . . . (xn, yn)} and Y ′ = {y′1 . . . y′n} the set of new variables associated to {y1 . . . yn} respectively. We define the new ordering of V ar(σj) ∪ Y ′ as follows : rank(xk) < rank(y′k ) < rank(yk) st. 1 ≤ k ≤ n.

We define Gσj (V,A) as the precedence graph associated to σj with V = ⋃1≤k≤n {xk, yk, y′k } and A = {⋃1≤k≤n{(xk, y′k ), (y′k , yk)}}.

To rewrite the quantifier group QjXj of the QBF formula (see definition 6), a new ordering is derived by applying topological sort algorithm on the precedence graph. Let us note that such a graph is acyclic. In figure 1, the graph representation of σj = σ ↑ Xj is illustrated. The ordering x1 . . . xn y′1 . . . y′ny1 . . . yn is then considered.

✗✔

✖✕

Definition 6 Let Φ = Q1X1 . . .QmXm Ψ be a QBF, σ = {σ1 . . . σm} a universal symmetry and for j ∈ {1 . . .m} σj = σ ↑ Xj = {(x1, y1), . . . (xn, yn)}. Every quantifier group QjXj of Φ is rewritten :

• if Qj = ∀ and σ ↑ Xj ̸= ∅ then Qpj X p j = ∀(Xj\V ar(σj))x1 . . . xn∃α∀y′1 . . . y′n∃y1 . . . yn

(see figure 1) st. X p j = Xj ∪ {y′1 . . . y′n} and α is a new variable.

• otherwise Qpj X p j = QjXj

Φ is then rewritten as ΦS = Qp1X p 1 . . .Qpi X p i . . .QpmX pm Ψ∧ SBP ∧QSBP

Remark 1 In definition 6, a new variable α is introduced to constrain the set of variables {x1, . . . xn} to be assigned before {y′1 , . . . , y′n}.

Property 1 Let Φ be a QBF and σ a symmetry of Φ, then Φ is valid iff ΦS is valid.

To sketch the proof of property 1, we consider the QBF given in the example 1. Applying our approach on Φ, we obtain the QBF :

Φs = ∀x1∃α∀y′1∃y1x2y2 Ψ1 ∧ (¬x1 ∨ y1) ∧ (¬x1 ∨¬x2 ∨ y2) ∧ (y1 ∨ ¬x2¬y2) ∧ (x1 ∨ y1 ∨ ¬y′1 ) ∧ (x1 ∨ ¬y1 ∨ y′1 ) When x1 is assigned to the value true, from the clause (¬x1 ∨ y1) we deduce that y1 is true. If x1 is assigned the value false, the original universal variable y1 is deduced by substitution (y′1 and y1 are equivalent) thanks to the added constraint ¬x1 → (y1 ↔ y′1). As rank(y′1) < rank(y1), we only need to substitute all occurrences of y1 by y′1 .

3.3 Breaking all symmetries

Generating QSBP

When considering several symmetries, we can not eliminate them independently by processing each single symmetry using the single symmetry breaking approach described in section 3.2. One needs to consider the interactions between the different symmetries. Indeed, considering an universal outliteral yk and its associated new variable y′k , the qsbp(σ(yk)) express the conditions under which such literals yk and y′k are equivalent. As only one variable y′k is introduced for each universal out-literal yk, when yk appears in several symmetries, the different conditions leading to such equivalence need to be combined.

Definition 7 Let Φ be a QBF, and σ = {(x1, y1) . . . (xi, y) . . . }. σ′ = {(z1, w1) . . . (zj , y) . . . } two symmetries of Φ with y an universal out-literal. The qsbp's associated to y with respect to σ and σ′ can be written in the following form (see definition 4) :

• qsbp(σ(y)) = {α1 → (y ↔ y′ )) . . . αN → (y ↔ y′ )}
• qsbp(σ′ (y)) = {β1 → (y ↔ y′ ) . . . βM → (y ↔ y′ )}.

We define a binary correlation operator η between σ and σ′ as follows : η(σ(y), σ′ (y)) = {(α1 ∧ β1) → (y ↔ y′ ) . . . (α1 ∧ βM) → (y ↔ y′ ) . . . (αN ∧β1) → (y ↔ y′ ) . . . (αN ∧βM) → (y ↔ y′ )}.

Definition 8 Let S = {σ1 . . . σn} be a set of symmetries of a given QBF and y is universal literal. We define,

• S[y] = {σj |∃(x, y) ∈ σj } = {σ′1 . . . σ′|S[y]|}.
• qsbp(S[y]) = η(η . . . η(σ′1 , σ′2 ) . . . , σ′|S[y]| ) . . . ).

Definition 9 Let S = {σ1 . . . σn } be the set of symmetries of a given QBF Φ = QX Ψ. The new QBF matrix ΨS is defined as follows:

Prefix ordering

Let us now show how a new QBF prefix is built when considering a set of symmetries (for a single symmetry see definition 6). For a set of symmetries {σ1 , . . . , σn}, we consider for each universal quantifier group QkXk, all the projections σi ↑ Xk for each symmetry σi . The new quantifier group QpkX p k is obtained from the precedence graph representation of all these projections. Let us recall that each symmetry σi is considered p-ordered. Additionally, to avoid cycles from the graph representation of {σi ↑ Xk|1 ≤ i ≤ n}, each projection σi ↑ Xk is considered lexicographically ordered.

Definition 10 Let σ = {(x1, y1), . . . , (xn, yn)} be a set of cycles. σ is called lexicographically ordered (lex-ordered in short), iff xi > 0, xi ≤ |yi| 1 ≤ i ≤ n and xi < xi+1 1 ≤ i < n

Example 4 Let Φ = Q1X1 . . .QmXm Ψ be a QBF, σ and σ′ two symmetries of Φ st. σ ↑ X1 = {(x2, x1)(¬x3, ¬x4)(x5, x6)}, σ′ ↑ X1 = {(x3, x1)(x2, ¬x6)} and Q1 = ∀. With respect to lexicographical order, σ ↑ X1 = {(x1, x2)(x3, x4)(x5, x6)} and σ′ ↑ X1 = {(x1, x3)(x2, ¬x6)} Figure 2 shows the precedence graph representation of both σ ↑ X1 and σ′ ↑ X1. Applying topological sort algorithm, the quantifier QP1 X P 1 is then rewritten as QP1 X P 1 = ∀x1x5∃α∀x′2 x′3 ∃x2x3∀x′4 x′6 ∃x4x6

✗✔

✖✕

✗✔

✖✕

Dealing with universal cycles of the form (y, x) and (z, ¬x)

To preserve the equivalence (wrt. validity) between the original QBF and the new generated one, let us now address the last problem arising from the interactions between the different symmetries. As illustrated in the following example, the problem arises for symmetries where a universally quantified out-literal x appears both positively (x) and negatively (¬x).

Using our approach the quantifier group QiXi is rewritten as ∀(Xi\V ar(σ, σ′ ))∀x1x2∃α∀y′2∃y2. The generated SBP for σ contains the clause c = (¬x1 ∨ x4). For σ′ its corresponding SBP contains the clause c′ = (¬x2 ∨ ¬y2). As the universal variable x4 is substituted with an existential one, applying the Q-resolution rule [Kleine-B¨uning et al.,

1995] on c and c′ leads to a universally quantified resolvent r = (¬x1 ∨ ¬x2). Consequently, the new obtained QBF is invalid. Finding a new ordering which avoid this problem is a very challenging task. In example 5, such a problem can be avoided by considering the new ordering x1 < y2 < x2 instead of the used lex-ordering. Another possible solution, actually under investigation is to apply composition between symmetries. More precisely, if we consider σ ◦ σ′ ◦ σ we obtain a new symmetry σ′′ = (x1, ¬x2). If in addition to σ and σ′ , we also consider σ′′ , then the previous resolvent generated using Q-resolution is now not universally quantified. Indeed, as x2 is an out-literal, its universal quantifier is substituted with an existential one. Then the resolvent r contains a literal ¬x2 whose associated variable is existentially quantified. Finally, the quantifier group QiXi can be rewritten as Qpi X p i = ∀x1∃α∀x′2∃x2∀y′2∃y2.

The above discussion gives us an idea on how to solve in the general case, the problem arising from symmetries with universal cycles of the form (y, x) and (z, ¬x). In this paper, such a problem is simply avoided using the following restriction :

Definition 11 Let Φ = Q1X1 . . .QmXmΨ be a QBF, y ∈ V arU(Φ) and S the set of symmetries of Φ. We define S[y] ↓ y = {σ ↓ y|σ ∈ S[y]}. For σ = {(x1, y1), . . . , (xk, yk) . . . , (xn, yn)}, we define σ↓ yk = {(x1, y1), . . . , (xk-1, yk-1)}. The restriction of S wrt. y is defined as rt(S, y) = {σ|σ ∈ S, σ[y] = ∅, σ[¬y] = ∅} ∪ S[y] ∪ S[¬y]↓{¬y}. For the set of variables V arU(Φ) = {v1, . . . , v|V arU(Φ)|}, we define rt(S, V arU(Φ)) = rt(. . . rt(S, v1), v2) . . . v|V arU(Φ)|) . . . )

Note that if S[y] = ∅ or S[¬y] = ∅, then rt(S, y) = S. Naturally, for a given set of symmetries S, the new QBF formula is generated using rt(S, V arU(Φ)). In this way the obtained formula is equivalent wrt. validity to the original one.

Complexity

Let σ be a symmetry of a QBF and CNF(QSBP(σ)) the CNF representation of QSBP(σ). The worst case spacial complexity of CNF(QSBP(σ)) is in O(|σ|2 ). Considering σ = {σ1, . . . , σn} with σi = (xi, yi), 1 ≤ i ≤ n, the worst case is reached when all cycles of σ are universal. In this case, QSBP(σ) = ⋃1≤i≤n qsbp(σi(yi)). |QSBP(σ)| = ∑1≤i≤n |qsbp(σ(yi))|. |qsbp(σ(yi))| is equal to 2(i - 1) + 2 = 2i (see definition 4). Then, |QSBP(σ)| = ∑1≤i≤n 2i which is equal to n(n + 1). More interestingly, using the same new variables introduced for CNF(SBP), the size of QSBP(σ) becomes linear. Unfortunately, because of the correlations between different symmetries, the QSBP associated to a set of symmetries is exponential in the worst case. In practice, on all the considered QBF instances, the number of applied correlations (definition 7) does not exceed 3. Consequently, the QSBP is most often of reasonable size.

4 Experiments

The experimental results reported in this section are obtained on a Xeon 3.2 GHz (2 GB RAM) and performed on a large panel of symmetric instances (619) available from [Giunchiglia et al., 2001a]. This set of QBF instances contains different families like toilet, k *, FPGA, qshifter. As a comparison, we run the state-of-the-art DPLL-like solver SEMPROP [Letz, 2002] on QBF instances with and without breaking symmetries. The time limit is fixed to 900 seconds. Results are reported in seconds. The symmetry computation time (including detection and QSBP generation) is not reported (less than one second in most cases).

The scatter plot (in log scale) given in figure 3 illustrate the comprative results of SEMPROP [Letz, 2002] on each QBF instance Φ and ΦS respectively. The x-axis (resp. y-axis) corresponds to the cpu time tx (resp. ty) obtained by SEMPROP on Φ (resp. ΦS ). Each dot with (tx, ty) coordinates, corresponds to a QBF instance. Dots above (resp. below) the diagonal indicate instances where the original formula Φ is solved faster i.e. tx < ty (resp. slower i.e. tx > ty) than the QBF formula ΦS .

Figure 3 clearly shows the computational gain obtained using symmetry breaking predicates (about 167 instances are solved more efficiently). In some cases the gain is up to 2 orders of magnitude. Of course, there exists some instances where breaking symmetries decreases the performances of SEMPROP(about 50 instances). On the remaining instances, the performance of the solver remains the same with or without breaking symmetries.

Table 1 provides more detailed results on the different QBF families. The second column (NB) represents the number of instances in each family. The third column (U) indicates if the instances contain universal symmetries (Y ) or not (N). For each family, S and TT represents the total number of solved instances and the total run-time needed for solving all the instances (900 seconds are added for each unsolved one) respectively.

As we can see, table 1 gives us more comprehensive results with respect to each family. First, breaking symmetries significantly improves SEMPROP performances on many QBF families leading to more solved instances (18 instances). Secondly, the existence of universal symmetries seems to be an important factor for reducing the search time. Not surprisingly, we have also noticed that symmetries between literals occurring in the innermost quantifier group are useless. Indeed, such symmetries does not lead to a great reduction in the search tree, since their corresponding variables are assigned last i.e. the formula is considerably reduced by the previous assignments. Finally, for QBF families containing only existential symmetries, breaking them do not improves the search time. On k branch, k lin, toilet a families containing only existential symmetries, no improvement is observed. Most of these instances correspond to the dots near the diagonal (see figure 3).

5 Conclusion

In this paper, a new approach to break symmetries in QBF formulae is proposed. Using universally quantified auxiliary variables, new symmetry breaking predicates are generated and safely added to the QBF formula. Experimental results show that breaking symmetries leads to significant improvements of the state-of-the-art QBF solver SEMPROP on many classes of QBF instances. These experimental results suggest that for QBF instances containing universal symmetries, significant improvements are obtained. As future works, we plan to investigate the problem arising from the presence of both positive and negative out-literal in the set of symmetries.