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 25 articles )

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

1 2 next

  1. Bloem, Roderick; Braud-Santoni, Nicolas; Hadzic, Vedad; Egly, Uwe; Lonsing, Florian; Seidl, Martina: Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations (2021)
  2. Heule, Marijn J. H.; Seidl, Martina; Biere, Armin: Solution validation and extraction for QBF preprocessing (2017)
  3. Janota, Mikoláš; Klieber, William; Marques-Silva, Joao; Clarke, Edmund: Solving QBF with counterexample guided refinement (2016)
  4. Lonsing, Florian; Egly, Uwe; Seidl, Martina: Q-resolution with generalized axioms (2016)
  5. Fichte, Johannes K.; Szeider, Stefan: Backdoors to normality for disjunctive logic programs (2015)
  6. Janota, Mikoláš; Marques-Silva, Joao: Expansion-based QBF solving versus Q-resolution (2015)
  7. Goldberg, Eugene; Manolios, Panagiotis: Quantifier elimination by dependency sequents (2014)
  8. Janota, Mikoláš; Klieber, William; Marques-Silva, Joao; Clarke, Edmund: Solving QBF with counterexample guided refinement (2012)
  9. Bubeck, Uwe; Kleine Büning, Hans: Rewriting (dependency-)quantified 2-CNF with arbitrary free literals into existential 2-HORN (2010)
  10. Egly, Uwe; Seidl, Martina; Woltran, Stefan: A solver for QBFs in negation normal form (2009)
  11. Lonsing, Florian; Biere, Armin: A compact representation for syntactic dependencies in QBFs (2009)
  12. Lonsing, Florian; Biere, Armin: Efficiently representing existential dependency sets for expansion-based QBF solvers (2009)
  13. Samer, Marko; Szeider, Stefan: Backdoor sets of quantified Boolean formulas (2009)
  14. Stéphan, Igor; Da Mota, Benoit: A unified framework for certificate and compilation for QBF (2009)
  15. Stéphan, Igor; da Mota, Benoit; Nicolas, Pascal: From (quantified) Boolean formulae to answer set programming (2009)
  16. Lonsing, Florian; Biere, Armin: Nenofex: Expanding NNF for QBF solving (2008)
  17. Bubeck, Uwe; Kleine Büning, Hans: Bounded universal expansion for preprocessing QBF (2007)
  18. Jussila, Toni; Biere, Armin; Sinz, Carsten; Kröning, Daniel; Wintersteiger, Christoph M.: A first step towards a unified proof checker for QBF (2007)
  19. Martinenghi, Davide; Christiansen, Henning; Decker, Hendrik: Integrity checking and maintenance in relational and deductive databases and beyond (2007)
  20. Arieli, Ofer; Denecker, Marc; Van Nuffelen, Bert; Bruynooghe, Maurice: Computational methods for database repair by signed formulae (2006)

1 2 next