QuBE++

In this paper we describe QuBE++, an efficient solver for Quantified Boolean Formulas (QBFs). To the extent of our knowledge, QuBE++ is the first QBF reasoning engine that uses lazy data structures both for unit clauses propagation and for pure literals detection. QuBE++ also features non-chronological backtracking and a branching heuristic that leverages the information gathered during the backtracking phase. Owing to such techniques and to a careful implementation, QuBE++ turns out to be an efficient and robust solver, whose performances exceed those of other state-of-the-art QBF engines, and are comparable with the best engines currently available on SAT instances.


References in zbMATH (referenced in 24 articles , 1 standard article )

Showing results 1 to 20 of 24.
Sorted by year (citations)

1 2 next

  1. Cook, Byron; Kroening, Daniel; Rümmer, Philipp; Wintersteiger, Christoph M.: Ranking function synthesis for bit-vector relations (2013)
  2. Weihua, Su; Minghao, Yin; Jianan, Wang; Junping, Zhou: Message passing algorithm for solving QBF using more reasoning (2013)
  3. Wintersteiger, Christoph M.; Hamadi, Youssef; De Moura, Leonardo: Efficiently solving quantified bit-vector formulas (2013)
  4. Eirinakis, Pavlos; Ruggieri, Salvatore; Subramani, K.; Wojciechowski, Piotr: A complexity perspective on entailment of parameterized linear constraints (2012)
  5. Janota, Mikoláš; Klieber, William; Marques-Silva, Joao; Clarke, Edmund: Solving QBF with counterexample guided refinement (2012)
  6. Brihaye, Thomas; Bruyère, Véronique; Doyen, Laurent; Ducobu, Marc; Raskin, Jean-Francois: Antichain-based QBF solving (2011)
  7. Janota, Mikoláš; Marques-Silva, Joao: Abstraction-based algorithm for 2QBF (2011)
  8. Brummayer, Robert; Lonsing, Florian; Biere, Armin: Automated testing and debugging of SAT and QBF solvers (2010)
  9. Cook, Byron; Kroening, Daniel; Rümmer, Philipp; Wintersteiger, Christoph M.: Ranking function synthesis for bit-vector relations (2010)
  10. Pulina, Luca; Tacchella, Armando: An empirical study of QBF encodings: from treewidth estimation to useful preprocessing (2010)
  11. Lewis, Matthew; Marin, Paolo; Schubert, Tobias; Narizzano, Massimo; Becker, Bernd; Giunchiglia, Enrico: PaQuBE: distributed QBF solving with advanced knowledge sharing (2009)
  12. Lonsing, Florian; Biere, Armin: A compact representation for syntactic dependencies in QBFs (2009)
  13. Narizzano, Massimo; Peschiera, Claudia; Pulina, Luca; Tacchella, Armando: Evaluating and certifying QBFs: a comparison of state-of-the-art tools (2009)
  14. Jussila, Toni; Biere, Armin: Compressing BMC encodings with QBF. (2007)
  15. Arieli, Ofer; Denecker, Marc; Van Nuffelen, Bert; Bruynooghe, Maurice: Computational methods for database repair by signed formulae (2006)
  16. Giunchiglia, E.; Narizzano, M.; Tacchella, A.: Clause/Term resolution and learning in the evaluation of quantified Boolean formulas (2006)
  17. Alur, Rajeev; Madhusudan, P.; Nam, Wonhong: Symbolic computational techniques for solving games (2005)
  18. Alur, Rajeev; Madhusudan, P.; Nam, Wonhong: Symbolic computational techniques for solving games (2005)
  19. Benedetti, Marco: Quantifier trees for QBFs (2005)
  20. Egly, Uwe; Pichler, Reinhard; Woltran, Stefan: On deciding subsumption problems (2005)

1 2 next


Further publications can be found at: http://www.star.dist.unige.it/index.php?option=com_jombib&Itemid=42