Bloqqer

Blocked clause elimination for QBF. Quantified Boolean formulas (QBF) provide a powerful framework for encoding problems from various application domains, not least because efficient QBF solvers are available. Despite sophisticated evaluation techniques, the performance of such a solver usually depends on the way a problem is represented. However, the translation to processable QBF encodings is in general not unique and may either introduce variables and clauses not relevant for the solving process or blur information which could be beneficial for the solving process. To deal with both of these issues, preprocessors have been introduced which rewrite a given QBF before it is passed to a solver. In this paper, we present novel preprocessing methods for QBF based on blocked clause elimination (BCE), a technique successfully applied in SAT. Quantified blocked clause elimination (QBCE) allows to simulate various structural preprocessing techniques as BCE in SAT. We have implemented QBCE and extensions of QBCE in the preprocessor bloqqer. In our experiments we show that preprocessing with QBCE reduces formulas substantially and allows us to solve considerable more instances than the previous state-of-the-art


References in zbMATH (referenced in 31 articles , 1 standard article )

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

1 2 next

  1. Linsbichler, Thomas; Maratea, Marco; Niskanen, Andreas; Wallner, Johannes P.; Woltran, Stefan: Advanced algorithms for abstract dialectical frameworks based on complexity analysis of subclasses and SAT solving (2022)
  2. 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)
  3. Fandinno, Jorge; Laferriere, Francois; Romero, Javier; Schaub, Torsten; Son, Tran Cao: Planning with incomplete information in quantified answer set programming (2021)
  4. Beyersdorff, Olaf; Chew, Leroy; Sreenivasaiah, Karteek: A game characterisation of tree-like Q-resolution size (2019)
  5. Kiesl, Benjamin; Heule, Marijn J. H.; Biere, Armin: Truth assignments as conditional autarkies (2019)
  6. Peitl, Tomáš; Slivovsky, Friedrich; Szeider, Stefan: Long-distance Q-resolution with dependency schemes (2019)
  7. Pulina, Luca; Seidl, Martina: The 2016 and 2017 QBF solvers evaluations (QBFEVAL’16 and QBFEVAL’17) (2019)
  8. Kiesl, Benjamin; Seidl, Martina; Tompits, Hans; Biere, Armin: Local redundancy in SAT: generalizations of blocked clauses (2018)
  9. Egly, Uwe; Kronegger, Martin; Lonsing, Florian; Pfandler, Andreas: Conformant planning as a case study of incremental QBF solving (2017)
  10. Faymonville, Peter; Finkbeiner, Bernd; Rabe, Markus N.; Tentrup, Leander: Encodings of bounded synthesis (2017)
  11. Heule, Marijn J. H.; Seidl, Martina; Biere, Armin: Solution validation and extraction for QBF preprocessing (2017)
  12. Balabanov, Valeriy; Jiang, Jie-Hong Roland; Scholl, Christoph; Mishchenko, Alan; Brayton, Robert K.: 2QBF: challenges and solutions (2016)
  13. Balyo, Tomáš; Lonsing, Florian: HordeQBF: a modular and massively parallel QBF solver (2016)
  14. Janota, Mikoláš; Klieber, William; Marques-Silva, Joao; Clarke, Edmund: Solving QBF with counterexample guided refinement (2016)
  15. Kiesl, Benjamin; Seidl, Martina; Tompits, Hans; Biere, Armin: Super-blocked clauses (2016)
  16. Lonsing, Florian; Egly, Uwe; Seidl, Martina: Q-resolution with generalized axioms (2016)
  17. Lonsing, Florian; Seidl, Martina; Van Gelder, Allen: The QBF Gallery: behind the scenes (2016)
  18. Peitl, Tomáš; Slivovsky, Friedrich; Szeider, Stefan: Long distance Q-resolution with dependency schemes (2016)
  19. Rabe, Markus N.; Seshia, Sanjit A.: Incremental determinization (2016)
  20. Slivovsky, Friedrich; Szeider, Stefan: Quantifier reordering for QBF (2016)

1 2 next