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 7 articles , 1 standard article )
Showing results 1 to 7 of 7.
- 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)
- 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)
- Giunchiglia, Enrico; Marin, Paolo; Narizzano, Massimo: sQueezeBF: an effective preprocessor for QBFs based on equivalence reasoning (2010)