Quaffle: Quantified Boolean Formula Evaluator with Learning Quaffle is an experimental QBF solver. The idea of this solver is described in the following two papers: L. Zhang and S. Malik, ”Towards Symmetric Treatment of Conflicts And Satisfaction in Quantified Boolean Satisfiability Solver”, Proceedings of 8th International Conference on Principles and Practice of Constraint Programming (CP2002). Ithaca, NY, Sept. 2002. [PDF] L. Zhang and S. Malik, ”Conflict Driven Learning in a Quantified Boolean Satisfiability Solver”, Proceedings of International Conference on Computer Aided Design (ICCAD2002), San Jose, CA, Nov. 2002. [PDF] Source code for Quaffle is available for download here . Please read the lincence agreement on the top of each file. The code is experimental and for algorithm evaluation only. It should compile under most Unix/Linux machines using g++. The run time comparison of Quaffle with two other state of the art QBF solvers QuBE and Semprop is available here. The benchmarks are obtained from QBFLib. The experiments were carried out on a Dell PowerEdge 1500sc with 1133Mhz PIII CPU and 1G memory. Time out limit is 600 seconds.

References in zbMATH (referenced in 68 articles )

Showing results 21 to 40 of 68.
Sorted by year (citations)
  1. Janota, Mikoláš; Marques-Silva, Joao: Expansion-based QBF solving versus Q-resolution (2015)
  2. Tu, Kuan-Hua; Hsu, Tzu-Chien; Jiang, Jie-Hong R.: QELL: QBF reasoning with extended clause learning and levelized SAT solving (2015)
  3. Balabanov, Valeriy; Jiang, Jie-Hong R.: Unified QBF certification and its applications (2012)
  4. Goldberg, Eugene; Manolios, Panagiotis: SAT-solving based on boundary point elimination (2011)
  5. Brummayer, Robert; Lonsing, Florian; Biere, Armin: Automated testing and debugging of SAT and QBF solvers (2010)
  6. Giunchiglia, Enrico; Marin, Paolo; Narizzano, Massimo: sQueezeBF: an effective preprocessor for QBFs based on equivalence reasoning (2010)
  7. Klieber, William; Sapra, Samir; Gao, Sicun; Clarke, Edmund: A non-prenex, non-clausal QBF solver with game-state learning (2010)
  8. Kontchakov, Roman; Wolter, Frank; Zakharyaschev, Michael: Logic-based ontology comparison and module extraction, with an application to DL-Lite (2010)
  9. Lonsing, Florian; Biere, Armin: Integrating dependency schemes in search-based QBF solvers (2010)
  10. Pulina, Luca; Tacchella, Armando: An empirical study of QBF encodings: from treewidth estimation to useful preprocessing (2010)
  11. Egly, Uwe; Seidl, Martina; Woltran, Stefan: A solver for QBFs in negation normal form (2009)
  12. Lonsing, Florian; Biere, Armin: A compact representation for syntactic dependencies in QBFs (2009)
  13. Lonsing, Florian; Biere, Armin: Efficiently representing existential dependency sets for expansion-based QBF solvers (2009)
  14. Narizzano, Massimo; Peschiera, Claudia; Pulina, Luca; Tacchella, Armando: Evaluating and certifying QBFs: a comparison of state-of-the-art tools (2009)
  15. Stéphan, Igor; da Mota, Benoit; Nicolas, Pascal: From (quantified) Boolean formulae to answer set programming (2009)
  16. Kroening, Daniel; Strichman, Ofer: Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant (2008)
  17. Maratea, Marco; Ricca, Francesco; Faber, Wolfgang; Leone, Nicola: Look-back techniques and heuristics in DLV: Implementation, evaluation, and comparison to QBF solvers (2008)
  18. Pulina, Luca; Tacchella, Armando: Treewidth: A useful marker of empirical hardness in quantified Boolean logic encodings (2008)
  19. Bubeck, Uwe; Kleine Büning, Hans: Bounded universal expansion for preprocessing QBF (2007)
  20. Jussila, Toni; Biere, Armin; Sinz, Carsten; Kröning, Daniel; Wintersteiger, Christoph M.: A first step towards a unified proof checker for QBF (2007)