QUBOS

QUBOS: Deciding quantified Boolean logic using propositional satisfiability solvers. We describe QUBOS (QUantified BOolean Solver), a decision procedure for quantified Boolean logic. The procedure is based on nonclausal simplification techniques that reduce formulae to a propositional clausal form after which off-the-shelf satisfiability solvers can be employed. We show that there are domains exhibiting structure for which this procedure is very effective and we report on experimental results.


References in zbMATH (referenced in 20 articles )

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

  1. Janota, Mikoláš; Klieber, William; Marques-Silva, Joao; Clarke, Edmund: Solving QBF with counterexample guided refinement (2016)
  2. Janota, Mikoláš; Marques-Silva, Joao: Expansion-based QBF solving versus Q-resolution (2015)
  3. Goldberg, Eugene; Manolios, Panagiotis: Quantifier elimination by dependency sequents (2014)
  4. Janota, Mikoláš; Klieber, William; Marques-Silva, Joao; Clarke, Edmund: Solving QBF with counterexample guided refinement (2012)
  5. Bubeck, Uwe; Kleine Büning, Hans: Rewriting (dependency-)quantified 2-CNF with arbitrary free literals into existential 2-HORN (2010)
  6. Egly, Uwe; Seidl, Martina; Woltran, Stefan: A solver for QBFs in negation normal form (2009)
  7. Lonsing, Florian; Biere, Armin: A compact representation for syntactic dependencies in QBFs (2009)
  8. Lonsing, Florian; Biere, Armin: Efficiently representing existential dependency sets for expansion-based QBF solvers (2009)
  9. Samer, Marko; Szeider, Stefan: Backdoor sets of quantified Boolean formulas (2009)
  10. Stéphan, Igor; da Mota, Benoit; Nicolas, Pascal: From (quantified) Boolean formulae to answer set programming (2009)
  11. Lonsing, Florian; Biere, Armin: Nenofex: Expanding NNF for QBF solving (2008)
  12. Bubeck, Uwe; Kleine Büning, Hans: Bounded universal expansion for preprocessing QBF (2007)
  13. Jussila, Toni; Biere, Armin; Sinz, Carsten; Kröning, Daniel; Wintersteiger, Christoph M.: A first step towards a unified proof checker for QBF (2007)
  14. Martinenghi, Davide; Christiansen, Henning; Decker, Hendrik: Integrity checking and maintenance in relational and deductive databases and beyond (2007)
  15. Arieli, Ofer; Denecker, Marc; Van Nuffelen, Bert; Bruynooghe, Maurice: Computational methods for database repair by signed formulae (2006)
  16. Prasad, Mukul R.; Biere, Armin; Gupta, Aarti: A survey of recent advances in sat-based formal verification (2005)
  17. Prasad, Mukul R.; Biere, Armin; Gupta, Aarti: A survey of recent advances in SAT-based formal verification (2005)
  18. Egly, Uwe; Seidl, Martina; Tompits, Hans; Woltran, Stefan; Zolda, Michael: Comparing different prenexing strategies for quantified Boolean formulas (2004)
  19. Besnard, Philippe; Schaub, Torsten; Tompits, Hans; Woltran, Stefan: Paraconsistent reasoning via quantified Boolean formulas. II: Circumscribing inconsistent theories (2003)
  20. Ayari, Abdelwaheb; Basin, David: QUBOS: Deciding quantified Boolean logic using propositional satisfiability solvers (2002)