Solving QBF by Clause Selection

1 Introduction

The enormous success of SAT enabled us to solve problems that go beyond the NP complexity class. Among these, Quantified Boolean Formulas (QBFs) represent an important formalism. Indeed, as decidingQBFs is PSPACE-complete, they cover a wide range of problems. Namely from model checking, planning, or two-player games [Papadimitriou, 1994; Benedetti and Mangassarian, 2008; Rintanen, 2007; Narodytska et al., 2014].

In the recent years, a number of approaches were developed to solve QBF. Among the most representative are conflict/solution driven learning [Cadoli et al., 1998; Rintanen, 1999; Zhang and Malik, 2002; Giunchiglia et al., 2001], which extends SAT clause learning, and a number of approaches that expand the given QBF into a SAT problem [Biere, 2004; Benedetti, 2004; Janota et al., 2012]

This paper proposes a novel approach for QBF solving that has two distinctive features: 1) it uses a SAT solver as an NP

∗This work is partially supported by SFI PI grant BEACON (09/IN.1/I2618), FCT grant POLARIS (PTDC/EIACCO/123051/2010), CMU-Portugal grant AMOS CMUPEPB/TIC/0049/2013, and national funds through Fundac¸˜ao para a Ciˆencia e a Tecnologia (FCT) with reference UID/CEC/50021/2013.

oracle, 2) it is anchored in the duality hitting set principle. In the Boolean CNF world, the duality hitting set principle lets us reason about minimally unsatisfiable sets (MUSes) by traversing maximally satisfiable sets (MSSes). This has numerous applications in MUS computation (cf. [Reiter, 1987; Liffiton and Sakallah, 2008]) and more recently in MaxSAT solving and other domains [Karp, 2010; Chandrasekaran et al., 2011; Davies and Bacchus, 2011; Stern et al., 2012; Moreno-Centeno and Karp, 2013; Davies and Bacchus, 2013a; Previti and Marques-Silva, 2013; Davies and Bacchus, 2013b; Slaney, 2014].

We first relate MUS computation to solving QBF with two levels of quantification (∀∃). Then, we extend this idea for arbitrary number of quantification levels. Hence, the proposed approach is not only a novel approach to solving QBF but it can also be seen as an extension of the duality hitting set principle for PSPACE.

The proposed approach instantiates a SAT solver at each quantification level, whose task is to select or deselect clauses at that level. The fact that we are using a SAT solver as the underlying reasoning engine in our algorithm is a big engineering advantage. Indeed, if a better SAT solver appears, it can simply substitute the old one in our implementation. The main contributions of the paper are summarized as follows:

(1) A novel algorithm for solving QBF, called QESTO, is developed. (2) A link is established to implicit hitting set algorithms. (3) A link is established to the CEGAR-based QBF solving. (4) A prototype was implemented and evaluated.

The paper begins by overviewing the concepts and notation used (Sec. 2) and continues by developing an algorithm for two-level QBF (Sec. 3). Sec. 4 generalizes this approach to general QBF and Sec. 4.2 relates to other concepts and algorithms. Finally Sec. 5 describes experimental evaluation and Sec. 6 concludes the paper.

2 Preliminaries

Throughout the paper we assume an infinite set of Boolean variables, commonly denoted as x, u, e, etc. Boolean connectives (∧,∨,¬) are used under the traditional semantics. An assignment to a set of Boolean variables X is a mapping from X to the Boolean constants {0, 1}. For an assignment τ : X → {0, 1} and a formula φ we write φ|τ for the application of τ to the formula φ. Hence φ|τ is obtained by replacing all occurrences of each variable x ∈ X by the constant τ(x) and any trivial simplifications are performed (y ∨ 1 ≡ 1, etc.). An assignment τ is a satisfying assignment for a formula φ if φ|τ = 1. A formula is called satisfiable if there exists a satisfying assignment for it and otherwise it is unsatisfiable. A satisfying assignment of a formula φ is often referred to as a model of φ. For two formulas φ and ψ we write φ |= ψ if any satisfying assignments of φ is also a satisfying assignment of ψ.

A Boolean formula is called a literal if it is a Boolean variable or its negation. For a literal l, we write var(l) for the variable in l. A Boolean formula is called a clause if it is a disjunction of literals. A Boolean formula is in Conjunctive Normal Form (CNF) if it is a conjunction of clauses. As common in literature, we often treat clauses as sets of literals (implicitly disjoined) and formulas in CNF as sets of clauses (implicitly conjoined). Observe that the empty set of clauses is semantically true (as the empty conjunction is true) and the empty clause is semantically equivalent to false (as the empty disjunction is false).

Quantified Boolean formulas (QBFs) [Giunchiglia et al., 2009] extend Boolean formulas by allowing to quantify over variables using the existential or the universal quantifier (∃, ∀). Any QBF can be rewritten to an equivalent Boolean formula by rewriting any ∀x. Φ as Φ|{x↦→0} ∧ Φ|{x↦→1} and ∃x. Φ as Φ|{x↦→0} ∨ Φ|{x↦→1}.

A QBF is closed if all variables are bound by a quantifier. A QBF is in prenex form if it can be written as Q1x1 . . .Qnxk. φ where φ is a Boolean formula and Qi ∈ {∃, ∀}. For formulas in prenex form, the quantifier part is called the prefix and the Boolean part the matrix. Unless specified otherwise, in this paper we will be dealing with formulas that are both prenex and closed and the matrix is in CNF. Any adjacent variables with the same quantifier in the prefix are merged into blocks. This enables us to write QBFs in the form Q1X1 . . .QnXk. φ where Xi are sets of variables and Qi ̸= Qi+1 is assumed. We say that Xi is a block at the quantification level i. We write lv(x) for the quantification level of a variable x, i.e., lv(x) = i if x ∈ Xi. We extend this notation to literals. If a variable lv(x) = i and Qi = ∀ than we say that x is universal and analogously for existential variables. The class of closed QBF formulas in prenex form with CNF matrix is referred to as PQCNF.

We model a SAT solver by the function SAT(ψ), which returns a satisfying assignment if the given formula ψ is satisfiable; otherwise it returns the constant ⊥.

An important fact about PQCNF formulas is that any variables universally quantified at the end of the prefix can be removed. For instance, ∃e1e2∀u. (e1 ∨ u) ∧ (¬e2 ∨ ¬u) is equivalent to ∃e1e2. e1 ∧ ¬e2.

3 Solving Two-level PQCNF

Consider a formula ∀X∃Y. φ, where φ is in CNF. To motivate our discussion, let us investigate what must happen for the formula to be false. There must be an assignment τ to the variables X so that there is no corresponding value for the Y variables that would make the matrix φ true. In other words, the CNF φ|τ is unsatisfiable. In the opposite case, when the formula is true, any assignment τ to X makes the CNF φ|τ

input : ∀X∃Y. φ 1 output:truth value C ← {(¬sC ∨ ¬l) | C ∈ φ, l ∈ C, l universal} 2 while true do 3 τ ← SAT(C ) // compute selection 4 if τ = ⊥ then return true 5 S ← {C ∈ φ | τ(sc) = 1} 6 φ′ ← {∨l∈C,var(l)∈Y l | C ∈ S} 7 µ←SAT(φ′ ) // find a model 8 if µ = ⊥ then return false 9 S′ ← {C ∈ φ | there is l ∈ C s.t. µ(l) = 1} 10 C ←C ∧ ∨C∈φ,C/∈S′ sC

satisfiable. Hence, to decide whether a given 2-level PQCNF formula is true or not, it is sufficient to decide whether there exists such assignment to X or not. This is the approach we will take from now on.

Now let us look more closely at the effect of the application of τ to φ. Consider the simple example ∀u∃e. {(u ∨ e), (u ∨ ¬e), (¬u ∨ e)}. If τ(u) = 1, the application of τ yields the CNF {(e)} and τ(u) = 0 yields the CNF {(e), (¬e)}. We can see that the application of τ acts as a selector on the clauses comprising of existential variables. In this particular case, τ(u) = 0 selects an unsatisfiable set of clauses. This resembles the way clauses are selected in recent approaches for implicitly manipulating hitting sets [Chandrasekaran et al., 2011; Davies and Bacchus, 2011; Stern et al., 2012; Moreno-Centeno and Karp, 2013; Previti and Marques-Silva, 2013]. However, in QBF, clauses cannot be selected arbitrarily. Consider another simple example ∀u∃e.{(u ∨ e), (¬u ∨ ¬e)}. Here, regardless of the value of u, the clauses are never selected at the same time, i.e., the result is always satisfiable. This is because selecting a clause requires setting to false all of its universal literals.

The above ideas give rise to a natural algorithm. First, select some set of clauses S and test for its satisfiability. If it is unsatisfiable, stop. If it is satisfiable, block S and any of its subsets to be selected in the future and then repeat. The blocking step can be improved by looking at the satisfying assignment µ of S. Such assignment satisfies some set S′ s.t. S ⊆ S′ . Hence, we can block any set that is a subset of S′ .

This idea is made precise by Algorithm 1. We consider a formula C , which captures the requirements on the considered sets of clauses. Sets of clauses are modeled by selection variables sC , which have the traditional meaning that a clause C ∈ φ is selected whenever sC is true. The formula C is initialized by the condition that a clause can be selected only if it is possible to set all of its universal literals to false.

The algorithm iterates over the following sequence of steps. First it chooses some set of clauses that is permitted by C (ln. 3). If no such set exists, the algorithm terminates and returns true (the formula is true because there is no set of clauses yielding unsatisfiability). Next, the algorithm tests whether the existential part of the selected clauses are satisfiable (ln. 7). If it is unsatisfiable, then we are done because τ is an assignment to the universal variables that selects an unsatisfiable set of clauses. If not, we block all subsets of clauses satisfied by the model. This is done by calculating the set S′ of clauses satisfied by the assignment to the existential variables and then requiring that at least one clause from its complement is selected.

Example 1. Consider the following matrix with the prefix ∀u1u2u3∃e1e2e3; the clauses are identified by a number on the left and they are graphically split into the universal and existential part:

Let us begin by selecting the clauses 1 and 2 , i.e., s1 = s2 = 1. This is possible because it is possible to set to false all the literals u1, u2, u3. The selected clauses correspond to the existential part φ′ = {e1 ∨ e2, ¬e1 ∨ e2}, which is satisfiable by the assignment µ = {e1 ↦→ 0, e2 ↦→ 1, e3 ↦→ 0}, let's say. The assignment µ satisfies the clauses 1 , 2 , and 4 . Hence, the clause 3 must be selected in any further attempts, i.e., the condition C is strengthened by the unit clause (s3). Due to this condition, in the next iteration the algorithm cannot select the clause 1 nor 2 since they contain the literal u1 but 3 contains the literal ¬u1. Let's say the algorithm selects 3 and 4 , which yields the existential part φ′ = {e3, ¬e1 ∨ e3}, satisfiable by µ = {e1 ↦→ 0, e2 ↦→ 0, e3 ↦→ 1}, which satisfies the clauses 2 , 3 , and 4 . This means that the clause 2 must be selected in any next attempts, which is a contradiction with the previous condition because 2 and 3 cannot be selected at the same time due to the respective literals u1 and ¬u1. Hence the algorithm terminates and responds that the formula is true.

4 Generalizing for Arbitrary Prefixes: QESTO

Now we look at how the ideas for solving PQCNF by selection generalize to prefixes of arbitrary length. Hence, we assume that we are given a formula of the form Q1X1 . . .QnXn. φ, where Qi ∈ {∃, ∀}, Qn = ∃, and φ is a propositional formula in CNF. Recall that Qn = ∃ can be assumed as any universal variable at the end of the prefix can be removed.

For the sake of presentation, we adopt the game-theoretic point of view on QBF (cf. [Goultiaeva et al., 2011]). Any QBF in prenex closed form is seen as a game between the universal and existential player. The universal player tries to falsify the matrix while the existential tries to satisfy it. Under this perspective, a QBF is true if and only if there is a winning strategy for the existential player.

More precisely, a game consists of n rounds and in round i, the player Qi assigns a value to all the variables Xi. At the end of the game we evaluate the matrix φ by the accumulated assignment. The game is won by the universal player if the matrix evaluates to false, and it is won by the existential player if it evaluates to true. We say that there is a winning strategy for the existential player if the player can play so that he wins any game irregardless of how the universal player plays. Analogously, we define a winning strategy for the universal player. A formula is true if and only if there is a winning strategy for the existential player. Conversely, formula is false if and only if there is a winning strategy for the universal player.

Example 2. Consider the formula ∀u∃e. {¬u ∨ e, u ∨ ¬e}. The assignments {u ↦→ 0},{e ↦→ 1} represent a game where the existential player loses. The assignments {u ↦→ 1},{e ↦→ 1} represent a game where the existential player wins. There exists a winning strategy for the existential player, which is {e ↦→ u}. Hence, the formula is true.

Example 3. Consider the formula ∃e1∀u∃e2. {e1 ∨ u ∨ e2, e1 ∨ u ∨ ¬e2, ¬e1 ∨ ¬u ∨ e2, ¬e1 ∨ ¬u ∨ ¬e2}. The assignments {e1 ↦→ 0}, {u ↦→ 0},{e2 ↦→ 1} represent a game where the existential player loses. There exists a winning strategy for the universal player, which is {u ↦→ e1}. Hence, the formula is false.

The game-theoretic perspective lets us look at the selection-based solving symmetrically: the existential player tries to deselect clauses-so that the matrix becomes trueand the universal tries to select clauses-so that the matrix becomes false.

The following concepts concretize this idea. For each clause C ∈ φ and a quantification level k ∈ 1..n we introduce a variable skC , which indicates that the clause C is selected at the quantification level k. If skC is false, then we say that C is deselected at the quantification level k. Selecting and deselecting clauses is guided by the following rules:

1. A clause can be selected at level k if it was selected in all the previous levels and all its literals at the level k are set to false.
2. A clause can be deselected at level k if it was deselected in one of the previous levels or at least one of the literals at level k is set to true.

Observe that deselection behaves monotonically, i.e., once a clause is deselected it cannot be selected back again. This is unsurprising as once a clause is satisfied during the game, it remains satisfied.

The next thing to consider is how to encode the rules of the game. These are formulated as follows:

1. If all clauses C ∈ φ are deselected at some level k, the universal player loses.
2. If a clause C ∈ φ does not contain any literal l with lv(l) > k then the existential player loses if the clause is selected at level k.

These constraints correspond to the rules discussed above but they detect as soon as possible that a player has lost, i.e., once all clauses are satisfied, the universal player loses, and once the empty clause is derived, the existential player loses.

In its workings, the proposed algorithm is similar to the two-level one. Starting from the first level, the players select and deselect clauses based on the rules of the game. At each level i we maintain a condition C i, which blocks choices that lead to a loss of player Qi. These conditions are strengthened throughout the course of the algorithm. If a condition C i

Algorithm 2: QESTO: Solving PQCNF

1 for i ∈ 1..n do C i ←InitCondition(i) 2 qlev ← 1 3 S0 ←φ 4 while true do 5 if qlev = n + 1 then 6 conflict ← {snC ↦→ 0 | C ∈ φ} 7 Goto 11 8 α← ∧C∈Sqlev-1 sqlev-1 C ∧ ∧C/∈Sqlev-1 ¬sqlev-1 C 9 (µ, conflict) ← SAT(C qlev ∧α) 10 if µ = ⊥ then 11 (btlev, CL) ← Analyze(qlev, conflict) 12 if btlev = -1 then return (Qqlev = ∀) 13 C btlev ← C btlev ∧CL 14 qlev ← btlev 15 else 16 Sqlev = {C ∈ φ | µ(sqlev C ) = 1} 17 qlev ← qlev + 1

Algorithm 3: Condition Initialization

1 Function InitCondition (k) 2 if k = 1 then C1 ← {s1C ≜ ∧l∈C,lv(l)=1 ¬l | C ∈ φ} 3 else Ck ← {skC ≜ sk-1 C ∧ ∧l∈C,lv(l)=k ¬l | C ∈ φ} 4 if Qk = ∀ then Ck ←Ck ∧ ∨C∈φ sC 5 else 6 for C ∈ φ do 7 if there is no existential l ∈ C s.t. lv(l) > k then 8 C k ← C k ∧skC 9 return Ck

becomes unsatisfiable, it means that player Qi has lost under the current choices. Hence, we perform an analysis that tries to rectify some of the previous choices of the losing player. This consists in strengthening one of the conditions Ck for some k < i (we look more closely at the loss analysis later).

We name the algorithm QESTO (Qbf clausE SelecTion sOlver), which is listed in Algorithm 2. The algorithm uses the subroutine InitCondition (Algorithm 3) to initialize the conditions C i, i ∈ 1..n. Then QESTO continues by iterating the main loop (lns. 4-15) until the formula is solved. In each iteration the algorithm operates at a quantification level qlev. It is constructing sets Si, which consist of the clauses currently selected at level i. To simplify the presentation, we also introduce the set S0, which contains all the clauses in φ. To construct the set Sqlev we search for a model of the condition Cqlev restricted by the selections made so far (ln. 9). If this SAT call results in unsatisfiability, we backtrack to a quantification level chosen by the function Analyze. If the analysis fails, it returns the backtracking level -1 and the algorithm terminates-the formula is true iff the losing player

1 Function Analyze (qlev,conflict) 2 begin 3 Sc ← {C ∈ φ | ¬sqlev-1 C ∈ conflict} 4 E ← {l | l ∈ C,C ∈ Sc, l existential, lv(l) < qlev} 5 if E = ∅ then return (-1, ·) 6 btlev ←max({lv(l) | l ∈ E}) // btrack lev 7 CL ← ∨C∈Sc ¬sC // learned clause 8 return (btlev, CL)

is the universal player (ln. 12). One special case is treated at the beginning of the loop and this is when the quantification level is n + 1 (ln. 7). This means that the existential player satisfied all the clauses (recall that Qn = ∃), in which case we treat this situation as losing for the universal player.

4.1 Loss Analysis

Let us look more closely at how QESTO recovers from a loss of either of the players (lns. 11-14). Hence, we consider the situation where one of the conditions C i becomes unsatisfiable under the choices of selected clauses made by the players so far. This situation is analyzed and two outcomes are computed: the quantification level btlev where the algorithm returns to, and, a strengthening (a learned clause) for the condition Cbtlev that will prevent the losing player from making the same mistake again. This is somewhat analogous to how SAT solvers perform conflict analysis.

To get the best out of the underlying SAT solver, we rely on the ability of the SAT solver to provide us with a final conflict clause for unsatisfiable calls. For a formula ψ and a conjunction of literals α-designated as assumptions-final conflict clause conflict is a clause that contains only variables appearing in the assumptions α and it holds that ψ |= conflict. Which practically means that if ψ ∧ α is unsatisfiable, then ψ∧¬conflict is also unsatisfiable and ¬conflict is a subset of α that is sufficient to arrive to unsatisfiability.

In our scenario, at level qlev, the assumptions are made up of the variables sqlev-1 C and these signal to the SAT solver what choices were made so far. Hence, inspecting the clause conflict lets us infer with more precision which choices were responsible for the loss of the player at hand. 1

Note that instead of the final conflict clause technique, we could have analyzed the corresponding resolution refutation-if the solver produces one [Zhang and Malik, 2003] (in fact only the leaves of the refutation are needed, similarly as in the core extraction techniques, which appear in a number of applications of SAT).

As the loss analysis is quite different for the two players, we separate it into two respective procedures. The analysis for the existential player is quite straightforward and is presented in Algorithm 4. The final conflict clause conflict gives us a set of selected clauses Sc at level qlev-1 that lead to the

1 This approach also enables us to use incremental SAT [E´en and S¨orensson, 2003b] so that only the assumptions need to change when the same level is reached again.

1 Function Analyze (qlev,conflict) 2 begin 3 Sc ← {C ∈ φ | sqlev-1 C ∈ conflict} 4 S′c ← {C ∈ Sc | C not satisfied by an exist. lit} 5 if S′C = ∅ then return (-1, ·) 6 btlev ←max({k | skC = 0,C ∈ S′c , k universal}) R ← {C ∈ Sc | C sat. by an ex. lit at lev. > btlev} 7 return (btlev, ∨C∈(Sc∖R) sbtlev C )

unsatisfiability of Cqlev. To rectify this, the existential player must ensure that at least one of these clauses is deselected, the next time we get to the level qlev. For the existential player to deselect one of the clauses at a level l < qlev there must be an existential literal at that level. Otherwise, the existential player cannot influence the state of the clause. Hence, the backtrack level is calculated as the maximum over the levels of existential literals in the clauses Sc that are at a lower level than qlev. If there are no such literals, then the existential player cannot rectify the loss and the formula is solved (it is false). The learned clause is constructed so that it forces the deselection of at least one clause from the problematic set Sc.

The analysis for the universal player is inverse (Algorithm 5). At the time of a loss, there is some set of clauses Sc that are deselected and are causing the universal player to lose at the level qlev. If a clause is deselected by the existential player, the universal player cannot do anything about it. So we shift our attention to clauses S′ l ⊆ Sc that are deselected by the universal player, i.e., satisfied by a universal literal. If there are no such clauses, the universal player cannot rectify the loss and therefore the formula is true. Otherwise, the backtrack level is computed as the maximum over the levels where the clauses in S′c were deselected. Now we could define the learned clause as ∨C∈Sc sbtlev C , but we can do better if we realize that the existential player can always repeat any choices that he has made after btlev. Hence, if the existential player was able to deselect a clause after btlev, he can do so again next time and therefore we remove these clauses from the learned clause.

4.2 Comparison to Other Approaches

In the context of a CNF formula ψ, a maximal satisfiable set (MSS) is a set of clauses ψ′ ⊆ ψ that is satisfiable and adding any clause from ψ to it makes it unsatisfiable. A complement ψ \ ψ′ of such set is called a minimal correction set (MCS). Conversely, minimal unsatisfiable set (MUS) is a set ψ′ ⊆ ψ that is unsatisfiable and removing any of its clauses makes it satisfiable. It is well known that the set of all MUSes is the set of all minimal hitting sets of MCSes (and also the other way around). This duality of hitting sets is useful for calculating all MUSes or MUSes with certain properties, which has been exploited in a number of works [Liffiton and Sakallah, 2008; Previti and MarquesSilva, 2013]. Moreover, algorithms based on iteratively analyzing implicitly represented hitting sets find a growing number of applications [Karp, 2010; Chandrasekaran et al., 2011; Davies and Bacchus, 2011; Stern et al., 2012; MorenoCenteno and Karp, 2013; Davies and Bacchus, 2013a; 2013b; Slaney, 2014]. The two-level approach we propose explicitly links this paradigm to QBF solving. Indeed, solving a twolevel QBF (∀∃) can be phrased as a search for an MUS comprising of the clauses containing only the existential part. The universal part, imposes "rules" on which clauses may appear in an unsatisfiable set. Indeed, any clauses C1,C2 that contain universal literals y ∈ C1, ¬y ∈ C2 are never considered together. Algorithm 1 then iterates over satisfiable subsets of the matrix φ and requires that a complement of the satisfiable set is selected next time, which is consistent with the idea that MUSes are hitting sets of MCSes. Note that our algorithm does not to go over maximally satisfiable sets but it only requires satisfiable sets. Similarly, we do not require a minimal unsatisfiable set, but simply any unsatisfiable set. In our implementation, however, we make sure that the decision polarities of the selection variables in the SAT solver are set so that the SAT solver tends to find larger satisfiable sets.

The two-level approach can also be related to the counterexample guided abstraction refinement algorithm AReQS [Janota and Marques-Silva, 2011]. Indeed, the selector variables in our approach (Algorithm 1) can be seen as the Tseitin variables introduced in AReQS. We should stress, however, that the generalization of AReQS-RAReQS [Janota et al., 2012]-is already completely different from our generalization (Algorithm 2). In RAReQS the generalization is done by recursion and the algorithm introduces a number of fresh variables throughout its course. While QESTO and RAReQS are similar for the two-quantification-level case, they are vastly different in the general case. Unlike RAReQS, QESTO does not introduce fresh variables as the algorithm progresses-selector variables are introduced at the very beginning and their number is bound. In this sense, our proposed algorithm differentiates itself from other expansionbased algorithms that convert the given formula into a SAT problem [Benedetti, 2004; Biere, 2004]. Further, RAReQS may create an exponential number of solvers due to the recursive calls while in QESTO, the number of solvers is always linear in the number of quantification levels (and it is fixed).

In its skeleton, our algorithm is similar to the conflict/solution-driven learning algorithms [Giunchiglia et al., 2001; Zhang and Malik, 2002]; in the sense that it starts from the outermost quantification level, progresses to the inwards quantification level and backtracks whenever needed. It is, however, very different in how the algorithm is constructed and how learning is performed. Indeed, the building blocks of QESTO are a SAT solver and selection variables, which let us navigate the search space. This approach lets us devise a learning procedure anchored in the SAT solver's ability to analyze unsatisfiability (the final conflict clause), rather than building a dedicated unit propagator and learner; this gives us a strong engineering advantage.

5 Experimental Evaluation

We have implemented a prototype of Algorithm 2 named Qesto. The prototype used for the evaluation was implemented in C ++ and the SAT solver minisat 2.2 [E´en and S¨orensson, 2003a] was used. The experimental results were carried out on Linux machines with Intel Xeon 5160 3GHz processors and 4GB of memory. The time limit was set to 800 s and the memory limit to 2GB.

For the evaluation we used the QBFLIB benchmark suite used in the 2014 QBF Gallery 2 and the benchmarks from the 2QBF track of the 2010 QBF Evaluation. All the instances were preprocessed by the preprocessor bloqqer [Biere et al., 2011] and instances solved by the preprocessor were excluded from the evaluation. For comparison we have chosen a set of representative state-of-the-art QBF solvers. The conflict/solution-driven solver DepQBF [Lonsing and Biere, 2010]; the CEGAR-based solver RAReQS and its 2QBF version AReQS [Janota and Marques-Silva, 2011; Janota et al., 2012]; and the non-CNF solver GhostQ [Klieber et al., 2010]. Since GhostQ is a non-CNF solver, it was run on the unpreprocessed benchmarks as the solver's reverse engineering procedure benefits from their structure; it is also how it was run in the competition.

Table 1 summarizes the number of solved instances for the considered solvers. Figures 2 and 1 show cactus plots for the respective benchmark sets (cactus plots consist of points (x, y) meaning there are x instances solved in y sec). Since the QBFLIB cactus plot has a rather a long tail, the plot contains only those instances that were not solved within 60 seconds by all the solvers.

2 http://www.kr.tuwien.ac.at/events/qbfgallery2013/benchmarks/ eval2012r2.tar.7z

GhostQ clearly dominates in the QBFLIB suite and it is followed by our prototype Qesto. There is a difference of only one solved instance between the solvers DepQBF and RAReQS. The success of the non-CNF solver GhostQ, confirms the well-known fact that representing QBF problems as CNF is harmful for solving [Ans´otegui et al., 2005; Klieber et al., 2010; Goultiaeva and Bacchus, 2010] (we return to the topic in our future work discussion).

In the 2QBF suite our prototype Qesto solves the most instances. However, AReQS solves just 1 instance less, which comes as no surprise as the algorithms are closely related (see Section 4.2). Interestingly, GhostQ performs rather poorly on this set of benchmarks, which suggests that our prototype gives a higher degree of robustness when compared to others. More detailed presentation of the results can be found on the authors' website 3 .

6 Summary and FutureWork

This paper describes an algorithm QESTO to solve QBF in prenex form with a matrix in CNF. The algorithm is first presented in its two-level form (∀∃), which is shown to have a clear correspondence to implicit hitting sets, which appear in a number of applications of artificial intelligence. This two-level approach is also linked to the recent CEGAR-based two-level QBF algorithm AReQS [Janota and Marques-Silva, 2011]. The second half of the paper generalizes the twolevel approach to QBFs with arbitrary number of quantification levels, giving rise to the QESTO algorithm. QESTO is an entirely novel approach to QBF solving and the experimental evaluation suggests that it is quite robust. It should also be noted that QESTO is quite advantageous from the engineering perspective since a SAT solver is utilized in a blackbox fashion. QESTO is also quite interesting from the theoretical perspective as it can be seen as a generalization of duality hitting set principle for PSPACE.

On the QBFLIB benchmarks QESTO was outperformed by the non-CNF solver GhostQ [Klieber et al., 2010]. This suggests that it would be worthwhile investigating how QESTO could be applied to non-CNF formulas. We believe that this should be possible as this was already successfully done for conflicts/solution-driven learning algorithms [Zhang, 2006; Goultiaeva et al., 2013]. Other improvements, such as pure literals or variable dependencies, are also considered for future work.

3 http://sat.inesc-id.pt/%7Emikolas/sw/qesto/