QUBE

QuBE: A System for Deciding Quantified Boolean Formulas Satisfiability. Deciding the satisfiability of a Quantified Boolean Formula (QBF) is an important research issue in Artificial Intelligence. Many reasoning tasks involving planning [1], abduction, reasoning about knowledge, non monotonic reasoning [2], can be directly mapped into the problem of deciding the satisfiability of a QBF. In this paper we present QuBE, a system for deciding QBFs satisfiability. We start our presentation in § 2 with some terminology and definitions necessary for the rest of the paper. In § 3 we present a high level description of QuBE’s basic algorithm. QuBE’s available options are described in § 4. We end our presentation in § 5 with some experimental results showing QuBE effectiveness in comparison with other systems. QuBE, and more information about QuBE, are available at www.mrg.dist.unige.it/star/qube.


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. Balabanov, Valeriy; Jiang, Jie-Hong Roland; Scholl, Christoph; Mishchenko, Alan; Brayton, Robert K.: 2QBF: challenges and solutions (2016)
  2. Balyo, Tomáš; Lonsing, Florian: Hordeqbf: A modular and massively parallel QBF solver (2016)
  3. Janota, Mikoláš; Klieber, William; Marques-Silva, Joao; Clarke, Edmund: Solving QBF with counterexample guided refinement (2016)
  4. Janota, Mikoláš; Marques-Silva, Joao: Expansion-based QBF solving versus Q-resolution (2015)
  5. Jordan, Charles; Kaiser, Lukasz; Lonsing, Florian; Seidl, Martina: (\mathsfMPIDepQBF): towards parallel QBF solving without knowledge sharing (2014)
  6. Cook, Byron; Kroening, Daniel; Rümmer, Philipp; Wintersteiger, Christoph M.: Ranking function synthesis for bit-vector relations (2013)
  7. Weihua, Su; Minghao, Yin; Jianan, Wang; Junping, Zhou: Message passing algorithm for solving QBF using more reasoning (2013)
  8. Wintersteiger, Christoph M.; Hamadi, Youssef; De Moura, Leonardo: Efficiently solving quantified bit-vector formulas (2013)
  9. Biere, Armin; Lonsing, Florian; Seidl, Martina: Blocked clause elimination for QBF (2011)
  10. Janota, Mikoláš; Marques-Silva, Joao: Abstraction-based algorithm for 2QBF (2011)
  11. Goultiaeva, Alexandra; Bacchus, Fahiem: Exploiting circuit representations in QBF solving (2010)
  12. Goultiaeva, Alexandra; Iverson, Vicki; Bacchus, Fahiem: Beyond CNF: a circuit-based QBF solver (2009)
  13. Lonsing, Florian; Biere, Armin: A compact representation for syntactic dependencies in QBFs (2009)
  14. Jussila, Toni; Biere, Armin: Compressing BMC encodings with QBF (2007)
  15. Kleine Büning, Hans; Subramani, K.; Zhao, Xishun: Boolean functions as models for quantified Boolean formulas (2007)
  16. Sofronie-Stokkermans, Viorica: On unification for bounded distributive lattices (2007)
  17. Arieli, Ofer; Denecker, Marc; Van Nuffelen, Bert; Bruynooghe, Maurice: Computational methods for database repair by signed formulae (2006)
  18. Alur, Rajeev; Madhusudan, P.; Nam, Wonhong: Symbolic computational techniques for solving games (2005) ioport
  19. Alur, Rajeev; Madhusudan, P.; Nam, Wonhong: Symbolic computational techniques for solving games (2005) ioport
  20. Egly, Uwe; Pichler, Reinhard; Woltran, Stefan: On deciding subsumption problems (2005)

1 2 next