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.
Keywords for this software
References in zbMATH (referenced in 14 articles , 1 standard article )
Showing results 1 to 14 of 14.
Sorted by year (- Pulina, Luca; Seidl, Martina: The 2016 and 2017 QBF solvers evaluations (QBFEVAL’16 and QBFEVAL’17) (2019)
- Egly, Uwe; Kronegger, Martin; Lonsing, Florian; Pfandler, Andreas: Conformant planning as a case study of incremental QBF solving (2017)
- Heule, Marijn J. H.; Seidl, Martina; Biere, Armin: Solution validation and extraction for QBF preprocessing (2017)
- Janota, Mikoláš; Klieber, William; Marques-Silva, Joao; Clarke, Edmund: Solving QBF with counterexample guided refinement (2016)
- Lonsing, Florian; Seidl, Martina; Van Gelder, Allen: The QBF Gallery: behind the scenes (2016)
- Wimmer, Ralf; Gitina, Karina; Nist, Jennifer; Scholl, Christoph; Becker, Bernd: Preprocessing for DQBF ralf (2015)
- Heule, Marijn J. H.; Seidl, Martina; Biere, Armin: A unified proof system for QBF preprocessing (2014)
- Heyman, Tamir; Smith, Dan; Mahajan, Yogesh; Leong, Lance; Abu-Haimed, Husam: Dominant controllability check using QBF-solver and netlist optimizer (2014)
- Janota, Mikoláš; Grigore, Radu; Marques-Silva, Joao: On QBF proofs and preprocessing (2013)
- Janota, Mikoláš; Klieber, William; Marques-Silva, Joao; Clarke, Edmund: Solving QBF with counterexample guided refinement (2012)
- Biere, Armin; Lonsing, Florian; Seidl, Martina: Blocked clause elimination for QBF (2011)
- Janota, Mikoláš; Marques-Silva, Joao: Abstraction-based algorithm for 2QBF (2011)
- Lonsing, Florian; Biere, Armin: Failed literal detection for QBF (2011)
- Giunchiglia, Enrico; Marin, Paolo; Narizzano, Massimo: sQueezeBF: an effective preprocessor for QBFs based on equivalence reasoning (2010)