In this short paper, we describe QBF solvers from the latest QBFEval that were based on the SAT-to-SAT solver. We present the main ideas behind the solvers and discuss their strengths and weaknesses. - QSTS: This version represents our solver without any out-of-the-box preprocessors. - XB-QSTS: This version represents our solver with both QXBF [12] and BLOQQER [2] preprocessors. - XB-BID-QSTS: This version integrates our solver with BREAKID, an award-winning symmetry breaker [4], in addition to QXBF and BLOQQER.
SAT-TO-SAT is a recently introduced solver that integrates several SAT solvers to solve problems arbitrarily high in the polynomial hierarchy [7, 3]. In order to evaluate its performance, we submitted three versions of this solver to the latest QBF evaluation: -interpretation is a mapping ! ft; f ; ug, where u denotes unknown. We often identify a partial -interpretation J with a set of tuples pv with p 2 ; v 2 ft; f g (with each atom occurring at most once), meaning that J assigns all atoms occurring in this set to their corresponding values, and all others to unknown. This allows us to define the “union” of two interpretations. E.g., if and are disjoint, I is a (partial) -interpretation and J a (partial) -interpretation, we use I [ J to interpret symbols in in the same way as I and symbols in in the same way as J . If I and J are two -interpretations, we will use the expression I [ J only if I [ J indeed defines a partial interpretation (i.e., does not contain both pt and pf ).
Formulas. Propositional formulas are recursively built from atoms p; q; r; : : : using connectives ^, _ and :. A propositional theory is a collection of propositional formulas that implicitly represents their conjunction. A singleton theory f g is sometimes shown as . A propositional formula is a -formula if its atoms are in . A literal is an atom or its negation. A clause is a disjunction of literals. A formula is in Conjunctive Normal Form (CNF) if it is a conjunction of clauses. A sub-formula occurs positively (resp. negatively) if it is within the scope of an even (resp. odd) number of negations.
A quantified Boolean formula (QBF) is built using the same recursive rules, but also using quantifiers 8 and 9 over propositional atoms. Similar to propositional theories, we define a QBF theory to be a collection of quantified Boolean formulas. A -QBF is a QBF with free symbols belonging to . A -QBF with = fg is called a QBF sentence. We use 9 : ' to abbreviate 9p1 : : : 9pn : ' if = fp1; : : : ; png. For QBF ', we use '( ) to denote that '’s free symbols are all in , i.e., ' is a -QBF. A prenex QBF is a QBF in which all quantifiers are in the front, i.e., a sequence of quantifiers followed by a propositional formula. The QDIMACS format is a numerical format to describe prenex QBFs in which the propositional formula is in CNF. QDIMACS is the de-facto standard for representing QBF instances.
Satisfiability Relation for QBFs. The satisfiability relation between -interpretations I and a -QBFs ', denoted by I j= ', is defined recursively in the standard way: (i) I j= p if I (p) = t; (ii) I j= :' if I 6j= '; (iii) I j= ' ^ '0 (resp. I j= ' _ '0) if I j= ' and (resp. or) I j= '0; (iv) I j= 8x : ' (resp. I j= 9x : ') if (I [ fxtg) j= ' and (resp. or) (I [ fxf g) j= '. For a (partial) -interpretation I and -QBF ', we call ' I -satisfiable if ' has a model that extends I and I -unsatisfiable otherwise. 3
SAT-TO-SAT This section discusses the high-level ideas behind SAT-TO-SAT solver. The first subsection describes the inner workings of the core solver. The second subsection describes preprocessing techniques used to optimize the input for our solver. 3.1
SAT-TO-SAT
Nested SAT Solvers. SAT-TO-SAT starts from a simple idea that has been around for
years in the QBF community, i.e., nesting of SAT solvers [16, 9, 15]. The idea is easiest
to explain in the case of a 2QBF. For a theory of the form = 8 : '1 ) 9 : '2
with '1 and '2 in CNF, we can rewrite as :9 : ['1 ^ :9 : '2]. The idea is that
the first SAT solver tries to find an assignment I for to satisfy '1 (i.e., essentially,
searching for a witness to the falsify ) and, as soon as such an assignment I is found,
the second solver searches for an assignment I0 to such that I [ I0 is a model for '2.
In case no assignment I0 is found, I indeed witnesses falsity of . But, if I0 is found,
we analyze '2 to learn a new clause C over that falsifies I and is a consequence
of :9 : '2. We then add C to the theory of the first solver and continue searching
for a new assignment I. This idea is very effective as (
Quantifier-Independent Decision Ordering. To the best of our knowledge, a limitation that all contemporary QBF solvers share is that, when solving QBF theories, the decision ordering on quantified variables is bound by the quantification order. That is, inner level variables are decided on only after all outer level variables are assigned a value. For example, in the formula 9x9y 8p8q (x; y; p; q), the variables p and q cannot be decided upon unless the truth values of both x and y have been assigned. This restriction is present in nested SAT solvers (the second SAT solver can only be called if a complete assignment for is found), non-CNF solvers such as GHOSTQ [10], counterexample guided abstraction refinement (CEGAR) solvers such as RAREQS [8], and QDPLL-based solvers such as DEPQBF [11].
Such a dependence between variable decision ordering and quantification level is problematic because it means that relevant conflicts and/or solutions in QBF theories cannot be found unless all (possibly irrelevant) outer-level variables have a value. Solvers such as DEPQBF partly mitigate this problem by extracting (static) variable dependency information out of QBF theories. While a valuable approach, such solutions neither address the root cause of the problem nor are they general enough to apply to all QBF theories. The SAT-TO-SAT approach is based on a new method to make variable decision ordering independent of the quantification structure of those variables. The intuition is that when the outermost solver arrives in a situation with a partial assignment for (following the notation introduced in the paragraph on nested solvers above), it can already call the nested solver. The nested solver should then search for an assignment to that models '2 for every interpretation of the unassigned variables in . If such an assignment is found, a conflict clause can be added to the theory of the outermost solver. The search for such an assignment would in general require major modifications to the solver. Instead, we implemented this in a different way. We show that certain theory transformation, that include duplication of the atoms in , achieve the same effect. This method has been detailed for the case of 2QBF by Janhunen et al. [7] and extended to the general case by Bogaerts et al. [3]. 3.2
Definition Extraction. We detect definitions and pull them to the outermost level possible. This technique is similar to reverse Tseitin engineering in GhostQ [6] and is based on the observation that the following two formulas are always equivalent: '(x) = 9y : [ 1 ^ :9z : 9z0 : (z0 ,
2(x; y)) ^ 3)]: '(x) = 9y : 9z0 : [ 1 ^ (z0 , 2(x; y)) ^ :9z :
Transforming the first formula to the second reduces the level of variable z0 by moving it to outer levels of a QBF theory. Repeated applications of this transformation guarantee that all definitions are moved to the outermost level possible. Our current implementation only extracts definitions of the form z0 , Vfl1; : : : lkg or z0 , Wfl1; : : : lkg. Identifying other Boolean definitions is a topic for future research.
Extracting definitions leads to QBF theories with a richer vocabulary for the outerlevel solvers. Since conflict clauses are the only means of passing information between SAT solvers in SAT-TO-SAT, having a rich vocabulary in the outer solver means that information can be passed along more succinctly. For instance, when z = Vfl1; : : : ; lng and z0 = Vfl10; : : : ; lm0g, the conflict clause z _ z0 summarizes n m different conflict clauses li _ lj0 (for 1 i n and 1 j m). Hence, enriching the vocabulary of outer-level solver with variables z and z0 allows us to reduce the number of conflict clauses passed from the inner-level solver to the outer-level solver.
Unit and Equality Propagation. When extracting definitions z , Wfl1; : : : ; lkg or z , Vfl1; : : : ; lkg, we look for special cases when k = 0 or k = 1. When k = 0, we propagate the forced value of z to obtain a simpler QBF (unit propagation) and, when k = 1, we replace all occurrences of z with l1 (equality propagation). Propagating unit and/or equal literals sometimes leads to vast simplifications in a QBF instance. Extended Learning Vocabulary. Sometimes when the internal solver in SAT-TO-SAT finds a model, there are several alternatives to constructing a conflict clause. This happens when some clauses at level k depend on more than one literal from levels below k (i.e., outer levels). In such cases, for each clause C with more than one variable from outer levels, we can introduce a new auxiliary variable vC which is equivalent to the disjunction of all literals in C that belong to the outer level. Similar to definition extraction, the richer learning vocabulary for outer level solver is expected to summarize many conflict clauses into one. This, in turn, is a limited type of extended resolution [17] that leads to stronger learned clauses. In SAT-TO-SAT, introduction of such auxiliary variables happens statically, in a preprocessing phase.
This idea is not new and has been recently studied in two independent papers [9, 15]. Janota et al. [9] calls this idea clause selection.
Weakened Definitions. Our previous QBF pre-processing techniques introduced several definitions. Depending on how the defined variables are used, some definitions can be weakened, essentially only adding one of the two implications. By analyzing the dependency graph of the definition structure, we can determine which formulas depend positively or negatively on given variables and, in a sound way, drop one direction of the introduced definitions.
Symmetry Breaking. After the preprocessing techniques described above, we detect and break symmetries of the QBF theory similar to Audemard et al. [1]. That is, for each quantifier alternation (which also corresponds to each SAT solver that we create), we fix all variables from other levels and, using symmetry breaking tool BREAKID [4], we check if there exist some automorphisms over the set of variables at the current level. If such automorphisms are found, we add the symmetry breaking clauses generated by BREAKID to the solver for that level. Contrary to the work by Audemard et al. [1], our symmetry breaking techniques do not require any modifications to the actual solver: they are based merely on preprocessing. 4 4.1
Not all optimizations were applied in all versions of our solvers submitted to QBFEval 2016. We experimentally tested which combinations of optimizations work well together, as well with other existing QBF preprocessors and submitted the following three configurations to the QBF Evaluation: – QSTS: Our QSTS submission is comprised of our bare-bone solver (i.e., the nested SAT solver architecture of SAT-TO-SAT plus its quantifier-independent decision ordering feature) as well as following optimizing transformations: definition extraction, unit and equality propagation, and weakened definitions. – XB-QSTS: Our XB-QSTS submission is similar to QSTS except that it disables the quantifier-independent decision ordering but uses QXBF and BLOQQER preprocessors in order to simplify a given QBF instance. – XB-BID-QSTS: Our XB-BID-QSTS submission is similar to XB-QSTS except that it also uses symmetry breaking. 4.2
For experimental results, we ran QBFEval 2016 instances (which consists of 825 formulas in Prenex CNF format) on a machine with a 32-core Intel® Xeon® CPU E5-4650 clocked at 2.70GHz, with 256GB of memory, and running Ubuntu Linux with kernel version 3.13.0-91. We limited the resources available for each process to one CPU core, at most 4GB of memory, and at most 600 seconds of time.
Under the above conditions, we ran the three different configurations of our solver (i.e., QSTS, XB-QSTS and XB-BID-QSTS) and compared them with RAREQS+BLOQQER (i.e., RAREQS QBF solver plus BLOQQER preprocessor), DEPQBF (under its best configuration, i.e., DEPQBF-V2, as it participated in the QBFEval) and GHOSTQCEGAR. We used all 825 instances that were made available in the Prenex CNF track. Table 1 summarizes our results.
As Table 1 shows, RAREQS+BLOQQER shows the best performance among all these solvers. This result is consistent with competition results of QBFEval 2016 in which RAREQS+BLOQQER was ranked first. Also, the total number of solved QBF instances for RAREQS+BLOQQER in our experiments is almost indistinguishable from competition results (hence, further confirmation for the results we report here). That is, RAREQS+BLOQQER solved 640 QBF instances in QBFEval 2016 and 639 instances in our experiments. Our experiments also show consistency with QBFEval 2016 in the case of XB-QSTS (our only bug-free submission to QBFEval 2016), DEPQBF-V2 and
Solver RAREQS+BLOQQER
XB-BID-QSTS
XB-QSTS
DEPQBF-V3 GHOSTQ-CEGAR
QSTS
GHOSTQ-CEGAR solvers. That is, the difference between the total number of solved instances in our experiments and those reported by QBFEval 2016 is at most eight.
As indicated by Table 1, our corrected version of XB-BID-QSTS performs better than our XB-QSTS solver, and they both perform better than all other solvers except RAREQS+BLOQQER. Hence, we conclude that we could have received both the 2nd and the 3rd ranks in QBFEval 2016 if we had managed to submit a correctly working version of XB-BID-QSTS. 5
We briefly discussed our contribution, SAT-TO-SAT, to the latest QBF evaluation. The main difference between SAT-TO-SAT and other QBF solvers is its ability to make variable decision ordering independent from the quantifier prefix. We conclude that, while still in an early development stage, SAT-TO-SAT is a promising solver capable og competing with the best QBF solvers on Prenex CNFs. Additionally, our experiments with bug-fixed versions of our solver showed the effectiveness of symmetry breaking. That is, a bug-free submission of XB-BID-QSTS would have been ranked 2nd in the Prenex-CNF track of QBFEval 2016 after RAREQS+BLOQQER and before XB-QSTS. Acknowledgments. This work is generously supported by the Finnish Center of Excellence in Computational Inference Research (COIN) funded by the Academy of Finland (under grant #251170). 3. Bogaerts, B., Janhunen, T., Tasharrofi, S.: Solving QBF instances with nested SAT solvers.
In: Darwiche, A. (ed.) Beyond NP, Papers from the 2016 AAAI Workshop, Phoenix, Arizona,
USA, February 12, 2016. AAAI Workshops, vol. WS-16-05. AAAI Press (2016), http:
//www.aaai.org/ocs/index.php/WS/AAAIW16/paper/view/12603
4. Devriendt, J., Bogaerts, B., Bruynooghe, M., Denecker, M.: Improved static symmetry
breaking for SAT. In: Creignou, N., Berre, D.L. (eds.) Theory and Applications of Satisfiability
Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016,
Proceedings. Lecture Notes in Computer Science, vol. 9710, pp. 104–122. Springer (2016),
http://dx.doi.org/10.1007/978-3-319-40970-2_8
5. Feydy, T., Stuckey, P.J.: Lazy clause generation reengineered. In: Gent, I.P. (ed.)
Principles and Practice of Constraint Programming - CP 2009, 15th International Conference, CP
2009, Lisbon, Portugal, September 20-24, 2009, Proceedings. Lecture Notes in Computer
Science, vol. 5732, pp. 352–366. Springer (2009), http://dx.doi.org/10.1007/
978-3-642-04244-7_29
6. Goultiaeva, A., Bacchus, F.: Recovering and utilizing partial duality in QBF. In: Theory and
Applications of Satisfiability Testing - SAT 2013 - 16th International Conference, Helsinki,
Finland, July 8-12, 2013. Proceedings. pp. 83–99 (2013), http://dx.doi.org/10.
1007/978-3-642-39071-5_8
7. Janhunen, T., Tasharrofi, S., Ternovska, E.: Sat-to-sat: Declarative extension of SAT solvers
with new propagators. In: Schuurmans, D., Wellman, M.P. (eds.) Proceedings of the
Thirtieth AAAI Conference on Artificial Intelligence, February 12-17, 2016, Phoenix, Arizona,
USA. pp. 978–984. AAAI Press (2016), http://www.aaai.org/ocs/index.php/
AAAI/AAAI16/paper/view/12323
8. Janota, M., Klieber, W., Marques-Silva, J., Clarke, E.M.: Solving QBF with counterexample
guided refinement. In: Cimatti, A., Sebastiani, R. (eds.) Theory and Applications of
Satisfiability Testing - SAT 2012 - 15th International Conference, Trento, Italy, June 17-20, 2012.
Proceedings. Lecture Notes in Computer Science, vol. 7317, pp. 114–128. Springer (2012),
http://dx.doi.org/10.1007/978-3-642-31612-8_10
9. Janota, M., Marques-Silva, J.: Solving QBF by clause selection. In: Yang, Q., Wooldridge,
M. (eds.) Proceedings of the Twenty-Fourth International Joint Conference on Artificial
Intelligence, IJCAI 2015, Buenos Aires, Argentina, July 25-31, 2015. pp. 325–331. AAAI
Press (2015), http://ijcai.org/Abstract/15/052
10. Klieber, W., Sapra, S., Gao, S., Clarke, E.M.: A non-prenex, non-clausal QBF solver with
game-state learning. In: Theory and Applications of Satisfiability Testing - SAT 2010, 13th
International Conference, Proceedings. pp. 128–142 (2010), http://dx.doi.org/10.
1007/978-3-642-14186-7_12
11. Lonsing, F., Biere, A.: DepQBF: A dependency-aware QBF solver. Journal of
Satisfiability (JSAT) 7(