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

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

  1. Balyo, Tomáš; Lonsing, Florian: Hordeqbf: A modular and massively parallel QBF solver (2016)
  2. Jordan, Charles; Kaiser, Lukasz; Lonsing, Florian; Seidl, Martina: $\mathsfMPIDepQBF$: towards parallel QBF solving without knowledge sharing (2014)
  3. Weihua, Su; Minghao, Yin; Jianan, Wang; Junping, Zhou: Message passing algorithm for solving QBF using more reasoning (2013)
  4. Goultiaeva, Alexandra; Bacchus, Fahiem: Exploiting circuit representations in QBF solving (2010)
  5. Goultiaeva, Alexandra; Iverson, Vicki; Bacchus, Fahiem: Beyond CNF: a circuit-based QBF solver (2009)
  6. Jussila, Toni; Biere, Armin: Compressing BMC encodings with QBF. (2007)
  7. Arieli, Ofer; Denecker, Marc; Van Nuffelen, Bert; Bruynooghe, Maurice: Computational methods for database repair by signed formulae (2006)
  8. Alur, Rajeev; Madhusudan, P.; Nam, Wonhong: Symbolic computational techniques for solving games (2005)
  9. Alur, Rajeev; Madhusudan, P.; Nam, Wonhong: Symbolic computational techniques for solving games (2005)
  10. Egly, Uwe; Pichler, Reinhard; Woltran, Stefan: On deciding subsumption problems (2005)
  11. Giunchiglia, Enrico; Narizzano, Massimo; Tacchella, Armando: Backjumping for quantified Boolean logic satisfiability (2003)
  12. Madhusudan, P.; Nam, Wonhong; Alur, Rajeev: Symbolic computational techniques for solving games (2003)
  13. Madhusudan, P.; Nam, Wonhong; Alur, Rajeev: Symbolic computational techniques for solving games. (2003)
  14. Giunchiglia, Enrico; Narizzano, Massimo; Tacchella, Armando: QUBE: A system for deciding quantified Boolean formulas satisfiability (2001)