sQueezeBF

sQueezeBF: an effective preprocessor for QBFs based on equivalence reasoning In this paper we present sQueezeBF, an effective preprocessor for QBFs that combines various techniques for eliminating variables and/or redundant clauses. In particular sQueezeBF combines (i) variable elimination via Q-resolution, (ii) variable elimination via equivalence substitution and (iii) equivalence breaking via equivalence rewriting. The experimental analysis shows that sQueezeBF can produce significant reductions in the number of clauses and/or variables -- up to the point that some instances are solved directly by sQueezeBF -- and that it can significantly improve the efficiency of a range of state-of-the-art QBF solvers -- up to the point that some instances cannot be solved without sQueezeBF preprocessing.


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

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

  1. Egly, Uwe; Kronegger, Martin; Lonsing, Florian; Pfandler, Andreas: Conformant planning as a case study of incremental QBF solving (2017)
  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; Seidl, Martina; Van Gelder, Allen: The QBF Gallery: behind the scenes (2016)
  5. Wimmer, Ralf; Gitina, Karina; Nist, Jennifer; Scholl, Christoph; Becker, Bernd: Preprocessing for DQBF ralf (2015)
  6. Heule, Marijn J. H.; Seidl, Martina; Biere, Armin: A unified proof system for QBF preprocessing (2014)
  7. Heyman, Tamir; Smith, Dan; Mahajan, Yogesh; Leong, Lance; Abu-Haimed, Husam: Dominant controllability check using QBF-solver and netlist optimizer (2014)
  8. Janota, Mikoláš; Grigore, Radu; Marques-Silva, Joao: On QBF proofs and preprocessing (2013)
  9. Janota, Mikoláš; Klieber, William; Marques-Silva, Joao; Clarke, Edmund: Solving QBF with counterexample guided refinement (2012)
  10. Biere, Armin; Lonsing, Florian; Seidl, Martina: Blocked clause elimination for QBF (2011)
  11. Janota, Mikoláš; Marques-Silva, Joao: Abstraction-based algorithm for 2QBF (2011)
  12. Lonsing, Florian; Biere, Armin: Failed literal detection for QBF (2011)
  13. Giunchiglia, Enrico; Marin, Paolo; Narizzano, Massimo: sQueezeBF: an effective preprocessor for QBFs based on equivalence reasoning (2010)