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 27 articles , 1 standard article )

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

1 2 next

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

1 2 next

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